The complete lattice structure on two-sided ideals

instance TwoSidedIdeal.instSemilatticeSup (R : Type u_1) [NonUnitalNonAssocRing R] : SemilatticeSup (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instSemilatticeSup R = SemilatticeSup.mk (fun (I J : TwoSidedIdeal R) => { ringCon := I.ringCon ⊔ J.ringCon }) ⋯ ⋯ ⋯

theorem TwoSidedIdeal.sup_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] (I J : TwoSidedIdeal R) : (I ⊔ J).ringCon = I.ringCon ⊔ J.ringCon

theorem TwoSidedIdeal.mem_sup_left {R : Type u_1} [NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} {x : R} (h : x ∈ I) : x ∈ I ⊔ J

theorem TwoSidedIdeal.mem_sup_right {R : Type u_1} [NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} {x : R} (h : x ∈ J) : x ∈ I ⊔ J

theorem TwoSidedIdeal.mem_sup {R : Type u_1} [NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} {x : R} : x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x

instance TwoSidedIdeal.instSemilatticeInf (R : Type u_1) [NonUnitalNonAssocRing R] : SemilatticeInf (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instSemilatticeInf R = SemilatticeInf.mk (fun (I J : TwoSidedIdeal R) => { ringCon := I.ringCon ⊓ J.ringCon }) ⋯ ⋯ ⋯

theorem TwoSidedIdeal.inf_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] (I J : TwoSidedIdeal R) : (I ⊓ J).ringCon = I.ringCon ⊓ J.ringCon

theorem TwoSidedIdeal.mem_inf (R : Type u_1) [NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R} {x : R} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

instance TwoSidedIdeal.instSupSet (R : Type u_1) [NonUnitalNonAssocRing R] : SupSet (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instSupSet R = { sSup := fun (s : Set (TwoSidedIdeal R)) => { ringCon := sSup (TwoSidedIdeal.ringCon '' s) } }

theorem TwoSidedIdeal.sSup_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] (S : Set (TwoSidedIdeal R)) : (sSup S).ringCon = sSup (TwoSidedIdeal.ringCon '' S)

theorem TwoSidedIdeal.iSup_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] {ι : Type u_2} (I : ι → TwoSidedIdeal R) : (⨆ (i : ι), I i).ringCon = ⨆ (i : ι), (I i).ringCon

instance TwoSidedIdeal.instCompleteSemilatticeSup (R : Type u_1) [NonUnitalNonAssocRing R] : CompleteSemilatticeSup (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instCompleteSemilatticeSup R = CompleteSemilatticeSup.mk ⋯ ⋯

instance TwoSidedIdeal.instInfSet (R : Type u_1) [NonUnitalNonAssocRing R] : InfSet (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instInfSet R = { sInf := fun (s : Set (TwoSidedIdeal R)) => { ringCon := sInf (TwoSidedIdeal.ringCon '' s) } }

theorem TwoSidedIdeal.sInf_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] (S : Set (TwoSidedIdeal R)) : (sInf S).ringCon = sInf (TwoSidedIdeal.ringCon '' S)

theorem TwoSidedIdeal.iInf_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] {ι : Type u_2} (I : ι → TwoSidedIdeal R) : (⨅ (i : ι), I i).ringCon = ⨅ (i : ι), (I i).ringCon

instance TwoSidedIdeal.instCompleteSemilatticeInf (R : Type u_1) [NonUnitalNonAssocRing R] : CompleteSemilatticeInf (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instCompleteSemilatticeInf R = CompleteSemilatticeInf.mk ⋯ ⋯

theorem TwoSidedIdeal.mem_iInf (R : Type u_1) [NonUnitalNonAssocRing R] {ι : Type u_2} {I : ι → TwoSidedIdeal R} {x : R} : x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i

theorem TwoSidedIdeal.mem_sInf (R : Type u_1) [NonUnitalNonAssocRing R] {S : Set (TwoSidedIdeal R)} {x : R} : x ∈ sInf S ↔ ∀ I ∈ S, x ∈ I

instance TwoSidedIdeal.instTop (R : Type u_1) [NonUnitalNonAssocRing R] : Top (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instTop R = { top := { ringCon := ⊤ } }

theorem TwoSidedIdeal.top_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] : ⊤.ringCon = ⊤

@[simp]

theorem TwoSidedIdeal.mem_top (R : Type u_1) [NonUnitalNonAssocRing R] {x : R} : x ∈ ⊤

instance TwoSidedIdeal.instBot (R : Type u_1) [NonUnitalNonAssocRing R] : Bot (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instBot R = { bot := { ringCon := ⊥ } }

theorem TwoSidedIdeal.bot_ringCon (R : Type u_1) [NonUnitalNonAssocRing R] : ⊥.ringCon = ⊥

@[simp]

theorem TwoSidedIdeal.mem_bot (R : Type u_1) [NonUnitalNonAssocRing R] {x : R} : x ∈ ⊥ ↔ x = 0

instance TwoSidedIdeal.instCompleteLattice (R : Type u_1) [NonUnitalNonAssocRing R] : CompleteLattice (TwoSidedIdeal R)

Equations

• TwoSidedIdeal.instCompleteLattice R = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem TwoSidedIdeal.one_mem_iff {R : Type u_2} [NonAssocRing R] (I : TwoSidedIdeal R) : 1 ∈ I ↔ I = ⊤

theorem TwoSidedIdeal.one_mem {R : Type u_2} [NonAssocRing R] (I : TwoSidedIdeal R) : I = ⊤ → 1 ∈ I

Alias of the reverse direction of TwoSidedIdeal.one_mem_iff.

theorem TwoSidedIdeal.eq_top {R : Type u_2} [NonAssocRing R] (I : TwoSidedIdeal R) : 1 ∈ I → I = ⊤

Alias of the forward direction of TwoSidedIdeal.one_mem_iff.