mathlib documentation

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

An additive submonoid is equivalent to a ℕ-submodule.

Equations