# mathlibdocumentation

algebra.module.submodule_lattice

# The lattice structure on submodules #

This file defines the lattice structure on submodules, submodule.complete_lattice, 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 linear_algebra/basic.lean, most notably those which use span.

## Implementation notes #

This structure should match the add_submonoid.complete_lattice structure, and we should try to unify the APIs where possible.

@[protected, instance]
def submodule.has_bot {R : Type u_1} {M : Type u_3} [semiring R] [ M] :

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

Equations
@[protected, instance]
def submodule.inhabited' {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
Equations
@[simp]
theorem submodule.bot_coe {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
= {0}
@[simp]
theorem submodule.bot_to_add_submonoid {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
@[simp]
theorem submodule.restrict_scalars_bot (R : Type u_1) {S : Type u_2} {M : Type u_3} [semiring R] [semiring S] [ M] [ M] [ R] [ M] :
@[simp]
theorem submodule.mem_bot (R : Type u_1) {M : Type u_3} [semiring R] [ M] {x : M} :
x x = 0
@[protected, instance]
def submodule.unique_bot {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
Equations
@[protected, instance]
def submodule.order_bot {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
Equations
@[protected]
theorem submodule.eq_bot_iff {R : Type u_1} {M : Type u_3} [semiring R] [ M] (p : M) :
p = ∀ (x : M), x px = 0
@[protected, ext]
theorem submodule.bot_ext {R : Type u_1} {M : Type u_3} [semiring R] [ M] (x y : ) :
x = y
@[protected]
theorem submodule.ne_bot_iff {R : Type u_1} {M : Type u_3} [semiring R] [ M] (p : M) :
p ∃ (x : M) (H : x p), x 0
theorem submodule.nonzero_mem_of_bot_lt {R : Type u_1} {M : Type u_3} [semiring R] [ M] {p : 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] [ M] {p : M} (h : p ) :
∃ (b : M), b p b 0
@[simp]
theorem submodule.bot_equiv_punit_symm_apply {R : Type u_1} {M : Type u_3} [semiring R] [ M] (x : punit) :
@[simp]
theorem submodule.bot_equiv_punit_apply {R : Type u_1} {M : Type u_3} [semiring R] [ M] (x : ) :
def submodule.bot_equiv_punit {R : Type u_1} {M : Type u_3} [semiring R] [ M] :

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

Equations
theorem submodule.eq_bot_of_subsingleton {R : Type u_1} {M : Type u_3} [semiring R] [ M] (p : M)  :
p =
@[protected, instance]
def submodule.has_top {R : Type u_1} {M : Type u_3} [semiring R] [ M] :

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

Equations
@[simp]
theorem submodule.top_coe {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
@[simp]
theorem submodule.top_to_add_submonoid {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
@[simp]
theorem submodule.mem_top {R : Type u_1} {M : Type u_3} [semiring R] [ M] {x : M} :
@[simp]
theorem submodule.restrict_scalars_top (R : Type u_1) {S : Type u_2} {M : Type u_3} [semiring R] [semiring S] [ M] [ M] [ R] [ M] :
@[protected, instance]
def submodule.order_top {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
Equations
theorem submodule.eq_top_iff' {R : Type u_1} {M : Type u_3} [semiring R] [ M] {p : M} :
p = ∀ (x : M), x p
@[simp]
theorem submodule.top_equiv_self_symm_apply_coe {R : Type u_1} {M : Type u_3} [semiring R] [ M] (x : M) :
= x
@[simp]
theorem submodule.top_equiv_self_apply {R : Type u_1} {M : Type u_3} [semiring R] [ M] (x : ) :
def submodule.top_equiv_self {R : Type u_1} {M : Type u_3} [semiring R] [ M] :

The top submodule is linearly equivalent to the module.

Equations
@[protected, instance]
def submodule.has_Inf {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
Equations
@[protected, instance]
def submodule.has_inf {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
Equations
@[protected, instance]
def submodule.complete_lattice {R : Type u_1} {M : Type u_3} [semiring R] [ M] :
Equations
@[simp]
theorem submodule.inf_coe {R : Type u_1} {M : Type u_3} [semiring R] [ M] {p q : M} :
(p q) = p q
@[simp]
theorem submodule.mem_inf {R : Type u_1} {M : Type u_3} [semiring R] [ M] {p q : M} {x : M} :
x p q x p x q
@[simp]
theorem submodule.Inf_coe {R : Type u_1} {M : Type u_3} [semiring R] [ M] (P : set M)) :
(Inf P) = ⋂ (p : M) (H : p P), p
@[simp]
theorem submodule.finset_inf_coe {R : Type u_1} {M : Type u_3} [semiring R] [ M] {ι : Type u_2} (s : finset ι) (p : ι → M) :
(s.inf p) = ⋂ (i : ι) (H : i s), (p i)
@[simp]
theorem submodule.infi_coe {R : Type u_1} {M : Type u_3} [semiring R] [ M] {ι : Sort u_2} (p : ι → M) :
(⨅ (i : ι), p i) = ⋂ (i : ι), (p i)
@[simp]
theorem submodule.mem_Inf {R : Type u_1} {M : Type u_3} [semiring R] [ M] {S : set M)} {x : M} :
x Inf S ∀ (p : M), p Sx p
@[simp]
theorem submodule.mem_infi {R : Type u_1} {M : Type u_3} [semiring R] [ M] {ι : Sort u_2} (p : ι → 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] [ M] {ι : Type u_2} {s : finset ι} {p : ι → M} {x : M} :
x s.inf p ∀ (i : ι), i sx p i
theorem submodule.mem_sup_left {R : Type u_1} {M : Type u_3} [semiring R] [ M] {S T : M} {x : M} :
x Sx S T
theorem submodule.mem_sup_right {R : Type u_1} {M : Type u_3} [semiring R] [ M] {S T : M} {x : M} :
x Tx S T
theorem submodule.add_mem_sup {R : Type u_1} {M : Type u_3} [semiring R] [ M] {S T : M} {s t : M} (hs : s S) (ht : t T) :
s + t S T
theorem submodule.mem_supr_of_mem {R : Type u_1} {M : Type u_3} [semiring R] [ M] {ι : Sort u_2} {b : M} {p : ι → M} (i : ι) (h : b p i) :
b ⨆ (i : ι), p i
theorem submodule.sum_mem_supr {R : Type u_1} {M : Type u_3} [semiring R] [ M] {ι : Type u_2} [fintype ι] {f : ι → M} {p : ι → M} (h : ∀ (i : ι), f i p i) :
∑ (i : ι), f i ⨆ (i : ι), p i
theorem submodule.sum_mem_bsupr {R : Type u_1} {M : Type u_3} [semiring R] [ M] {ι : Type u_2} {s : finset ι} {f : ι → M} {p : ι → M} (h : ∀ (i : ι), i sf i p i) :
∑ (i : ι) in s, f i ⨆ (i : ι) (H : i s), p i

Note that submodule.mem_supr is provided in linear_algebra/basic.lean.

theorem submodule.mem_Sup_of_mem {R : Type u_1} {M : Type u_3} [semiring R] [ M] {S : set M)} {s : M} (hs : s S) {x : M} :
x sx Sup S
theorem submodule.disjoint_def {R : Type u_1} {M : Type u_3} [semiring R] [ M] {p p' : M} :
p' ∀ (x : M), x px p'x = 0
theorem submodule.disjoint_def' {R : Type u_1} {M : Type u_3} [semiring R] [ M] {p p' : M} :
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} [semiring R] [ M] {p q : M} (hpq : q) {a : p} (ha : a q) :
a = 0
def add_submonoid.to_nat_submodule {M : Type u_3}  :

An additive submonoid is equivalent to a ℕ-submodule.

Equations
@[simp]
theorem add_submonoid.to_nat_submodule_symm {M : Type u_3}  :
@[simp]
theorem add_submonoid.coe_to_nat_submodule {M : Type u_3} (S : add_submonoid M) :
@[simp]
@[simp]
theorem submodule.to_add_submonoid_to_nat_submodule {M : Type u_3} (S : M) :
def add_subgroup.to_int_submodule {M : Type u_3}  :

An additive subgroup is equivalent to a ℤ-submodule.

Equations
@[simp]
theorem add_subgroup.to_int_submodule_symm {M : Type u_3}  :
@[simp]
theorem add_subgroup.coe_to_int_submodule {M : Type u_3} (S : add_subgroup M) :
@[simp]
@[simp]
theorem submodule.to_add_subgroup_to_int_submodule {M : Type u_3} (S : M) :