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.instBotSubmodule {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

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

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.restrictScalars_bot (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMul S R] [IsScalarTower S R M] : Submodule.restrictScalars S ⊥ = ⊥

@[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

@[simp]

theorem Submodule.restrictScalars_eq_bot_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMul S R] [IsScalarTower S R M] {p : Submodule R M} : Submodule.restrictScalars S p = ⊥ ↔ p = ⊥

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

Equations

• Submodule.uniqueBot = { toInhabited := inferInstance, uniq := (_ : ∀ (x : { x // x ∈ ⊥ }), x = default) }

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

Equations

• Submodule.instOrderBotSubmoduleToLEToPreorderInstPartialOrderSetLike = OrderBot.mk (_ : ∀ (p : Submodule R M) (x : M), x ∈ ⊥ → x ∈ p)

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 : M), x ∈ p → x = 0

theorem Submodule.bot_ext {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : { x // x ∈ ⊥ }) (y : { x // x ∈ ⊥ }) : 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, 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, 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, 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 : { x // 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} ), ↑(LinearEquiv.symm Submodule.botEquivPUnit) x = 0

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

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

Equations

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

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 { x // x ∈ p }] : p = ⊥

Top element of a submodule

instance Submodule.instTopSubmodule {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

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

@[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.mem_top {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} : x ∈ ⊤

@[simp]

theorem Submodule.restrictScalars_top (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMul S R] [IsScalarTower S R M] : Submodule.restrictScalars S ⊤ = ⊤

@[simp]

theorem Submodule.restrictScalars_eq_top_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMul S R] [IsScalarTower S R M] {p : Submodule R M} : Submodule.restrictScalars S p = ⊤ ↔ p = ⊤

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

Equations

• Submodule.instOrderTopSubmoduleToLEToPreorderInstPartialOrderSetLike = OrderTop.mk (_ : ∀ (x : Submodule R M) (x_1 : M), x_1 ∈ x → True)

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_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : { x // x ∈ ⊤ }) : ↑Submodule.topEquiv x = ↑x

@[simp]

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

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

The top submodule is linearly equivalent to the module.

This is the module version of AddSubmonoid.topEquiv.

Equations

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

Infima & suprema in a submodule

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

Equations

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

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

Equations

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

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

Equations

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

@[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 : Submodule R M) (_ : 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) : ↑(Finset.inf s p) = ⋂ (i : ι) (_ : 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 : Submodule R M), 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 ∈ Finset.inf s p ↔ ∀ (i : ι), i ∈ s → x ∈ 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) : (Finset.sum Finset.univ fun 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 : ι), i ∈ s → f i ∈ p i) : (Finset.sum s fun i => f i) ∈ ⨆ (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.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.instUniqueSubmodule {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] : Unique (Submodule R M)

Equations

• Submodule.instUniqueSubmodule = { toInhabited := { default := ⊥ }, uniq := (_ : ∀ (a : Submodule R M), a = default) }

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.instNontrivialSubmodule {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] : Nontrivial (Submodule R M)

Equations

• @Submodule.instNontrivialSubmodule = @Submodule.instNontrivialSubmodule.proof_1

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 : M), 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 : M), x ∈ p → ∀ (y : M), 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 : { x // x ∈ 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 : { x // 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 : { x // 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] : ↑(OrderIso.symm AddSubmonoid.toNatSubmodule) = 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] : ↑(OrderIso.symm AddSubgroup.toIntSubmodule) = 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) : Submodule.toAddSubgroup (↑AddSubgroup.toIntSubmodule S) = S

@[simp]

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