# 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_2} [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_2} [semiring R] [ M] :
Equations
@[simp]
theorem submodule.bot_coe {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
= {0}
@[simp]
theorem submodule.bot_to_add_submonoid {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
@[simp]
theorem submodule.mem_bot (R : Type u_1) {M : Type u_2} [semiring R] [ M] {x : M} :
x x = 0
@[protected, instance]
def submodule.unique_bot {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
theorem submodule.nonzero_mem_of_bot_lt {R : Type u_1} {M : Type u_2} [semiring R] [ M] {I : M} (bot_lt : < I) :
∃ (a : I), a 0
@[protected, instance]
def submodule.order_bot {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
@[protected]
theorem submodule.eq_bot_iff {R : Type u_1} {M : Type u_2} [semiring R] [ M] (p : M) :
p = ∀ (x : M), x px = 0
@[protected]
theorem submodule.ne_bot_iff {R : Type u_1} {M : Type u_2} [semiring R] [ M] (p : M) :
p ∃ (x : M) (H : x p), x 0
@[protected, instance]
def submodule.has_top {R : Type u_1} {M : Type u_2} [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_2} [semiring R] [ M] :
@[simp]
theorem submodule.top_to_add_submonoid {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
@[simp]
theorem submodule.mem_top {R : Type u_1} {M : Type u_2} [semiring R] [ M] {x : M} :
@[protected, instance]
def submodule.order_top {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
theorem submodule.eq_top_iff' {R : Type u_1} {M : Type u_2} [semiring R] [ M] {p : M} :
p = ∀ (x : M), x p
@[protected, instance]
def submodule.has_Inf {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
@[protected, instance]
def submodule.has_inf {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
@[protected, instance]
def submodule.complete_lattice {R : Type u_1} {M : Type u_2} [semiring R] [ M] :
Equations
@[simp]
theorem submodule.inf_coe {R : Type u_1} {M : Type u_2} [semiring R] [ M] {p q : M} :
@[simp]
theorem submodule.mem_inf {R : Type u_1} {M : Type u_2} [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_2} [semiring R] [ M] (P : set M)) :
(Inf P) = ⋂ (p : M) (H : p P), p
@[simp]
theorem submodule.infi_coe {R : Type u_1} {M : Type u_2} [semiring R] [ M] {ι : Sort u_3} (p : ι → M) :
(⨅ (i : ι), p i) = ⋂ (i : ι), (p i)
@[simp]
theorem submodule.mem_Inf {R : Type u_1} {M : Type u_2} [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_2} [semiring R] [ M] {ι : Sort u_3} (p : ι → M) {x : M} :
(x ⨅ (i : ι), p i) ∀ (i : ι), x p i
theorem submodule.mem_sup_left {R : Type u_1} {M : Type u_2} [semiring R] [ M] {S T : M} {x : M} :
x Sx S T
theorem submodule.mem_sup_right {R : Type u_1} {M : Type u_2} [semiring R] [ M] {S T : M} {x : M} :
x Tx S T
theorem submodule.mem_supr_of_mem {R : Type u_1} {M : Type u_2} [semiring R] [ M] {ι : Sort u_3} {b : M} {p : ι → M} (i : ι) (h : b p i) :
b ⨆ (i : ι), 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_2} [semiring R] [ M] {S : set M)} {s : M} (hs : s S) {x : M} :
x sx Sup S
def add_submonoid.to_nat_submodule {M : Type u_2}  :

An additive submonoid is equivalent to a ℕ-submodule.

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