mathlib3 documentation

algebra.module.submodule.lattice

The lattice structure on submodules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] [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_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]
@[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_smul 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
@[simp]
theorem submodule.restrict_scalars_eq_bot_iff {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_smul S R] [is_scalar_tower S R M] {p : submodule R M} :
@[protected, instance]
def submodule.unique_bot {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[protected, instance]
def submodule.order_bot {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[protected]
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 p x = 0
@[protected, 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
@[protected]
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
theorem submodule.nonzero_mem_of_bot_lt {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {p : submodule R 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] [add_comm_monoid M] [module R M] {p : submodule R M} (h : p ) :
(b : M), b p b 0

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] [add_comm_monoid M] [module R M] (p : submodule R M) [subsingleton p] :
p =
@[protected, 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]
@[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_smul S R] [is_scalar_tower S R M] :
@[simp]
theorem submodule.restrict_scalars_eq_top_iff {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_smul S R] [is_scalar_tower S R M] {p : submodule R M} :
@[protected, instance]
def submodule.order_top {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
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_apply {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (x : ) :
def submodule.top_equiv {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.

This is the module version of add_submonoid.top_equiv.

Equations
@[simp]
theorem submodule.top_equiv_symm_apply_coe {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
@[protected, instance]
def submodule.has_Inf {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
Equations
@[protected, instance]
def submodule.has_inf {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} :
(p q) = p q
@[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)) :
(has_Inf.Inf P) = (p : submodule R M) (H : p P), p
@[simp]
theorem submodule.finset_inf_coe {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_2} (s : finset ι) (p : ι submodule R 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] [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 has_Inf.Inf S (p : submodule R M), p S x 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
@[simp]
theorem submodule.mem_finset_inf {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_2} {s : finset ι} {p : ι submodule R M} {x : M} :
x s.inf p (i : ι), i s 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 S x 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 T x 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.sub_mem_sup {R' : Type u_1} {M' : Type u_2} [ring R'] [add_comm_group 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) :
finset.univ.sum (λ (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 s f i p i) :
s.sum (λ (i : ι), 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} :
theorem submodule.disjoint_def {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} :
disjoint p p' (x : M), x p x p' x = 0
theorem submodule.disjoint_def' {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {p p' : submodule R M} :
disjoint p p' (x : M), x p (y : M), y p' x = y x = 0
theorem submodule.eq_zero_of_coe_mem_of_disjoint {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {p q : submodule R M} (hpq : disjoint p q) {a : p} (ha : a q) :
a = 0

An additive submonoid is equivalent to a ℕ-submodule.

Equations

An additive subgroup is equivalent to a ℤ-submodule.

Equations