Complete lattice homomorphisms #
This file defines frame homomorphisms and complete 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 #
sSupHom
: Maps which preserve⨆
.sInfHom
: Maps which preserve⨅
.FrameHom
: Frame homomorphisms. Maps which preserve⨆
,⊓
and⊤
.CompleteLatticeHom
: Complete lattice homomorphisms. Maps which preserve⨆
and⨅
.
Typeclasses #
Concrete homs #
CompleteLatticeHom.setPreimage
:Set.preimage
as a complete lattice homomorphism.
TODO #
Frame homs are Heyting homs.
- toFun : α → β
The underlying function of a sSupHom.
The proposition that a
sSupHom
commutes with arbitrary suprema/joins.
The type of ⨆
-preserving functions 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 ⊤ = ⊤
The proposition that frame homomorphisms commute with arbitrary suprema/joins.
The type of frame homomorphisms from α
to β
. They preserve finite meets and arbitrary joins.
Instances For
- toFun : α → β
The proposition that complete lattice homomorphism commutes with arbitrary suprema/joins.
The type of complete lattice homomorphisms from α
to β
.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
The proposition that members of
sSupHomClass
s commute with arbitrary suprema/joins.
sSupHomClass F α β
states that F
is a type of ⨆
-preserving morphisms.
You should extend this class when you extend sSupHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
The proposition that members of
sInfHomClass
s commute with arbitrary infima/meets.
sInfHomClass F α β
states that F
is a type of ⨅
-preserving morphisms.
You should extend this class when you extend sInfHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
The proposition that members of
FrameHomClass
commute with arbitrary suprema/joins.
FrameHomClass F α β
states that F
is a type of frame morphisms. They preserve ⊓
and ⨆
.
You should extend this class when you extend FrameHom
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
The proposition that members of
CompleteLatticeHomClass
commute with arbitrary suprema/joins.
CompleteLatticeHomClass F α β
states that F
is a type of complete lattice morphisms.
You should extend this class when you extend CompleteLatticeHom
.
Instances
Supremum homomorphisms #
Infimum homomorphisms #
Frame homomorphisms #
Reinterpret a FrameHom
as a LatticeHom
.
Instances For
Copy of a FrameHom
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Instances For
Instances For
Composition of FrameHom
s as a FrameHom
.
Instances For
Complete lattice homomorphisms #
Reinterpret a CompleteLatticeHom
as a sSupHom
.
Instances For
Reinterpret a CompleteLatticeHom
as a BoundedLatticeHom
.
Instances For
Copy of a CompleteLatticeHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
id
as a CompleteLatticeHom
.
Instances For
Composition of CompleteLatticeHom
s as a CompleteLatticeHom
.
Instances For
Dual homs #
Reinterpret a complete lattice homomorphism as a complete lattice homomorphism between the dual lattices.
Instances For
Concrete homs #
Set.preimage
as a complete lattice homomorphism.
See also sSupHom.setImage
.
Instances For
Using Set.image
, a function between types yields a sSupHom
between their lattices of
subsets.
See also CompleteLatticeHom.setPreimage
.
Instances For
The map (a, b) ↦ a ⊔ b
as a sSupHom
.
Instances For
The map (a, b) ↦ a ⊓ b
as an sInfHom
.