Lattice homomorphisms #
This file defines (bounded) lattice homomorphisms.
We use the FunLike
design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Types of morphisms #
SupHom
: Maps which preserve⊔
.InfHom
: Maps which preserve⊓
.SupBotHom
: Finitary supremum homomorphisms. Maps which preserve⊔
and⊥
.InfTopHom
: Finitary infimum homomorphisms. Maps which preserve⊓
and⊤
.LatticeHom
: Lattice homomorphisms. Maps which preserve⊔
and⊓
.BoundedLatticeHom
: Bounded lattice homomorphisms. Maps which preserve⊤
,⊥
,⊔
and⊓
.
Typeclasses #
TODO #
Do we need more intersections between BotHom
, TopHom
and lattice homomorphisms?
- toFun : α → β
The underlying function of a
SupHom
- map_sup' : ∀ (a b : α), SupHom.toFun s (a ⊔ b) = SupHom.toFun s a ⊔ SupHom.toFun s b
A
SupHom
preserves suprema.
The type of ⊔
-preserving functions from α
to β
.
Instances For
- toFun : α → β
The underlying function of an
InfHom
- map_inf' : ∀ (a b : α), InfHom.toFun s (a ⊓ b) = InfHom.toFun s a ⊓ InfHom.toFun s b
An
InfHom
preserves infima.
The type of ⊓
-preserving functions from α
to β
.
Instances For
- toFun : α → β
- map_sup' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊔ b) = SupHom.toFun s.toSupHom a ⊔ SupHom.toFun s.toSupHom b
- map_bot' : SupHom.toFun s.toSupHom ⊥ = ⊥
A
SupBotHom
preserves the bottom element.
The type of finitary supremum-preserving homomorphisms from α
to β
.
Instances For
- toFun : α → β
- map_inf' : ∀ (a b : α), InfHom.toFun s.toInfHom (a ⊓ b) = InfHom.toFun s.toInfHom a ⊓ InfHom.toFun s.toInfHom b
- map_top' : InfHom.toFun s.toInfHom ⊤ = ⊤
An
InfTopHom
preserves the top element.
The type of finitary infimum-preserving homomorphisms from α
to β
.
Instances For
- toFun : α → β
- map_sup' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊔ b) = SupHom.toFun s.toSupHom a ⊔ SupHom.toFun s.toSupHom b
- map_inf' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊓ b) = SupHom.toFun s.toSupHom a ⊓ SupHom.toFun s.toSupHom b
A
LatticeHom
preserves infima.
The type of lattice homomorphisms from α
to β
.
Instances For
- toFun : α → β
- map_sup' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊔ b) = SupHom.toFun s.toSupHom a ⊔ SupHom.toFun s.toSupHom b
- map_inf' : ∀ (a b : α), SupHom.toFun s.toSupHom (a ⊓ b) = SupHom.toFun s.toSupHom a ⊓ SupHom.toFun s.toSupHom b
- map_top' : SupHom.toFun s.toSupHom ⊤ = ⊤
A
BoundedLatticeHom
preserves the top element. - map_bot' : SupHom.toFun s.toSupHom ⊥ = ⊥
A
BoundedLatticeHom
preserves the bottom element.
The type of bounded lattice homomorphisms from α
to β
.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
A
SupHomClass
morphism preserves suprema.
SupHomClass F α β
states that F
is a type of ⊔
-preserving morphisms.
You should extend this class when you extend SupHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
An
InfHomClass
morphism preserves infima.
InfHomClass F α β
states that F
is a type of ⊓
-preserving morphisms.
You should extend this class when you extend InfHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
A
SupBotHomClass
morphism preserves the bottom element.
SupBotHomClass F α β
states that F
is a type of finitary supremum-preserving morphisms.
You should extend this class when you extend SupBotHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
An
InfTopHomClass
morphism preserves the top element.
InfTopHomClass F α β
states that F
is a type of finitary infimum-preserving morphisms.
You should extend this class when you extend SupBotHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
A
LatticeHomClass
morphism preserves infima.
LatticeHomClass F α β
states that F
is a type of lattice morphisms.
You should extend this class when you extend LatticeHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
A
BoundedLatticeHomClass
morphism preserves the top element.A
BoundedLatticeHomClass
morphism preserves the bottom element.
BoundedLatticeHomClass F α β
states that F
is a type of bounded lattice morphisms.
You should extend this class when you extend BoundedLatticeHom
.
Instances
Special case of map_compl
for boolean algebras.
Special case of map_sdiff
for boolean algebras.
Special case of map_symmDiff
for boolean algebras.
Supremum homomorphisms #
The constant function as a SupHom
.
Instances For
Infimum homomorphisms #
The constant function as an InfHom
.
Instances For
Finitary supremum homomorphisms #
Finitary infimum homomorphisms #
Lattice homomorphisms #
Reinterpret a LatticeHom
as an InfHom
.
Instances For
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Copy of a LatticeHom
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Instances For
Composition of LatticeHom
s as a LatticeHom
.
Instances For
An order homomorphism from a linear order is a lattice homomorphism.
Reinterpret an order homomorphism to a linear order as a LatticeHom
.
Instances For
Bounded lattice homomorphisms #
Reinterpret a BoundedLatticeHom
as a SupBotHom
.
Instances For
Reinterpret a BoundedLatticeHom
as an InfTopHom
.
Instances For
Reinterpret a BoundedLatticeHom
as a BoundedOrderHom
.
Instances For
Copy of a BoundedLatticeHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
id
as a BoundedLatticeHom
.
Instances For
Composition of BoundedLatticeHom
s as a BoundedLatticeHom
.
Instances For
Dual homs #
Reinterpret a lattice homomorphism as a lattice homomorphism between the dual lattices.
Instances For
Reinterpret a bounded lattice homomorphism as a bounded lattice homomorphism between the dual bounded lattices.
Instances For
Adjoins a ⊤
to the domain and codomain of a SupHom
.
Instances For
Adjoins a ⊥
to the domain and codomain of a SupHom
.
Instances For
Adjoins a ⊤
to the codomain of a SupHom
.
Instances For
Adjoins a ⊥
to the domain of a SupHom
.
Instances For
Adjoins a ⊤
to the domain and codomain of an InfHom
.
Instances For
Adjoins a ⊥
to the domain and codomain of an InfHom
.
Instances For
Adjoins a ⊤
to the codomain of an InfHom
.
Instances For
Adjoins a ⊥
to the codomain of an InfHom
.
Instances For
Adjoins a ⊤
to the domain and codomain of a LatticeHom
.
Instances For
Adjoins a ⊥
to the domain and codomain of a LatticeHom
.
Instances For
Adjoins a ⊤
and ⊥
to the domain and codomain of a LatticeHom
.
Instances For
Adjoins a ⊥
to the codomain of a LatticeHom
.
Instances For
Adjoins a ⊥
to the domain and codomain of a LatticeHom
.
Instances For
Adjoins a ⊤
and ⊥
to the codomain of a LatticeHom
.