The lattice structure on Submodules

This file defines the lattice structure on submodules, Submodule.CompleteLattice, with ⊥ defined as {0} and ⊓ defined as intersection of the underlying carrier. If p and q are submodules of a module, p ≤ q means that p ⊆ q.

Many results about operations on this lattice structure are defined in LinearAlgebra/Basic.lean, most notably those which use span.

Implementation notes

This structure should match the AddSubmonoid.CompleteLattice structure, and we should try to unify the APIs where possible.

Bottom element of a submodule

instance Submodule.instBot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : Bot (Submodule R M)

The set {0} is the bottom element of the lattice of submodules.

Equations

• Submodule.instBot = { bot := let __src := ⊥; { carrier := {0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }

instance Submodule.inhabited' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : Inhabited (Submodule R M)

Equations

• Submodule.inhabited' = { default := ⊥ }

@[simp]

theorem Submodule.bot_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : ↑⊥ = {0}

@[simp]

theorem Submodule.bot_toAddSubmonoid {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : ⊥.toAddSubmonoid = ⊥

@[simp]

theorem Submodule.bot_toAddSubgroup {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] : ⊥.toAddSubgroup = ⊥

@[simp]

theorem Submodule.mem_bot (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} : x ∈ ⊥ ↔ x = 0

instance Submodule.uniqueBot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : Unique ↥⊥

Equations

• Submodule.uniqueBot = { toInhabited := inferInstance, uniq := ⋯ }

instance Submodule.instOrderBot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : OrderBot (Submodule R M)

Equations

• Submodule.instOrderBot = OrderBot.mk ⋯

theorem Submodule.eq_bot_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x = 0

theorem Submodule.bot_ext_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x : ↥⊥} {y : ↥⊥} : x = y ↔ True

theorem Submodule.bot_ext {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : ↥⊥) (y : ↥⊥) : x = y

theorem Submodule.ne_bot_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0

theorem Submodule.nonzero_mem_of_bot_lt {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (bot_lt : ⊥ < p) : ∃ (a : ↥p), a ≠ 0

theorem Submodule.exists_mem_ne_zero_of_ne_bot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (h : p ≠ ⊥) : ∃ b ∈ p, b ≠ 0

@[simp]

theorem Submodule.botEquivPUnit_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : ∀ (x : ↥⊥), Submodule.botEquivPUnit x = PUnit.unit

@[simp]

theorem Submodule.botEquivPUnit_symm_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : ∀ (x : PUnit.{v + 1} ), Submodule.botEquivPUnit.symm x = 0

def Submodule.botEquivPUnit {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : ↥⊥ ≃ₗ[R] PUnit.{v + 1}

The bottom submodule is linearly equivalent to punit as an R-module.

Equations

• Submodule.botEquivPUnit = { toFun := fun (x : ↥⊥) => PUnit.unit, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : PUnit.{?u.42 + 1} ) => 0, left_inv := ⋯, right_inv := ⋯ }

theorem Submodule.subsingleton_iff_eq_bot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} : Subsingleton ↥p ↔ p = ⊥

theorem Submodule.eq_bot_of_subsingleton {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} [Subsingleton ↥p] : p = ⊥

theorem Submodule.nontrivial_iff_ne_bot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} : Nontrivial ↥p ↔ p ≠ ⊥

Top element of a submodule

instance Submodule.instTop {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : Top (Submodule R M)

The universal set is the top element of the lattice of submodules.

Equations

• Submodule.instTop = { top := let __src := ⊤; { carrier := Set.univ, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }

@[simp]

theorem Submodule.top_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : ↑⊤ = Set.univ

@[simp]

theorem Submodule.top_toAddSubmonoid {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : ⊤.toAddSubmonoid = ⊤

@[simp]

theorem Submodule.top_toAddSubgroup {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] : ⊤.toAddSubgroup = ⊤

@[simp]

theorem Submodule.mem_top {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} : x ∈ ⊤

instance Submodule.instOrderTop {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : OrderTop (Submodule R M)

Equations

• Submodule.instOrderTop = OrderTop.mk ⋯

theorem Submodule.eq_top_iff' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} : p = ⊤ ↔ ∀ (x : M), x ∈ p

@[simp]

theorem Submodule.topEquiv_symm_apply_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : ↑(Submodule.topEquiv.symm x) = x

@[simp]

theorem Submodule.topEquiv_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : ↥⊤) : Submodule.topEquiv x = ↑x

def Submodule.topEquiv {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : ↥⊤ ≃ₗ[R] M

The top submodule is linearly equivalent to the module.

This is the module version of AddSubmonoid.topEquiv.

Equations

• Submodule.topEquiv = { toFun := fun (x : ↥⊤) => ↑x, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : M) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Infima & suprema in a submodule

instance Submodule.instInfSet {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : InfSet (Submodule R M)

Equations

• Submodule.instInfSet = { sInf := fun (S : Set (Submodule R M)) => { carrier := ⋂ s ∈ S, ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }

instance Submodule.instInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : Inf (Submodule R M)

Equations

• Submodule.instInf = { inf := fun (p q : Submodule R M) => { carrier := ↑p ∩ ↑q, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }

instance Submodule.completeLattice {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : CompleteLattice (Submodule R M)

Equations

• Submodule.completeLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Submodule.inf_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} : ↑(p ⊓ q) = ↑p ∩ ↑q

@[simp]

theorem Submodule.mem_inf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} {x : M} : x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q

@[simp]

theorem Submodule.sInf_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (P : Set (Submodule R M)) : ↑(sInf P) = ⋂ p ∈ P, ↑p

@[simp]

theorem Submodule.finset_inf_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} (s : Finset ι) (p : ι → Submodule R M) : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)

@[simp]

theorem Submodule.iInf_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} (p : ι → Submodule R M) : ↑(⨅ (i : ι), p i) = ⋂ (i : ι), ↑(p i)

@[simp]

theorem Submodule.mem_sInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set (Submodule R M)} {x : M} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

@[simp]

theorem Submodule.mem_iInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} (p : ι → Submodule R M) {x : M} : x ∈ ⨅ (i : ι), p i ↔ ∀ (i : ι), x ∈ p i

@[simp]

theorem Submodule.mem_finset_inf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {s : Finset ι} {p : ι → Submodule R M} {x : M} : x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i

theorem Submodule.inf_iInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} [Nonempty ι] {p : ι → Submodule R M} (q : Submodule R M) : q ⊓ ⨅ (i : ι), p i = ⨅ (i : ι), q ⊓ p i

theorem Submodule.mem_sup_left {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} {T : Submodule R M} {x : M} : x ∈ S → x ∈ S ⊔ T

theorem Submodule.mem_sup_right {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} {T : Submodule R M} {x : M} : x ∈ T → x ∈ S ⊔ T

theorem Submodule.add_mem_sup {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} {T : Submodule R M} {s : M} {t : M} (hs : s ∈ S) (ht : t ∈ T) : s + t ∈ S ⊔ T

theorem Submodule.sub_mem_sup {R' : Type u_4} {M' : Type u_5} [Ring R'] [AddCommGroup M'] [Module R' M'] {S : Submodule R' M'} {T : Submodule R' M'} {s : M'} {t : M'} (hs : s ∈ S) (ht : t ∈ T) : s - t ∈ S ⊔ T

theorem Submodule.mem_iSup_of_mem {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} {b : M} {p : ι → Submodule R M} (i : ι) (h : b ∈ p i) : b ∈ ⨆ (i : ι), p i

theorem Submodule.sum_mem_iSup {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} [Fintype ι] {f : ι → M} {p : ι → Submodule R M} (h : ∀ (i : ι), f i ∈ p i) : ∑ i : ι, f i ∈ ⨆ (i : ι), p i

theorem Submodule.sum_mem_biSup {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {s : Finset ι} {f : ι → M} {p : ι → Submodule R M} (h : ∀ i ∈ s, f i ∈ p i) : ∑ i ∈ s, f i ∈ ⨆ i ∈ s, p i

Note that Submodule.mem_iSup is provided in Mathlib/LinearAlgebra/Span.lean.

theorem Submodule.mem_sSup_of_mem {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set (Submodule R M)} {s : Submodule R M} (hs : s ∈ S) {x : M} : x ∈ s → x ∈ sSup S

@[simp]

theorem Submodule.toAddSubmonoid_sSup {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set (Submodule R M)) : (sSup s).toAddSubmonoid = sSup (Submodule.toAddSubmonoid '' s)

@[simp]

theorem Submodule.subsingleton_iff (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : Subsingleton (Submodule R M) ↔ Subsingleton M

@[simp]

theorem Submodule.nontrivial_iff (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] : Nontrivial (Submodule R M) ↔ Nontrivial M

instance Submodule.instUniqueOfSubsingleton {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] : Unique (Submodule R M)

Equations

• Submodule.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }

instance Submodule.unique' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] : Unique (Submodule R M)

Equations

• Submodule.unique' = inferInstance

instance Submodule.instNontrivial {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] : Nontrivial (Submodule R M)

Equations

• ⋯ = ⋯

Disjointness of submodules

theorem Submodule.disjoint_def {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} : Disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = 0

theorem Submodule.disjoint_def' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} : Disjoint p p' ↔ ∀ x ∈ p, ∀ y ∈ p', x = y → x = 0

theorem Submodule.eq_zero_of_coe_mem_of_disjoint {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : Disjoint p q) {a : ↥p} (ha : ↑a ∈ q) : a = 0

theorem Submodule.mem_right_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : Disjoint p p') {x : ↥p} : ↑x ∈ p' ↔ x = 0

theorem Submodule.mem_left_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : Disjoint p p') {x : ↥p'} : ↑x ∈ p ↔ x = 0

ℕ-submodules

def AddSubmonoid.toNatSubmodule {M : Type u_3} [AddCommMonoid M] : AddSubmonoid M ≃o Submodule ℕ M

An additive submonoid is equivalent to a ℕ-submodule.

Equations

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

@[simp]

theorem AddSubmonoid.toNatSubmodule_symm {M : Type u_3} [AddCommMonoid M] : ⇑AddSubmonoid.toNatSubmodule.symm = Submodule.toAddSubmonoid

@[simp]

theorem AddSubmonoid.coe_toNatSubmodule {M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) : ↑(AddSubmonoid.toNatSubmodule S) = ↑S

@[simp]

theorem AddSubmonoid.toNatSubmodule_toAddSubmonoid {M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) : (AddSubmonoid.toNatSubmodule S).toAddSubmonoid = S

@[simp]

theorem Submodule.toAddSubmonoid_toNatSubmodule {M : Type u_3} [AddCommMonoid M] (S : Submodule ℕ M) : AddSubmonoid.toNatSubmodule S.toAddSubmonoid = S

ℤ-submodules

def AddSubgroup.toIntSubmodule {M : Type u_3} [AddCommGroup M] : AddSubgroup M ≃o Submodule ℤ M

An additive subgroup is equivalent to a ℤ-submodule.

Equations

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

@[simp]

theorem AddSubgroup.toIntSubmodule_symm {M : Type u_3} [AddCommGroup M] : ⇑AddSubgroup.toIntSubmodule.symm = Submodule.toAddSubgroup

@[simp]

theorem AddSubgroup.coe_toIntSubmodule {M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) : ↑(AddSubgroup.toIntSubmodule S) = ↑S

@[simp]

theorem AddSubgroup.toIntSubmodule_toAddSubgroup {M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) : (AddSubgroup.toIntSubmodule S).toAddSubgroup = S

@[simp]

theorem Submodule.toAddSubgroup_toIntSubmodule {M : Type u_3} [AddCommGroup M] (S : Submodule ℤ M) : AddSubgroup.toIntSubmodule S.toAddSubgroup = S