Modular Lattices #
This file defines (semi)modular lattices, a kind of lattice useful in algebra. For examples, look to the subobject lattices of abelian groups, submodules, and ideals, or consider any distributive lattice.
Typeclasses #
We define (semi)modularity typeclasses as Prop-valued mixins.
IsWeakUpperModularLattice
: Weakly upper modular lattices. Lattice wherea ⊔ b⊔ b
coversa
andb
ifa
andb
both covera ⊓ b⊓ b
.IsWeakLowerModularLattice
: Weakly lower modular lattices. Lattice wherea
andb
covera ⊓ b⊓ b
ifa ⊔ b⊔ b
covers botha
andb
IsUpperModularLattice
: Upper modular lattices. Lattices wherea ⊔ b⊔ b
coversa
ifb
coversa ⊓ b⊓ b
.IsLowerModularLattice
: Lower modular lattices. Lattices wherea
coversa ⊓ b⊓ b
ifa ⊔ b⊔ b
coversb
.
IsModularLattice
: Modular lattices. Lattices wherea ≤ c → (a ⊔ b) ⊓ c = a ⊔ (b ⊓ c)≤ c → (a ⊔ b) ⊓ c = a ⊔ (b ⊓ c)→ (a ⊔ b) ⊓ c = a ⊔ (b ⊓ c)⊔ b) ⊓ c = a ⊔ (b ⊓ c)⊓ c = a ⊔ (b ⊓ c)⊔ (b ⊓ c)⊓ c)
. We only require an inequality because the other direction holds in all lattices.
Main Definitions #
infIccOrderIsoIccSup
gives an order isomorphism between the intervals[a ⊓ b, a]⊓ b, a]
and[b, a ⊔ b]⊔ b]
. This corresponds to the diamond (or second) isomorphism theorems of algebra.
Main Results #
isModularLattice_iff_inf_sup_inf_assoc
: Modularity is equivalent to theinf_sup_inf_assoc
:(x ⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z⊓ z) ⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z⊔ (y ⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z⊓ z) = ((x ⊓ z) ⊔ y) ⊓ z⊓ z) ⊔ y) ⊓ z⊔ y) ⊓ z⊓ z
DistribLattice.isModularLattice
: Distributive lattices are modular.
References #
- [Manfred Stern, Semimodular lattices. {Theory} and applications][stern2009]
- [Wikipedia, Modular Lattice][https://en.wikipedia.org/wiki/Modular_lattice]
TODO #
- Relate atoms and coatoms in modular lattices
a ⊔ b⊔ b
coversa
andb
ifa
andb
both covera ⊓ b⊓ b
.
A weakly upper modular lattice is a lattice where a ⊔ b⊔ b
covers a
and b
if a
and b
both
cover a ⊓ b⊓ b
.
Instances
a
andb
covera ⊓ b⊓ b
ifa ⊔ b⊔ b
covers botha
andb
A weakly lower modular lattice is a lattice where a
and b
cover a ⊓ b⊓ b
if a ⊔ b⊔ b
covers
both a
and b
.
Instances
a ⊔ b⊔ b
coversa
andb
if eithera
orb
coversa ⊓ b⊓ b
An upper modular lattice, aka semimodular lattice, is a lattice where a ⊔ b⊔ b
covers a
and b
if either a
or b
covers a ⊓ b⊓ b
.
Instances
a
andb
both covera ⊓ b⊓ b
ifa ⊔ b⊔ b
covers eithera
orb
A lower modular lattice is a lattice where a
and b
both cover a ⊓ b⊓ b
if a ⊔ b⊔ b
covers
either a
or b
.
Instances
Whenever
x ≤ z≤ z
, then for anyy
,(x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)⊓ z ≤ x ⊔ (y ⊓ z)≤ x ⊔ (y ⊓ z)⊔ (y ⊓ z)⊓ z)
A modular lattice is one with a limited associativity between ⊓⊓
and ⊔⊔
.
Instances
Alias of covby_sup_of_inf_covby_of_inf_covby_left
.
Alias of inf_covby_of_covby_sup_of_covby_sup_left
.
Alias of covby_sup_of_inf_covby_left
.
Alias of covby_sup_of_inf_covby_right
.
Alias of inf_covby_of_covby_sup_left
.
Alias of inf_covby_of_covby_sup_right
.
A generalization of the theorem that if N
is a submodule of M
and
N
and M / N
are both Artinian, then M
is Artinian.
A generalization of the theorem that if N
is a submodule of M
and
N
and M / N
are both Noetherian, then M
is Noetherian.
The diamond isomorphism between the intervals [a ⊓ b, a]⊓ b, a]
and [b, a ⊔ b]⊔ b]
Equations
- One or more equations did not get rendered due to their size.
The diamond isomorphism between the intervals ]a ⊓ b, a[⊓ b, a[
and }b, a ⊔ b[⊔ b[
.
Equations
- One or more equations did not get rendered due to their size.
The diamond isomorphism between the intervals Set.Iic a
and Set.Ici b
.
Equations
- One or more equations did not get rendered due to their size.