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.

source
@[protected, instance]
def submodule.has_bot {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
has_bot (submodule R M)

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

Equations
source
@[protected, instance]
def submodule.inhabited' {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
inhabited (submodule R M)
Equations
source
@[simp]
theorem submodule.bot_coe {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
↑⊥ = {0}
source
@[simp]
theorem submodule.bot_to_add_submonoid {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
⊥.to_add_submonoid = ⊥
source
@[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] :
submodule.restrict_scalars S ⊥ = ⊥
source
@[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
source
@[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_scalar S R] [is_scalar_tower S R M] {p : submodule R M} :
submodule.restrict_scalars S p = ⊥ ↔ p = ⊥
source
@[protected, instance]
def submodule.unique_bot {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
unique ↥⊥
Equations
source
@[protected, instance]
def submodule.order_bot {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
order_bot (submodule R M)
Equations
source
@[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
source
@[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
source
@[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
source
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
source
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
source
@[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) :
⇑(submodule.bot_equiv_punit.symm) x = 0
source
@[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 : ↥⊥) :
⇑submodule.bot_equiv_punit x = punit.star
source
def submodule.bot_equiv_punit {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
↥⊥ ≃ₗ[R] punit

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

Equations
source
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 = ⊥
source
@[protected, instance]
def submodule.has_top {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
has_top (submodule R M)

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

Equations
source
@[simp]
theorem submodule.top_coe {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
↑⊤ = set.univ
source
@[simp]
theorem submodule.top_to_add_submonoid {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
⊤.to_add_submonoid = ⊤
source
@[simp]
theorem submodule.mem_top {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] {x : M} :
x ∈ ⊤
source
@[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] :
submodule.restrict_scalars S ⊤ = ⊤
source
@[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_scalar S R] [is_scalar_tower S R M] {p : submodule R M} :
submodule.restrict_scalars S p = ⊤ ↔ p = ⊤
source
@[protected, instance]
def submodule.order_top {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
order_top (submodule R M)
Equations
source
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
source
@[simp]
theorem submodule.top_equiv_apply {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] (x : ↥⊤) :
⇑submodule.top_equiv x = ↑x
source
def submodule.top_equiv {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
↥⊤ ≃ₗ[R] M

The top submodule is linearly equivalent to the module.

This is the module version of add_submonoid.top_equiv.

Equations
source
@[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) :
↑(⇑(submodule.top_equiv.symm) x) = x
source
@[protected, instance]
def submodule.has_Inf {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
has_Inf (submodule R M)
Equations
source
@[protected, instance]
def submodule.has_inf {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
has_inf (submodule R M)
Equations
source
@[protected, instance]
def submodule.complete_lattice {R : Type u_1} {M : Type u_3} [semiring R] [add_comm_monoid M] [module R M] :
complete_lattice (submodule R M)
Equations
source
@[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
source
@[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
source
@[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
source
@[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)
source
@[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)
source
@[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 ∈ S → x ∈ p
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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) :
∑ (i : ι) in s, f i ∈ ⨆ (i : ι) (H : i ∈ s), p i

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

source
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 ∈ s → x ∈ Sup S
source
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
source
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
source
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
source
def add_submonoid.to_nat_submodule {M : Type u_3} [add_comm_monoid M] :
add_submonoid M ≃o submodule ℕ M

An additive submonoid is equivalent to a ℕ-submodule.

Equations
source
@[simp]
theorem add_submonoid.to_nat_submodule_symm {M : Type u_3} [add_comm_monoid M] :
⇑(add_submonoid.to_nat_submodule.symm) = submodule.to_add_submonoid
source
@[simp]
theorem add_submonoid.coe_to_nat_submodule {M : Type u_3} [add_comm_monoid M] (S : add_submonoid M) :
↑(⇑add_submonoid.to_nat_submodule S) = ↑S
source
@[simp]
theorem add_submonoid.to_nat_submodule_to_add_submonoid {M : Type u_3} [add_comm_monoid M] (S : add_submonoid M) :
(⇑add_submonoid.to_nat_submodule S).to_add_submonoid = S
source
@[simp]
theorem submodule.to_add_submonoid_to_nat_submodule {M : Type u_3} [add_comm_monoid M] (S : submodule ℕ M) :
⇑add_submonoid.to_nat_submodule S.to_add_submonoid = S
source
def add_subgroup.to_int_submodule {M : Type u_3} [add_comm_group M] :
add_subgroup M ≃o submodule ℤ M

An additive subgroup is equivalent to a ℤ-submodule.

Equations
source
@[simp]
theorem add_subgroup.to_int_submodule_symm {M : Type u_3} [add_comm_group M] :
⇑(add_subgroup.to_int_submodule.symm) = submodule.to_add_subgroup
source
@[simp]
theorem add_subgroup.coe_to_int_submodule {M : Type u_3} [add_comm_group M] (S : add_subgroup M) :
↑(⇑add_subgroup.to_int_submodule S) = ↑S
source
@[simp]
theorem add_subgroup.to_int_submodule_to_add_subgroup {M : Type u_3} [add_comm_group M] (S : add_subgroup M) :
(⇑add_subgroup.to_int_submodule S).to_add_subgroup = S
source
@[simp]
theorem submodule.to_add_subgroup_to_int_submodule {M : Type u_3} [add_comm_group M] (S : submodule ℤ M) :
⇑add_subgroup.to_int_submodule S.to_add_subgroup = S