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.
The set {0}
is the bottom element of the lattice of submodules.
The bottom submodule is linearly equivalent to punit as an R
-module.
Instances For
The universal set is the top element of the lattice of submodules.
The top submodule is linearly equivalent to the module.
This is the module version of AddSubmonoid.topEquiv
.
Instances For
Note that Submodule.mem_iSup
is provided in LinearAlgebra/Span.lean
.
An additive submonoid is equivalent to a ℕ-submodule.
Instances For
An additive subgroup is equivalent to a ℤ-submodule.