Documentation

Mathlib.Algebra.Module.Submodule.Lattice

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.

source
ink
instance Submodule.instBotSubmodule {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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.
source
ink
instance Submodule.inhabited' {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Inhabited (Submodule R M)
Equations
  • Submodule.inhabited' = { default := ⊥ }
source
ink
@[simp]
theorem Submodule.bot_coe {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
↑⊥ = {0}
source
ink
@[simp]
theorem Submodule.bot_toAddSubmonoid {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
⊥.toAddSubmonoid = ⊥
source
ink
@[simp]
theorem Submodule.restrictScalars_bot (R : Type u_3) {S : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : Module R M] [inst : Module S M] [inst : SMul S R] [inst : IsScalarTower S R M] :
Submodule.restrictScalars S ⊥ = ⊥
source
ink
@[simp]
theorem Submodule.mem_bot (R : Type u_2) {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {x : M} :
x ∈ ⊥ ↔ x = 0
source
ink
@[simp]
theorem Submodule.restrictScalars_eq_bot_iff {R : Type u_1} {S : Type u_3} {M : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : Module R M] [inst : Module S M] [inst : SMul S R] [inst : IsScalarTower S R M] {p : Submodule R M} :
Submodule.restrictScalars S p = ⊥ ↔ p = ⊥
source
ink
instance Submodule.uniqueBot {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Unique { x // x ∈ ⊥ }
Equations
  • Submodule.uniqueBot = { toInhabited := inferInstance, uniq := (_ : ∀ (x : { x // x ∈ ⊥ }), x = default) }
source
ink
instance Submodule.instOrderBotSubmoduleToLEToPreorderInstPartialOrderSetLike {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
OrderBot (Submodule R M)
Equations
source
ink
theorem Submodule.eq_bot_iff {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) :
p = ⊥ ↔ ∀ (x : M), x ∈ p → x = 0
source
ink
theorem Submodule.bot_ext {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : { x // x ∈ ⊥ }) (y : { x // x ∈ ⊥ }) :
x = y
source
ink
theorem Submodule.ne_bot_iff {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) :
p ≠ ⊥ ↔ ∃ x, x ∈ p ∧ x ≠ 0
source
ink
theorem Submodule.nonzero_mem_of_bot_lt {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} (bot_lt : ⊥ < p) :
∃ a, a ≠ 0
source
ink
theorem Submodule.exists_mem_ne_zero_of_ne_bot {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} (h : p ≠ ⊥) :
∃ b, b ∈ p ∧ b ≠ 0
source
ink
@[simp]
theorem Submodule.botEquivPUnit_apply {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
∀ (x : { x // x ∈ ⊥ }), ↑Submodule.botEquivPUnit x = PUnit.unit
source
ink
@[simp]
theorem Submodule.botEquivPUnit_symm_apply {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
∀ (x : PUnit), ↑(LinearEquiv.symm Submodule.botEquivPUnit) x = 0
source
ink
def Submodule.botEquivPUnit {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
{ x // x ∈ ⊥ } ≃ₗ[R] PUnit

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.
source
ink
theorem Submodule.eq_bot_of_subsingleton {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) [inst : Subsingleton { x // x ∈ p }] :
p = ⊥
source
ink
instance Submodule.instTopSubmodule {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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.
source
ink
@[simp]
theorem Submodule.top_coe {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
↑⊤ = Set.univ
source
ink
@[simp]
theorem Submodule.top_toAddSubmonoid {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
⊤.toAddSubmonoid = ⊤
source
ink
@[simp]
theorem Submodule.mem_top {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {x : M} :
x ∈ ⊤
source
ink
@[simp]
theorem Submodule.restrictScalars_top (R : Type u_3) {S : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : Module R M] [inst : Module S M] [inst : SMul S R] [inst : IsScalarTower S R M] :
Submodule.restrictScalars S ⊤ = ⊤
source
ink
@[simp]
theorem Submodule.restrictScalars_eq_top_iff {R : Type u_1} {S : Type u_3} {M : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : Module R M] [inst : Module S M] [inst : SMul S R] [inst : IsScalarTower S R M] {p : Submodule R M} :
Submodule.restrictScalars S p = ⊤ ↔ p = ⊤
source
ink
instance Submodule.instOrderTopSubmoduleToLEToPreorderInstPartialOrderSetLike {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
OrderTop (Submodule R M)
Equations
  • Submodule.instOrderTopSubmoduleToLEToPreorderInstPartialOrderSetLike = OrderTop.mk (_ : ∀ (x : Submodule R M) (x_1 : M), x_1 ∈ x → True)
source
ink
theorem Submodule.eq_top_iff' {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} :
p = ⊤ ↔ ∀ (x : M), x ∈ p
source
ink
@[simp]
theorem Submodule.topEquiv_apply {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : { x // x ∈ ⊤ }) :
↑Submodule.topEquiv x = ↑x
source
ink
@[simp]
theorem Submodule.topEquiv_symm_apply_coe {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : M) :
↑(↑(LinearEquiv.symm Submodule.topEquiv) x) = x
source
ink
def Submodule.topEquiv {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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.
source
ink
instance Submodule.instInfSetSubmodule {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
InfSet (Submodule R M)
Equations
  • One or more equations did not get rendered due to their size.
source
ink
instance Submodule.instInfSubmodule {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Inf (Submodule R M)
Equations
  • One or more equations did not get rendered due to their size.
source
ink
instance Submodule.completeLattice {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
CompleteLattice (Submodule R M)
Equations
  • One or more equations did not get rendered due to their size.
source
ink
@[simp]
theorem Submodule.inf_coe {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} :
↑(p ⊓ q) = ↑p ∩ ↑q
source
ink
@[simp]
theorem Submodule.mem_inf {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} {x : M} :
x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q
source
ink
@[simp]
theorem Submodule.infₛ_coe {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (P : Set (Submodule R M)) :
↑(infₛ P) = Set.interᵢ fun p => Set.interᵢ fun h => ↑p
source
ink
@[simp]
theorem Submodule.finset_inf_coe {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Type u_1} (s : Finset ι) (p : ι → Submodule R M) :
↑(Finset.inf s p) = Set.interᵢ fun i => Set.interᵢ fun h => ↑(p i)
source
ink
@[simp]
theorem Submodule.infᵢ_coe {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Sort u_1} (p : ι → Submodule R M) :
↑(⨅ i, p i) = Set.interᵢ fun i => ↑(p i)
source
ink
@[simp]
theorem Submodule.mem_infₛ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : Set (Submodule R M)} {x : M} :
x ∈ infₛ S ↔ ∀ (p : Submodule R M), p ∈ S → x ∈ p
source
ink
@[simp]
theorem Submodule.mem_infᵢ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Sort u_1} (p : ι → Submodule R M) {x : M} :
(x ∈ ⨅ i, p i) ↔ ∀ (i : ι), x ∈ p i
source
ink
@[simp]
theorem Submodule.mem_finset_inf {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Type u_1} {s : Finset ι} {p : ι → Submodule R M} {x : M} :
x ∈ Finset.inf s p ↔ ∀ (i : ι), i ∈ s → x ∈ p i
source
ink
theorem Submodule.mem_sup_left {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : Submodule R M} {T : Submodule R M} {x : M} :
x ∈ S → x ∈ S ⊔ T
source
ink
theorem Submodule.mem_sup_right {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : Submodule R M} {T : Submodule R M} {x : M} :
x ∈ T → x ∈ S ⊔ T
source
ink
theorem Submodule.add_mem_sup {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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
source
ink
theorem Submodule.sub_mem_sup {R' : Type u_1} {M' : Type u_2} [inst : Ring R'] [inst : AddCommGroup M'] [inst : 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
source
ink
theorem Submodule.mem_supᵢ_of_mem {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Sort u_1} {b : M} {p : ι → Submodule R M} (i : ι) (h : b ∈ p i) :
b ∈ ⨆ i, p i
source
ink
theorem Submodule.sum_mem_supᵢ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Type u_1} [inst : Fintype ι] {f : ι → M} {p : ι → Submodule R M} (h : ∀ (i : ι), f i ∈ p i) :
(Finset.sum Finset.univ fun i => f i) ∈ ⨆ i, p i
source
ink
theorem Submodule.sum_mem_bsupᵢ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Type u_1} {s : Finset ι} {f : ι → M} {p : ι → Submodule R M} (h : ∀ (i : ι), i ∈ s → f i ∈ p i) :
(Finset.sum s fun i => f i) ∈ ⨆ i, ⨆ h, p i

Note that Submodule.mem_supᵢ is provided in LinearAlgebra/Span.lean.

source
ink
theorem Submodule.mem_supₛ_of_mem {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : Set (Submodule R M)} {s : Submodule R M} (hs : s ∈ S) {x : M} :
x ∈ s → x ∈ supₛ S
source
ink
theorem Submodule.disjoint_def {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {p' : Submodule R M} :
Disjoint p p' ↔ ∀ (x : M), x ∈ p → x ∈ p' → x = 0
source
ink
theorem Submodule.disjoint_def' {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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
source
ink
theorem Submodule.eq_zero_of_coe_mem_of_disjoint {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : Disjoint p q) {a : { x // x ∈ p }} (ha : ↑a ∈ q) :
a = 0
source
ink
def AddSubmonoid.toNatSubmodule {M : Type u_1} [inst : 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.
source
ink
@[simp]
theorem AddSubmonoid.toNatSubmodule_symm {M : Type u_1} [inst : AddCommMonoid M] :
↑(RelIso.toRelEmbedding (OrderIso.symm AddSubmonoid.toNatSubmodule)).toEmbedding = Submodule.toAddSubmonoid
source
ink
@[simp]
theorem AddSubmonoid.coe_toNatSubmodule {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
↑(↑(RelIso.toRelEmbedding AddSubmonoid.toNatSubmodule).toEmbedding S) = ↑S
source
ink
@[simp]
theorem AddSubmonoid.toNatSubmodule_toAddSubmonoid {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
(↑(RelIso.toRelEmbedding AddSubmonoid.toNatSubmodule).toEmbedding S).toAddSubmonoid = S
source
ink
@[simp]
theorem Submodule.toAddSubmonoid_toNatSubmodule {M : Type u_1} [inst : AddCommMonoid M] (S : Submodule ℕ M) :
↑(RelIso.toRelEmbedding AddSubmonoid.toNatSubmodule).toEmbedding S.toAddSubmonoid = S
source
ink
def AddSubgroup.toIntSubmodule {M : Type u_1} [inst : 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.
source
ink
@[simp]
theorem AddSubgroup.toIntSubmodule_symm {M : Type u_1} [inst : AddCommGroup M] :
↑(RelIso.toRelEmbedding (OrderIso.symm AddSubgroup.toIntSubmodule)).toEmbedding = Submodule.toAddSubgroup
source
ink
@[simp]
theorem AddSubgroup.coe_toIntSubmodule {M : Type u_1} [inst : AddCommGroup M] (S : AddSubgroup M) :
↑(↑(RelIso.toRelEmbedding AddSubgroup.toIntSubmodule).toEmbedding S) = ↑S
source
ink
@[simp]
theorem AddSubgroup.toIntSubmodule_toAddSubgroup {M : Type u_1} [inst : AddCommGroup M] (S : AddSubgroup M) :
Submodule.toAddSubgroup (↑(RelIso.toRelEmbedding AddSubgroup.toIntSubmodule).toEmbedding S) = S
source
ink
@[simp]
theorem Submodule.toAddSubgroup_toIntSubmodule {M : Type u_1} [inst : AddCommGroup M] (S : Submodule ℤ M) :
↑(RelIso.toRelEmbedding AddSubgroup.toIntSubmodule).toEmbedding (Submodule.toAddSubgroup S) = S