# 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.

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

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

instance Submodule.inhabited' {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
@[simp]
theorem Submodule.bot_coe {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
= {0}
@[simp]
theorem Submodule.bot_toAddSubmonoid {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
@[simp]
theorem Submodule.restrictScalars_bot (R : Type u_1) {S : Type u_2} {M : Type u_3} [] [] [] [Module R M] [Module S M] [SMul S R] [] :
@[simp]
theorem Submodule.mem_bot (R : Type u_1) {M : Type u_3} [] [] [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} [] [] [] [Module R M] [Module S M] [SMul S R] [] {p : } :
p =
instance Submodule.uniqueBot {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
Unique { x // x }
theorem Submodule.eq_bot_iff {R : Type u_1} {M : Type u_3} [] [] [Module R M] (p : ) :
p = ∀ (x : M), x px = 0
theorem Submodule.bot_ext {R : Type u_1} {M : Type u_3} [] [] [Module R M] (x : { x // x }) (y : { x // x }) :
x = y
theorem Submodule.ne_bot_iff {R : Type u_1} {M : Type u_3} [] [] [Module R M] (p : ) :
p x, x p x 0
theorem Submodule.nonzero_mem_of_bot_lt {R : Type u_1} {M : Type u_3} [] [] [Module R M] {p : } (bot_lt : < p) :
a, a 0
theorem Submodule.exists_mem_ne_zero_of_ne_bot {R : Type u_1} {M : Type u_3} [] [] [Module R M] {p : } (h : p ) :
b, b p b 0
@[simp]
theorem Submodule.botEquivPUnit_apply {R : Type u_1} {M : Type u_3} [] [] [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} [] [] [Module R M] :
∀ (x : PUnit.{v + 1} ), ↑(LinearEquiv.symm Submodule.botEquivPUnit) x = 0
def Submodule.botEquivPUnit {R : Type u_1} {M : Type u_3} [] [] [Module R M] :

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

Instances For
theorem Submodule.eq_bot_of_subsingleton {R : Type u_1} {M : Type u_3} [] [] [Module R M] (p : ) [Subsingleton { x // x p }] :
p =
instance Submodule.instTopSubmodule {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
Top ()

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

@[simp]
theorem Submodule.top_coe {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
= Set.univ
@[simp]
theorem Submodule.top_toAddSubmonoid {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
@[simp]
theorem Submodule.mem_top {R : Type u_1} {M : Type u_3} [] [] [Module R M] {x : M} :
@[simp]
theorem Submodule.restrictScalars_top (R : Type u_1) {S : Type u_2} {M : Type u_3} [] [] [] [Module R M] [Module S M] [SMul S R] [] :
@[simp]
theorem Submodule.restrictScalars_eq_top_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [] [] [] [Module R M] [Module S M] [SMul S R] [] {p : } :
p =
theorem Submodule.eq_top_iff' {R : Type u_1} {M : Type u_3} [] [] [Module R M] {p : } :
p = ∀ (x : M), x p
@[simp]
theorem Submodule.topEquiv_symm_apply_coe {R : Type u_1} {M : Type u_3} [] [] [Module R M] (x : M) :
↑(↑(LinearEquiv.symm Submodule.topEquiv) x) = x
@[simp]
theorem Submodule.topEquiv_apply {R : Type u_1} {M : Type u_3} [] [] [Module R M] (x : { x // x }) :
Submodule.topEquiv x = x
def Submodule.topEquiv {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
{ x // x } ≃ₗ[R] M

The top submodule is linearly equivalent to the module.

This is the module version of AddSubmonoid.topEquiv.

Instances For
instance Submodule.instInfSetSubmodule {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
instance Submodule.instInfSubmodule {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
Inf ()
instance Submodule.completeLattice {R : Type u_1} {M : Type u_3} [] [] [Module R M] :
@[simp]
theorem Submodule.inf_coe {R : Type u_1} {M : Type u_3} [] [] [Module R M] {p : } {q : } :
↑(p q) = p q
@[simp]
theorem Submodule.mem_inf {R : Type u_1} {M : Type u_3} [] [] [Module R M] {p : } {q : } {x : M} :
x p q x p x q
@[simp]
theorem Submodule.sInf_coe {R : Type u_1} {M : Type u_3} [] [] [Module R M] (P : Set ()) :
↑(sInf P) = ⋂ (p : ) (_ : p P), p
@[simp]
theorem Submodule.finset_inf_coe {R : Type u_1} {M : Type u_3} [] [] [Module R M] {ι : Type u_4} (s : ) (p : ι) :
↑() = ⋂ (i : ι) (_ : i s), ↑(p i)
@[simp]
theorem Submodule.iInf_coe {R : Type u_1} {M : Type u_3} [] [] [Module R M] {ι : Sort u_4} (p : ι) :
↑(⨅ (i : ι), p i) = ⋂ (i : ι), ↑(p i)
@[simp]
theorem Submodule.mem_sInf {R : Type u_1} {M : Type u_3} [] [] [Module R M] {S : Set ()} {x : M} :
x sInf S ∀ (p : ), p Sx p
@[simp]
theorem Submodule.mem_iInf {R : Type u_1} {M : Type u_3} [] [] [Module R M] {ι : Sort u_4} (p : ι) {x : M} :
x ⨅ (i : ι), p i ∀ (i : ι), x p i
@[simp]
theorem Submodule.mem_finset_inf {R : Type u_1} {M : Type u_3} [] [] [Module R M] {ι : Type u_4} {s : } {p : ι} {x : M} :
x ∀ (i : ι), i sx p i
theorem Submodule.mem_sup_left {R : Type u_1} {M : Type u_3} [] [] [Module R M] {S : } {T : } {x : M} :
x Sx S T
theorem Submodule.mem_sup_right {R : Type u_1} {M : Type u_3} [] [] [Module R M] {S : } {T : } {x : M} :
x Tx S T
theorem Submodule.add_mem_sup {R : Type u_1} {M : Type u_3} [] [] [Module R M] {S : } {T : } {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'] [] [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} [] [] [Module R M] {ι : Sort u_4} {b : M} {p : ι} (i : ι) (h : b p i) :
b ⨆ (i : ι), p i
theorem Submodule.sum_mem_iSup {R : Type u_1} {M : Type u_3} [] [] [Module R M] {ι : Type u_4} [] {f : ιM} {p : ι} (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} [] [] [Module R M] {ι : Type u_4} {s : } {f : ιM} {p : ι} (h : ∀ (i : ι), i sf i p i) :
(Finset.sum s fun i => f i) ⨆ (i : ι) (_ : i s), p i

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

theorem Submodule.mem_sSup_of_mem {R : Type u_1} {M : Type u_3} [] [] [Module R M] {S : Set ()} {s : } (hs : s S) {x : M} :
x sx sSup S
theorem Submodule.disjoint_def {R : Type u_1} {M : Type u_3} [] [] [Module R M] {p : } {p' : } :
Disjoint p p' ∀ (x : M), x px p'x = 0
theorem Submodule.disjoint_def' {R : Type u_1} {M : Type u_3} [] [] [Module R M] {p : } {p' : } :
Disjoint p p' ∀ (x : M), x p∀ (y : M), y p'x = yx = 0
theorem Submodule.eq_zero_of_coe_mem_of_disjoint {R : Type u_1} {M : Type u_3} [] [] [Module R M] {p : } {q : } (hpq : Disjoint p q) {a : { x // x p }} (ha : a q) :
a = 0

An additive submonoid is equivalent to a ℕ-submodule.

Instances For
@[simp]
theorem AddSubmonoid.toNatSubmodule_symm {M : Type u_3} [] :
@[simp]
theorem AddSubmonoid.coe_toNatSubmodule {M : Type u_3} [] (S : ) :
@[simp]
@[simp]
theorem Submodule.toAddSubmonoid_toNatSubmodule {M : Type u_3} [] (S : ) :
def AddSubgroup.toIntSubmodule {M : Type u_3} [] :

An additive subgroup is equivalent to a ℤ-submodule.

Instances For
@[simp]
theorem AddSubgroup.toIntSubmodule_symm {M : Type u_3} [] :