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.

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

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

Equations
@[instance]
def submodule.inhabited' {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[simp]
theorem submodule.bot_coe {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
= {0}
@[simp]
theorem submodule.bot_to_add_submonoid {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem submodule.restrict_scalars_bot (R : Type u_1) {S : Type u_2} {M : Type u_3} [semiring R] [semiring S] [add_comm_monoid M] [module R M] [module S M] [has_scalar S R] [is_scalar_tower S R M] :
@[simp]
theorem submodule.mem_bot (R : Type u_1) {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {x : M} :
x x = 0
@[instance]
def submodule.unique_bot {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
theorem submodule.nonzero_mem_of_bot_lt {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {I : submodule R M} (bot_lt : < I) :
∃ (a : I), a 0
theorem submodule.eq_bot_iff {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
p = ∀ (x : M), x px = 0
@[ext]
theorem submodule.bot_ext {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (x y : ) :
x = y
theorem submodule.ne_bot_iff {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) :
p ∃ (x : M) (H : x p), x 0
@[simp]
theorem submodule.bot_equiv_punit_symm_apply {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (x : punit) :
@[simp]
theorem submodule.bot_equiv_punit_apply {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (x : ) :
def submodule.bot_equiv_punit {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :

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

Equations
@[instance]
def submodule.has_top {R : Type u_1} {M : Type u_3} [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_3} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem submodule.top_to_add_submonoid {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
@[simp]
theorem submodule.mem_top {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module 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] [add_comm_monoid M] [module R M] [module S M] [has_scalar S R] [is_scalar_tower S R M] :
theorem submodule.eq_top_iff' {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {p : submodule R 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] [add_comm_monoid M] [module R M] (x : M) :
@[simp]
theorem submodule.top_equiv_self_apply {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (x : ) :
def submodule.top_equiv_self {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :

The top submodule is linearly equivalent to the module.

Equations
@[instance]
def submodule.has_Inf {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[instance]
def submodule.has_inf {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[instance]
def submodule.complete_lattice {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[simp]
theorem submodule.inf_coe {R : Type u_1} {M : Type u_3} [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_3} [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_3} [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_3} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} (p : ι → submodule R M) :
(⨅ (i : ι), p i) = ⋂ (i : ι), (p i)
@[simp]
theorem submodule.mem_Inf {R : Type u_1} {M : Type u_3} [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_3} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} (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_3} [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_3} [semiring R] [add_comm_monoid M] [module R M] {S T : submodule R M} {x : M} :
x Tx S T
theorem submodule.add_mem_sup {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {S T : submodule R 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] [add_comm_monoid M] [module R M] {ι : Sort u_2} {b : M} {p : ι → submodule R 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] [add_comm_monoid M] [module R M] {ι : Type u_2} [fintype ι] {f : ι → M} {p : ι → submodule R 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] [add_comm_monoid M] [module R M] {ι : Type u_2} {s : finset ι} {f : ι → M} {p : ι → submodule R 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] [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