The lattice of ideals in a ring #
Some basic results on lattice operations on ideals: ⊥, ⊤, ⊔, ⊓.
TODO #
Support right ideals, and two-sided ideals over non-commutative rings.
theorem
Ideal.instIsTwoSidedIInf
{α : Type u}
[Semiring α]
{ι : Sort u_1}
(I : ι → Ideal α)
[∀ (i : ι), (I i).IsTwoSided]
:
(iInf fun (i : ι) => I i).IsTwoSided
theorem
Ideal.eq_top_of_unit_mem
{α : Type u}
[Semiring α]
(I : Ideal α)
(x y : α)
(hx : Membership.mem I x)
(h : Eq (HMul.hMul y x) 1)
:
theorem
Ideal.eq_top_of_isUnit_mem
{α : Type u}
[Semiring α]
(I : Ideal α)
{x : α}
(hx : Membership.mem I x)
(h : IsUnit x)
:
theorem
Ideal.eq_top_iff_one
{α : Type u}
[Semiring α]
(I : Ideal α)
:
Iff (Eq I Top.top) (Membership.mem I 1)
theorem
Ideal.ne_top_iff_one
{α : Type u}
[Semiring α]
(I : Ideal α)
:
Iff (Ne I Top.top) (Not (Membership.mem I 1))
theorem
Ideal.mem_sup_left
{R : Type u}
[Semiring R]
{S T : Ideal R}
{x : R}
:
Membership.mem S x → Membership.mem (Max.max S T) x
theorem
Ideal.mem_sup_right
{R : Type u}
[Semiring R]
{S T : Ideal R}
{x : R}
:
Membership.mem T x → Membership.mem (Max.max S T) x
theorem
Ideal.mem_iSup_of_mem
{R : Type u}
[Semiring R]
{ι : Sort u_1}
{S : ι → Ideal R}
(i : ι)
{x : R}
:
Membership.mem (S i) x → Membership.mem (iSup S) x
theorem
Ideal.mem_sSup_of_mem
{R : Type u}
[Semiring R]
{S : Set (Ideal R)}
{s : Ideal R}
(hs : Membership.mem S s)
{x : R}
:
Membership.mem s x → Membership.mem (SupSet.sSup S) x
theorem
Ideal.mem_sInf
{R : Type u}
[Semiring R]
{s : Set (Ideal R)}
{x : R}
:
Iff (Membership.mem (InfSet.sInf s) x) (∀ ⦃I : Ideal R⦄, Membership.mem s I → Membership.mem I x)
theorem
Ideal.mem_inf
{R : Type u}
[Semiring R]
{I J : Ideal R}
{x : R}
:
Iff (Membership.mem (Min.min I J) x) (And (Membership.mem I x) (Membership.mem J x))
theorem
Ideal.mem_iInf
{R : Type u}
[Semiring R]
{ι : Sort u_1}
{I : ι → Ideal R}
{x : R}
:
Iff (Membership.mem (iInf I) x) (∀ (i : ι), Membership.mem (I i) x)
All ideals in a division (semi)ring are trivial.