Esakia morphisms #
This file defines pseudo-epimorphisms and Esakia morphisms.
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 #
PseudoEpimorphism
: Pseudo-epimorphisms. Mapsf
such thatf a ≤ b
implies the existence ofa'
such thata ≤ a'
andf a' = b
.EsakiaHom
: Esakia morphisms. Continuous pseudo-epimorphisms.
Typeclasses #
References #
- toFun : α → β
- monotone' : Monotone s.toFun
- exists_map_eq_of_map_le' : ∀ ⦃a : α⦄ ⦃b : β⦄, OrderHom.toFun s.toOrderHom a ≤ b → ∃ c, a ≤ c ∧ OrderHom.toFun s.toOrderHom c = b
The type of pseudo-epimorphisms, aka p-morphisms, aka bounded maps, from α
to β
.
Instances For
- toFun : α → β
- monotone' : Monotone s.toFun
- continuous_toFun : Continuous s.toFun
- exists_map_eq_of_map_le' : ∀ ⦃a : α⦄ ⦃b : β⦄, OrderHom.toFun s.toOrderHom a ≤ b → ∃ c, a ≤ c ∧ OrderHom.toFun s.toOrderHom c = b
The type of Esakia morphisms, aka continuous pseudo-epimorphisms, from α
to β
.
Instances For
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
PseudoEpimorphismClass F α β
states that F
is a type of ⊔
-preserving morphisms.
You should extend this class when you extend PseudoEpimorphism
.
Instances
- coe : F → α → β
- coe_injective' : Function.Injective FunLike.coe
- map_continuous : ∀ (f : F), Continuous ↑f
- map_monotone : ∀ (f : F), Monotone ↑f
EsakiaHomClass F α β
states that F
is a type of lattice morphisms.
You should extend this class when you extend EsakiaHom
.
Instances
Pseudo-epimorphisms #
Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun
directly.
Copy of a PseudoEpimorphism
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Instances For
id
as a PseudoEpimorphism
.
Instances For
Composition of PseudoEpimorphism
s as a PseudoEpimorphism
.
Instances For
Esakia morphisms #
Instances For
Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun
directly.
Copy of an EsakiaHom
with a new toFun
equal to the old one. Useful to fix definitional
equalities.
Instances For
Instances For
Composition of EsakiaHom
s as an EsakiaHom
.