Bounded order homomorphisms #
This file defines (bounded) order 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 #
TopHom
: Maps which preserve⊤⊤
.BotHom
: Maps which preserve⊥⊥
.BoundedOrderHom
: Bounded order homomorphisms. Monotone maps which preserve⊤⊤
and⊥⊥
.
Typeclasses #
The underlying function. The preferred spelling is
FunLike.coe
.toFun : α → βThe function preserves the top element. The preferred spelling is
map_top
.
The type of ⊤⊤
-preserving functions from α
to β
.
Instances For
The underlying function. The preferred spelling is
FunLike.coe
.toFun : α → βThe function preserves the bottom element. The preferred spelling is
map_bot
.
The type of ⊥⊥
-preserving functions from α
to β
.
Instances For
The function preserves the top element. The preferred spelling is
map_top
.The function preserves the bottom element. The preferred spelling is
map_bot
.
The type of bounded order homomorphisms from α
to β
.
Instances For
A
TopHomClass
morphism preserves the top element.
TopHomClass F α β
states that F
is a type of ⊤⊤
-preserving morphisms.
You should extend this class when you extend TopHom
.
Instances
A
BotHomClass
morphism preserves the bottom element.
BotHomClass F α β
states that F
is a type of ⊥⊥
-preserving morphisms.
You should extend this class when you extend BotHom
.
Instances
Morphisms preserve the top element. The preferred spelling is
_root_.map_top
.Morphisms preserve the bottom element. The preferred spelling is
_root_.map_bot
.
BoundedOrderHomClass F α β
states that F
is a type of bounded order morphisms.
You should extend this class when you extend BoundedOrderHom
.
Instances
Equations
- BoundedOrderHomClass.toTopHomClass = let src := inst; TopHomClass.mk (_ : ∀ (f : F), ↑f ⊤ = ⊤)
Equations
- BoundedOrderHomClass.toBotHomClass = let src := inst; BotHomClass.mk (_ : ∀ (f : F), ↑f ⊥ = ⊥)
Equations
- OrderIsoClass.toTopHomClass = let src := let_fun this := inferInstance; this; TopHomClass.mk (_ : ∀ (f : F), ↑f ⊤ = ⊤)
Equations
- OrderIsoClass.toBotHomClass = let src := let_fun this := inferInstance; this; BotHomClass.mk (_ : ∀ (f : F), ↑f ⊥ = ⊥)
Equations
- One or more equations did not get rendered due to their size.
Turn an element of a type F
satisfying TopHomClass F α β
into an actual
TopHom
. This is declared as the default coercion from F
to TopHom α β
.
Turn an element of a type F
satisfying BotHomClass F α β
into an actual
BotHom
. This is declared as the default coercion from F
to BotHom α β
.
Turn an element of a type F
satisfying BoundedOrderHomClass F α β
into an actual
BoundedOrderHom
. This is declared as the default coercion from F
to BoundedOrderHom α β
.
Equations
- instCoeTCBoundedOrderHom = { coe := BoundedOrderHomClass.toBoundedOrderHom }
Top homomorphisms #
Equations
- TopHom.instTopHomClassTopHom = TopHomClass.mk (_ : ∀ (self : TopHom α β), TopHom.toFun self ⊤ = ⊤)
Equations
- TopHom.instPartialOrderTopHom = PartialOrder.lift (fun f => ↑f) (_ : Function.Injective fun f => ↑f)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Bot homomorphisms #
Equations
- BotHom.instBotHomClassBotHom = BotHomClass.mk (_ : ∀ (self : BotHom α β), BotHom.toFun self ⊥ = ⊥)
Equations
- BotHom.instPartialOrderBotHom = PartialOrder.lift (fun f => ↑f) (_ : Function.Injective fun f => ↑f)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Bounded order homomorphisms #
Reinterpret a BoundedOrderHom
as a TopHom
.
Equations
- BoundedOrderHom.toTopHom f = { toFun := ↑f.toOrderHom, map_top' := (_ : ↑f.toOrderHom ⊤ = ⊤) }
Reinterpret a BoundedOrderHom
as a BotHom
.
Equations
- BoundedOrderHom.toBotHom f = { toFun := ↑f.toOrderHom, map_bot' := (_ : ↑f.toOrderHom ⊥ = ⊥) }
Equations
- One or more equations did not get rendered due to their size.
Copy of a BoundedOrderHom
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Equations
- One or more equations did not get rendered due to their size.
id
as a BoundedOrderHom
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- BoundedOrderHom.instInhabitedBoundedOrderHom α = { default := BoundedOrderHom.id α }
Composition of BoundedOrderHom
s as a BoundedOrderHom
.
Equations
- One or more equations did not get rendered due to their size.
Dual homs #
Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual orders.
Equations
- One or more equations did not get rendered due to their size.