Supports of subsemirings

Let R be a ring, and let S be a subsemiring of R. If S - S = S, then the support of S forms an ideal.

Main definitions

• Subsemiring.support: the support of a subsemiring, as an ideal.

theorem Subsemiring.eq_zero_of_mem_of_neg_mem {R : Type u_1} [Ring R] (S : Subsemiring R) [S.toAddSubmonoid.IsPointed] {x : R} (hx₁ : x ∈ S) (hx₂ : -x ∈ S) : x = 0

theorem Subsemiring.eq_zero_of_mem_of_neg_mem₂ {R : Type u_1} [Ring R] (S : Subsemiring R) [S.toAddSubmonoid.IsPointed] {x : R} (hx₁ : x ∈ S) (hx₂ : -x ∈ S) : x = 0

Alias of Subsemiring.eq_zero_of_mem_of_neg_mem.

theorem Subsemiring.mem_or_neg_mem {R : Type u_1} [Ring R] (S : Subsemiring R) [S.toAddSubmonoid.IsSpanning] (a : R) : a ∈ S ∨ -a ∈ S

class Subsemiring.HasIdealSupport {R : Type u_1} [Ring R] (S : Subsemiring R) : Prop

Typeclass to track when the support of a subsemiring forms an ideal.

• smul_mem_support (x : R) {a : R} (ha : a ∈ S.toAddSubmonoid.support) : x * a ∈ S.toAddSubmonoid.support

theorem Subsemiring.hasIdealSupport_iff {R : Type u_1} [Ring R] {S : Subsemiring R} : S.HasIdealSupport ↔ ∀ (x a : R), a ∈ S → -a ∈ S → x * a ∈ S ∧ -(x * a) ∈ S

theorem Subsemiring.smul_mem {R : Type u_1} [Ring R] (S : Subsemiring R) [S.HasIdealSupport] (x : R) {a : R} (h₁a : a ∈ S) (h₂a : -a ∈ S) : x * a ∈ S

theorem Subsemiring.neg_smul_mem {R : Type u_1} [Ring R] (S : Subsemiring R) [S.HasIdealSupport] (x : R) {a : R} (h₁a : a ∈ S) (h₂a : -a ∈ S) : -(x * a) ∈ S

def Subsemiring.support {R : Type u_1} [Ring R] (S : Subsemiring R) [S.HasIdealSupport] : Ideal R

The support S ∩ -S of a subsemiring S of a ring R, as an ideal.

Equations

• S.support = { toAddSubmonoid := S.toAddSubmonoid.support.toAddSubmonoid, smul_mem' := ⋯ }

theorem Subsemiring.mem_support {R : Type u_1} [Ring R] {S : Subsemiring R} [S.HasIdealSupport] {x : R} : x ∈ S.support ↔ x ∈ S ∧ -x ∈ S

theorem Subsemiring.coe_support {R : Type u_1} [Ring R] (S : Subsemiring R) [S.HasIdealSupport] : ↑S.support = ↑S ∩ -↑S

@[simp]

theorem Subsemiring.toAddSubmonoid_support {R : Type u_1} [Ring R] (S : Subsemiring R) [S.HasIdealSupport] : S.toAddSubmonoid.support = Submodule.toAddSubgroup S.support

instance Subsemiring.instHasIdealSupportOfIsSpanningToAddSubmonoid {R : Type u_1} [Ring R] (S : Subsemiring R) [S.toAddSubmonoid.IsSpanning] : S.HasIdealSupport

@[simp]

theorem Subsemiring.comap_toSubmonoid' {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (Q : Subsemiring S) : (comap f Q).toSubmonoid = Submonoid.comap (↑f) Q.toSubmonoid

@[simp]

theorem Subsemiring.comap_toAddSubmonoid {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (Q : Subsemiring S) : (comap f Q).toAddSubmonoid = AddSubmonoid.comap f.toAddMonoidHom Q.toAddSubmonoid

@[simp]

theorem Subsemiring.map_toSubmonoid' {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (P : Subsemiring R) : (map f P).toSubmonoid = Submonoid.map (↑f) P.toSubmonoid

@[simp]

theorem Subsemiring.map_toAddSubmonoid {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (P : Subsemiring R) : (map f P).toAddSubmonoid = AddSubmonoid.map f.toAddMonoidHom P.toAddSubmonoid

instance Subsemiring.instHasIdealSupportOfIsPointedToAddSubmonoid {R : Type u_2} [Ring R] (S : Subsemiring R) [S.toAddSubmonoid.IsPointed] : S.HasIdealSupport

@[simp]

theorem Subsemiring.support_eq_bot {R : Type u_2} [Ring R] (S : Subsemiring R) [S.toAddSubmonoid.IsPointed] : S.support = ⊥

theorem Subsemiring.IsPointed.neg_one_notMem {R : Type u_2} [Ring R] (S : Subsemiring R) [Nontrivial R] [S.toAddSubmonoid.IsPointed] : -1 ∉ S

instance Subsemiring.instIsSpanningToAddSubmonoidComap {R : Type u_2} {R' : Type u_3} [Ring R] [Ring R'] (f : R →+* R') (S' : Subsemiring R') [S'.toAddSubmonoid.IsSpanning] : (comap f S').toAddSubmonoid.IsSpanning

theorem Subsemiring.IsSpanning.map {R : Type u_2} {R' : Type u_3} [Ring R] [Ring R'] {f : R →+* R'} (S : Subsemiring R) [S.toAddSubmonoid.IsSpanning] (hf : Function.Surjective ⇑f) : (Subsemiring.map f S).toAddSubmonoid.IsSpanning

theorem Subsemiring.IsPointed.of_support_eq_bot {R : Type u_2} [Ring R] (S : Subsemiring R) [S.HasIdealSupport] (h : S.support = ⊥) : S.toAddSubmonoid.IsPointed

theorem Subsemiring.support_mono {R : Type u_2} [Ring R] {S T : Subsemiring R} [S.HasIdealSupport] [T.HasIdealSupport] (h : S ≤ T) : S.support ≤ T.support

instance Subsemiring.instHasIdealSupportMin {R : Type u_2} [Ring R] (S T : Subsemiring R) [S.HasIdealSupport] [T.HasIdealSupport] : (S ⊓ T).HasIdealSupport

@[simp]

theorem Subsemiring.support_inf {R : Type u_2} [Ring R] (S T : Subsemiring R) [S.HasIdealSupport] [T.HasIdealSupport] : (S ⊓ T).support = S.support ⊓ T.support

theorem Subsemiring.HasIdealSupport.sInf {R : Type u_2} [Ring R] {s : Set (Subsemiring R)} (h : ∀ S ∈ s, S.HasIdealSupport) : (InfSet.sInf s).HasIdealSupport

@[simp]

theorem Subsemiring.support_sInf {R : Type u_2} [Ring R] {s : Set (Subsemiring R)} (h : ∀ S ∈ s, S.HasIdealSupport) : (sInf s).support = sInf {I : Ideal R | ∃ (S : Subsemiring R) (hS : S ∈ s), I = S.support}

theorem Subsemiring.HasIdealSupport.sSup {R : Type u_2} [Ring R] {s : Set (Subsemiring R)} (hsn : s.Nonempty) (hsd : DirectedOn (fun (x1 x2 : Subsemiring R) => x1 ≤ x2) s) (h : ∀ S ∈ s, S.HasIdealSupport) : (sSup s).HasIdealSupport

@[simp]

theorem Subsemiring.support_sSup {R : Type u_2} [Ring R] {s : Set (Subsemiring R)} (hsn : s.Nonempty) (hsd : DirectedOn (fun (x1 x2 : Subsemiring R) => x1 ≤ x2) s) (h : ∀ S ∈ s, S.HasIdealSupport) : (sSup s).support = sSup {I : Ideal R | ∃ (S : Subsemiring R) (hS : S ∈ s), I = S.support}

instance Subsemiring.instHasIdealSupportComap {R : Type u_2} {R' : Type u_3} [Ring R] [Ring R'] (f : R →+* R') (S' : Subsemiring R') [S'.HasIdealSupport] : (comap f S').HasIdealSupport

@[simp]

theorem Subsemiring.comap_support {R : Type u_2} {R' : Type u_3} [Ring R] [Ring R'] (f : R →+* R') (S' : Subsemiring R') [S'.HasIdealSupport] : (comap f S').support = Ideal.comap f S'.support

theorem Subsemiring.HasIdealSupport.map {R : Type u_2} {R' : Type u_3} [Ring R] [Ring R'] {f : R →+* R'} {S : Subsemiring R} [S.HasIdealSupport] (hf : Function.Surjective ⇑f) (hsupp : f.toAddMonoidHom.ker ≤ S.toAddSubmonoid.support) : (Subsemiring.map f S).HasIdealSupport

@[simp]

theorem Subsemiring.map_support {R : Type u_2} {R' : Type u_3} [Ring R] [Ring R'] {f : R →+* R'} {S : Subsemiring R} [S.HasIdealSupport] (hf : Function.Surjective ⇑f) (hsupp : RingHom.ker f ≤ S.support) : (map f S).support = Ideal.map f S.support

instance instIsSpanningToAddSubmonoidNonneg (R : Type u_2) [Ring R] [LinearOrder R] [IsOrderedRing R] : (Subsemiring.nonneg R).toAddSubmonoid.IsSpanning

instance instIsPointedToAddSubmonoidNonneg (R : Type u_2) [Ring R] [PartialOrder R] [IsOrderedRing R] : (Subsemiring.nonneg R).toAddSubmonoid.IsPointed

theorem IsOrderedRing.mkOfSubsemiring {R : Type u_2} [Ring R] (S : Subsemiring R) [S.toAddSubmonoid.IsPointed] : IsOrderedRing R

noncomputable def Ring.isPointedPartialOrderEquiv (R : Type u_2) [Ring R] : { C : Subsemiring R // C.toAddSubmonoid.IsPointed } ≃ { o : PartialOrder R // IsOrderedRing R }

Equivalence between subsemirings with zero support in a ring R and partially ordered ring structures on R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ring.isPointedPartialOrderEquiv_apply {R : Type u_2} [Ring R] (C : Subsemiring R) (h : C.toAddSubmonoid.IsPointed) : ↑((isPointedPartialOrderEquiv R) ⟨C, h⟩) = PartialOrder.mkOfAddSubmonoid C.toAddSubmonoid

@[simp]

theorem Ring.isPointedPartialOrderEquiv_symm_apply {R : Type u_2} [Ring R] (o : PartialOrder R) (h : IsOrderedRing R) : ↑((isPointedPartialOrderEquiv R).symm ⟨o, h⟩) = Subsemiring.nonneg R

noncomputable def Ring.isPointedLinearOrderEquiv (R : Type u_2) [Ring R] : { C : Subsemiring R // C.toAddSubmonoid.IsPointed ∧ C.toAddSubmonoid.IsSpanning } ≃ { o : LinearOrder R // IsOrderedRing R }

Equivalence between maximal subsemirings with zero support in a ring R and linearly ordered ring structures on R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ring.isPointedLinearOrderEquiv_apply {R : Type u_2} [Ring R] (C : Subsemiring R) (h : C.toAddSubmonoid.IsPointed ∧ C.toAddSubmonoid.IsSpanning) : ↑((isPointedLinearOrderEquiv R) ⟨C, h⟩) = have this := ⋯; have this_1 := ⋯; LinearOrder.mkOfAddSubmonoid C.toAddSubmonoid

@[simp]

theorem Ring.isPointedLinearOrderEquiv_symm_apply {R : Type u_2} [Ring R] (o : LinearOrder R) (h : IsOrderedRing R) : ↑((isPointedLinearOrderEquiv R).symm ⟨o, h⟩) = Subsemiring.nonneg R