The lattice structure on Submodule
s #
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.
Bottom element of a submodule #
The set {0}
is the bottom element of the lattice of submodules.
Equations
- Submodule.instBot = { bot := let __src := ⊥; { carrier := {0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }
Equations
- Submodule.inhabited' = { default := ⊥ }
Equations
- Submodule.uniqueBot = { toInhabited := inferInstance, uniq := ⋯ }
Equations
The bottom submodule is linearly equivalent to punit as an R
-module.
Equations
- Submodule.botEquivPUnit = { toFun := fun (x : ↥⊥) => PUnit.unit, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : PUnit.{?u.42 + 1}) => 0, left_inv := ⋯, right_inv := ⋯ }
Instances For
Top element of a submodule #
The universal set is the top element of the lattice of submodules.
Equations
- Submodule.instTop = { top := let __src := ⊤; { carrier := Set.univ, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }
Equations
The top submodule is linearly equivalent to the module.
This is the module version of AddSubmonoid.topEquiv
.
Equations
- Submodule.topEquiv = { toFun := fun (x : ↥⊤) => ↑x, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : M) => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
Instances For
Infima & suprema in a submodule #
Equations
- Submodule.instInfSet = { sInf := fun (S : Set (Submodule R M)) => { carrier := ⋂ s ∈ S, ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }
Equations
- Submodule.instMin = { min := fun (p q : Submodule R M) => { carrier := ↑p ∩ ↑q, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ } }
Equations
- Submodule.completeLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Note that Submodule.mem_iSup
is provided in Mathlib/LinearAlgebra/Span.lean
.
Equations
- Submodule.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }
Equations
Disjointness of submodules #
ℕ-submodules #
An additive submonoid is equivalent to a ℕ-submodule.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ℤ-submodules #
An additive subgroup is equivalent to a ℤ-submodule.
Equations
- One or more equations did not get rendered due to their size.