Documentation

Mathlib.Algebra.Module.Submodule.Lattice

The lattice structure on Submodules #

This file defines the lattice structure on submodules, Submodule.CompleteLattice, 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 LinearAlgebra/Basic.lean, most notably those which use span.

Implementation notes #

This structure should match the AddSubmonoid.CompleteLattice structure, and we should try to unify the APIs where possible.

instance Submodule.instBotSubmodule {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

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

Equations
  • One or more equations did not get rendered due to their size.
instance Submodule.inhabited' {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Equations
  • Submodule.inhabited' = { default := }
@[simp]
theorem Submodule.bot_coe {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
= {0}
@[simp]
theorem Submodule.bot_toAddSubmonoid {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
.toAddSubmonoid =
@[simp]
theorem Submodule.restrictScalars_bot (R : Type u_3) {S : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : Module R M] [inst : Module S M] [inst : SMul S R] [inst : IsScalarTower S R M] :
@[simp]
theorem Submodule.mem_bot (R : Type u_2) {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {x : M} :
x x = 0
@[simp]
theorem Submodule.restrictScalars_eq_bot_iff {R : Type u_1} {S : Type u_3} {M : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : Module R M] [inst : Module S M] [inst : SMul S R] [inst : IsScalarTower S R M] {p : Submodule R M} :
instance Submodule.uniqueBot {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Unique { x // x }
Equations
  • Submodule.uniqueBot = { toInhabited := inferInstance, uniq := (_ : ∀ (x : { x // x }), x = default) }
Equations
theorem Submodule.eq_bot_iff {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) :
p = ∀ (x : M), x px = 0
theorem Submodule.bot_ext {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : { x // x }) (y : { x // x }) :
x = y
theorem Submodule.ne_bot_iff {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) :
p x, x p x 0
theorem Submodule.nonzero_mem_of_bot_lt {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} (bot_lt : < p) :
a, a 0
theorem Submodule.exists_mem_ne_zero_of_ne_bot {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} (h : p ) :
b, b p b 0
@[simp]
theorem Submodule.botEquivPUnit_apply {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
∀ (x : { x // x }), Submodule.botEquivPUnit x = PUnit.unit
@[simp]
theorem Submodule.botEquivPUnit_symm_apply {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
∀ (x : PUnit), ↑(LinearEquiv.symm Submodule.botEquivPUnit) x = 0
def Submodule.botEquivPUnit {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
{ x // x } ≃ₗ[R] PUnit

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

Equations
  • One or more equations did not get rendered due to their size.
theorem Submodule.eq_bot_of_subsingleton {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (p : Submodule R M) [inst : Subsingleton { x // x p }] :
p =
instance Submodule.instTopSubmodule {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Submodule.top_coe {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
= Set.univ
@[simp]
theorem Submodule.top_toAddSubmonoid {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
.toAddSubmonoid =
@[simp]
theorem Submodule.mem_top {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {x : M} :
@[simp]
theorem Submodule.restrictScalars_top (R : Type u_3) {S : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : Module R M] [inst : Module S M] [inst : SMul S R] [inst : IsScalarTower S R M] :
@[simp]
theorem Submodule.restrictScalars_eq_top_iff {R : Type u_1} {S : Type u_3} {M : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : Module R M] [inst : Module S M] [inst : SMul S R] [inst : IsScalarTower S R M] {p : Submodule R M} :
Equations
  • Submodule.instOrderTopSubmoduleToLEToPreorderInstPartialOrderSetLike = OrderTop.mk (_ : ∀ (x : Submodule R M) (x_1 : M), x_1 xTrue)
theorem Submodule.eq_top_iff' {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} :
p = ∀ (x : M), x p
@[simp]
theorem Submodule.topEquiv_apply {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : { x // x }) :
Submodule.topEquiv x = x
@[simp]
theorem Submodule.topEquiv_symm_apply_coe {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : M) :
↑(↑(LinearEquiv.symm Submodule.topEquiv) x) = x
def Submodule.topEquiv {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
{ x // x } ≃ₗ[R] M

The top submodule is linearly equivalent to the module.

This is the module version of AddSubmonoid.topEquiv.

Equations
  • One or more equations did not get rendered due to their size.
instance Submodule.instInfSetSubmodule {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Equations
  • One or more equations did not get rendered due to their size.
instance Submodule.instInfSubmodule {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Equations
  • One or more equations did not get rendered due to their size.
instance Submodule.completeLattice {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Submodule.inf_coe {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} :
↑(p q) = p q
@[simp]
theorem Submodule.mem_inf {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} {x : M} :
x p q x p x q
@[simp]
theorem Submodule.infₛ_coe {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (P : Set (Submodule R M)) :
↑(infₛ P) = Set.interᵢ fun p => Set.interᵢ fun h => p
@[simp]
theorem Submodule.finset_inf_coe {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Type u_1} (s : Finset ι) (p : ιSubmodule R M) :
↑(Finset.inf s p) = Set.interᵢ fun i => Set.interᵢ fun h => ↑(p i)
@[simp]
theorem Submodule.infᵢ_coe {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Sort u_1} (p : ιSubmodule R M) :
↑(i, p i) = Set.interᵢ fun i => ↑(p i)
@[simp]
theorem Submodule.mem_infₛ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : Set (Submodule R M)} {x : M} :
x infₛ S ∀ (p : Submodule R M), p Sx p
@[simp]
theorem Submodule.mem_infᵢ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Sort u_1} (p : ιSubmodule R M) {x : M} :
(x i, p i) ∀ (i : ι), x p i
@[simp]
theorem Submodule.mem_finset_inf {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Type u_1} {s : Finset ι} {p : ιSubmodule R M} {x : M} :
x Finset.inf s p ∀ (i : ι), i sx p i
theorem Submodule.mem_sup_left {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : Submodule R M} {T : Submodule R M} {x : M} :
x Sx S T
theorem Submodule.mem_sup_right {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : Submodule R M} {T : Submodule R M} {x : M} :
x Tx S T
theorem Submodule.add_mem_sup {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : Submodule R M} {T : Submodule R M} {s : M} {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} [inst : Ring R'] [inst : AddCommGroup M'] [inst : Module R' M'] {S : Submodule R' M'} {T : Submodule R' M'} {s : M'} {t : M'} (hs : s S) (ht : t T) :
s - t S T
theorem Submodule.mem_supᵢ_of_mem {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Sort u_1} {b : M} {p : ιSubmodule R M} (i : ι) (h : b p i) :
b i, p i
theorem Submodule.sum_mem_supᵢ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Type u_1} [inst : Fintype ι] {f : ιM} {p : ιSubmodule R M} (h : ∀ (i : ι), f i p i) :
(Finset.sum Finset.univ fun i => f i) i, p i
theorem Submodule.sum_mem_bsupᵢ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {ι : Type u_1} {s : Finset ι} {f : ιM} {p : ιSubmodule R M} (h : ∀ (i : ι), i sf i p i) :
(Finset.sum s fun i => f i) i, h, p i

Note that Submodule.mem_supᵢ is provided in LinearAlgebra/Span.lean.

theorem Submodule.mem_supₛ_of_mem {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {S : Set (Submodule R M)} {s : Submodule R M} (hs : s S) {x : M} :
x sx supₛ S
theorem Submodule.disjoint_def {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {p' : Submodule R M} :
Disjoint p p' ∀ (x : M), x px p'x = 0
theorem Submodule.disjoint_def' {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {p' : Submodule R M} :
Disjoint p p' ∀ (x : M), x p∀ (y : M), y p'x = yx = 0
theorem Submodule.eq_zero_of_coe_mem_of_disjoint {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : Disjoint p q) {a : { x // x p }} (ha : a q) :
a = 0

An additive submonoid is equivalent to a ℕ-submodule.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubmonoid.toNatSubmodule_symm {M : Type u_1} [inst : AddCommMonoid M] :
(RelIso.toRelEmbedding (OrderIso.symm AddSubmonoid.toNatSubmodule)).toEmbedding = Submodule.toAddSubmonoid
@[simp]
theorem AddSubmonoid.coe_toNatSubmodule {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
↑((RelIso.toRelEmbedding AddSubmonoid.toNatSubmodule).toEmbedding S) = S
@[simp]
theorem AddSubmonoid.toNatSubmodule_toAddSubmonoid {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :
((RelIso.toRelEmbedding AddSubmonoid.toNatSubmodule).toEmbedding S).toAddSubmonoid = S
@[simp]
theorem Submodule.toAddSubmonoid_toNatSubmodule {M : Type u_1} [inst : AddCommMonoid M] (S : Submodule M) :
(RelIso.toRelEmbedding AddSubmonoid.toNatSubmodule).toEmbedding S.toAddSubmonoid = S

An additive subgroup is equivalent to a ℤ-submodule.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem AddSubgroup.toIntSubmodule_symm {M : Type u_1} [inst : AddCommGroup M] :
(RelIso.toRelEmbedding (OrderIso.symm AddSubgroup.toIntSubmodule)).toEmbedding = Submodule.toAddSubgroup
@[simp]
theorem AddSubgroup.coe_toIntSubmodule {M : Type u_1} [inst : AddCommGroup M] (S : AddSubgroup M) :
↑((RelIso.toRelEmbedding AddSubgroup.toIntSubmodule).toEmbedding S) = S
@[simp]
theorem AddSubgroup.toIntSubmodule_toAddSubgroup {M : Type u_1} [inst : AddCommGroup M] (S : AddSubgroup M) :
Submodule.toAddSubgroup ((RelIso.toRelEmbedding AddSubgroup.toIntSubmodule).toEmbedding S) = S
@[simp]
theorem Submodule.toAddSubgroup_toIntSubmodule {M : Type u_1} [inst : AddCommGroup M] (S : Submodule M) :
(RelIso.toRelEmbedding AddSubgroup.toIntSubmodule).toEmbedding (Submodule.toAddSubgroup S) = S