Adjoining ⊤
and ⊥
to order maps and lattice homomorphisms #
This file defines ways to adjoin ⊤
or ⊥
or both to order maps (homomorphisms, embeddings and
isomorphisms) and lattice homomorphisms, and properties about the results.
Some definitions cause a possibly unbounded lattice homomorphism to become bounded, so they change the type of the homomorphism.
Taking the dual then adding ⊤
is the same as adding ⊥
then taking the dual.
This is the order iso form of WithTop.ofDual
, as proven by coe_toDualBotEquiv
.
Equations
Instances For
Embedding into WithTop α
.
Equations
- Function.Embedding.coeWithTop = { toFun := WithTop.some, inj' := ⋯ }
Instances For
The coercion α → WithTop α
bundled as monotone map.
Equations
- WithTop.coeOrderHom = { toFun := WithTop.some, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
Taking the dual then adding ⊥
is the same as adding ⊤
then taking the dual.
This is the order iso form of WithBot.ofDual
, as proven by coe_toDualTopEquiv
.
Equations
Instances For
Embedding into WithBot α
.
Equations
- Function.Embedding.coeWithBot = { toFun := WithBot.some, inj' := ⋯ }
Instances For
The coercion α → WithBot α
bundled as monotone map.
Equations
- WithBot.coeOrderHom = { toFun := WithBot.some, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
Lift an order homomorphism f : α →o β
to an order homomorphism WithBot α →o WithBot β
.
Equations
- f.withBotMap = { toFun := WithBot.map ⇑f, monotone' := ⋯ }
Instances For
Lift an order homomorphism f : α →o β
to an order homomorphism WithTop α →o WithTop β
.
Equations
- f.withTopMap = { toFun := WithTop.map ⇑f, monotone' := ⋯ }
Instances For
A version of WithBot.map
for order embeddings.
Equations
- f.withBotMap = { toEmbedding := f.optionMap, map_rel_iff' := ⋯ }
Instances For
A version of WithTop.map
for order embeddings.
Equations
- f.withTopMap = { toFun := WithTop.map ⇑f, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
Coercion α → WithBot α
as an OrderEmbedding
.
Equations
- OrderEmbedding.withBotCoe = { toFun := WithBot.some, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
Coercion α → WithTop α
as an OrderEmbedding
.
Equations
- OrderEmbedding.withTopCoe = { toFun := WithTop.some, inj' := ⋯, map_rel_iff' := ⋯ }
Instances For
A version of Equiv.optionCongr
for WithTop
.
Equations
- e.withTopCongr = { toEquiv := e.optionCongr, map_rel_iff' := ⋯ }
Instances For
A version of Equiv.optionCongr
for WithBot
.
Equations
- e.withBotCongr = { toEquiv := e.optionCongr, map_rel_iff' := ⋯ }
Instances For
Adjoins a ⊤
to the domain and codomain of a SupHom
.
Equations
- f.withTop = { toFun := WithTop.map ⇑f, map_sup' := ⋯ }
Instances For
Adjoins a ⊥
to the domain and codomain of a SupHom
.
Equations
- f.withBot = { toFun := Option.map ⇑f, map_sup' := ⋯, map_bot' := ⋯ }
Instances For
Adjoins a ⊤
to the codomain of a SupHom
.
Equations
- f.withTop' = { toFun := fun (a : WithTop α) => Option.elim a ⊤ ⇑f, map_sup' := ⋯ }
Instances For
Adjoins a ⊥
to the domain of a SupHom
.
Equations
- f.withBot' = { toFun := fun (a : WithBot α) => Option.elim a ⊥ ⇑f, map_sup' := ⋯, map_bot' := ⋯ }
Instances For
Adjoins a ⊤
to the domain and codomain of an InfHom
.
Equations
- f.withTop = { toFun := Option.map ⇑f, map_inf' := ⋯, map_top' := ⋯ }
Instances For
Adjoins a ⊥
to the domain and codomain of an InfHom
.
Equations
- f.withBot = { toFun := Option.map ⇑f, map_inf' := ⋯ }
Instances For
Adjoins a ⊤
to the codomain of an InfHom
.
Equations
- f.withTop' = { toFun := fun (a : WithTop α) => Option.elim a ⊤ ⇑f, map_inf' := ⋯, map_top' := ⋯ }
Instances For
Adjoins a ⊥
to the codomain of an InfHom
.
Equations
- f.withBot' = { toFun := fun (a : WithBot α) => Option.elim a ⊥ ⇑f, map_inf' := ⋯ }
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
.
Equations
- f.withTopWithBot = { toLatticeHom := f.withBot.withTop, map_top' := ⋯, map_bot' := ⋯ }
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
.
Equations
- f.withTopWithBot' = { toLatticeHom := f.withBot'.withTop', map_top' := ⋯, map_bot' := ⋯ }