Bounded order homomorphisms #
This file defines (bounded) order homomorphisms.
We use the fun_like 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 #
top_hom: Maps which preserve⊤.bot_hom: Maps which preserve⊥.bounded_order_hom: Bounded order homomorphisms. Monotone maps which preserve⊤and⊥.
Typeclasses #
structure
bounded_order_hom
(α : Type u_6)
(β : Type u_7)
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β] :
Type (max u_6 u_7)
- to_order_hom : α →o β
- map_top' : self.to_order_hom.to_fun ⊤ = ⊤
- map_bot' : self.to_order_hom.to_fun ⊥ = ⊥
The type of bounded order homomorphisms from α to β.
@[class]
structure
top_hom_class
(F : Type u_6)
(α : out_param (Type u_7))
(β : out_param (Type u_8))
[has_top α]
[has_top β] :
Type (max u_6 u_7 u_8)
top_hom_class F α β states that F is a type of ⊤-preserving morphisms.
You should extend this class when you extend top_hom.
@[class]
structure
bot_hom_class
(F : Type u_6)
(α : out_param (Type u_7))
(β : out_param (Type u_8))
[has_bot α]
[has_bot β] :
Type (max u_6 u_7 u_8)
bot_hom_class F α β states that F is a type of ⊥-preserving morphisms.
You should extend this class when you extend bot_hom.
@[class]
structure
bounded_order_hom_class
(F : Type u_6)
(α : out_param (Type u_7))
(β : out_param (Type u_8))
[has_le α]
[has_le β]
[bounded_order α]
[bounded_order β] :
Type (max u_6 u_7 u_8)
- to_rel_hom_class : rel_hom_class F has_le.le has_le.le
- map_top : ∀ (f : F), ⇑f ⊤ = ⊤
- map_bot : ∀ (f : F), ⇑f ⊥ = ⊥
bounded_order_hom_class F α β states that F is a type of bounded order morphisms.
You should extend this class when you extend bounded_order_hom.
@[protected, instance]
def
bounded_order_hom_class.to_top_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[has_le α]
[has_le β]
[bounded_order α]
[bounded_order β]
[bounded_order_hom_class F α β] :
top_hom_class F α β
@[protected, instance]
def
bounded_order_hom_class.to_bot_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[has_le α]
[has_le β]
[bounded_order α]
[bounded_order β]
[bounded_order_hom_class F α β] :
bot_hom_class F α β
@[protected, instance]
def
order_iso_class.to_top_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[has_le α]
[order_top α]
[partial_order β]
[order_top β]
[order_iso_class F α β] :
top_hom_class F α β
@[protected, instance]
def
order_iso_class.to_bot_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[has_le α]
[order_bot α]
[partial_order β]
[order_bot β]
[order_iso_class F α β] :
bot_hom_class F α β
@[protected, instance]
def
order_iso_class.to_bounded_order_hom_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[has_le α]
[bounded_order α]
[partial_order β]
[bounded_order β]
[order_iso_class F α β] :
bounded_order_hom_class F α β
Equations
- order_iso_class.to_bounded_order_hom_class = {to_rel_hom_class := order_iso_class.to_order_hom_class _inst_5, map_top := _, map_bot := _}
@[simp]
theorem
map_eq_top_iff
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[has_le α]
[order_top α]
[partial_order β]
[order_top β]
[order_iso_class F α β]
(f : F)
{a : α} :
@[simp]
theorem
map_eq_bot_iff
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[has_le α]
[order_bot α]
[partial_order β]
[order_bot β]
[order_iso_class F α β]
(f : F)
{a : α} :
@[protected, instance]
def
top_hom.has_coe_t
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[has_top α]
[has_top β]
[top_hom_class F α β] :
@[protected, instance]
def
bot_hom.has_coe_t
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[has_bot α]
[has_bot β]
[bot_hom_class F α β] :
@[protected, instance]
def
bounded_order_hom.has_coe_t
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β]
[bounded_order_hom_class F α β] :
has_coe_t F (bounded_order_hom α β)
Top homomorphisms #
@[protected, instance]
def
top_hom.top_hom_class
{α : Type u_2}
{β : Type u_3}
[has_top α]
[has_top β] :
top_hom_class (top_hom α β) α β
Equations
- top_hom.top_hom_class = {to_fun_like := {coe := top_hom.to_fun _inst_2, coe_injective' := _}, map_top := _}
@[protected, instance]
def
top_hom.has_coe_to_fun
{α : Type u_2}
{β : Type u_3}
[has_top α]
[has_top β] :
has_coe_to_fun (top_hom α β) (λ (_x : top_hom α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
@[simp]
theorem
top_hom.comp_id
{α : Type u_2}
{β : Type u_3}
[has_top α]
[has_top β]
(f : top_hom α β) :
f.comp (top_hom.id α) = f
@[simp]
theorem
top_hom.id_comp
{α : Type u_2}
{β : Type u_3}
[has_top α]
[has_top β]
(f : top_hom α β) :
(top_hom.id β).comp f = f
@[protected, instance]
Equations
@[protected, instance]
def
top_hom.partial_order
{α : Type u_2}
{β : Type u_3}
[has_top α]
[partial_order β]
[has_top β] :
partial_order (top_hom α β)
Equations
- top_hom.partial_order = partial_order.lift coe_fn top_hom.partial_order._proof_1
@[protected, instance]
def
top_hom.semilattice_inf
{α : Type u_2}
{β : Type u_3}
[has_top α]
[semilattice_inf β]
[order_top β] :
semilattice_inf (top_hom α β)
Equations
- top_hom.semilattice_inf = function.injective.semilattice_inf coe_fn top_hom.semilattice_inf._proof_1 top_hom.semilattice_inf._proof_2
@[protected, instance]
def
top_hom.semilattice_sup
{α : Type u_2}
{β : Type u_3}
[has_top α]
[semilattice_sup β]
[order_top β] :
semilattice_sup (top_hom α β)
Equations
- top_hom.semilattice_sup = function.injective.semilattice_sup coe_fn top_hom.semilattice_sup._proof_1 top_hom.semilattice_sup._proof_2
@[protected, instance]
Equations
- top_hom.lattice = function.injective.lattice coe_fn top_hom.lattice._proof_1 top_hom.lattice._proof_2 top_hom.lattice._proof_3
@[protected, instance]
def
top_hom.distrib_lattice
{α : Type u_2}
{β : Type u_3}
[has_top α]
[distrib_lattice β]
[order_top β] :
distrib_lattice (top_hom α β)
Equations
- top_hom.distrib_lattice = function.injective.distrib_lattice coe_fn top_hom.distrib_lattice._proof_1 top_hom.distrib_lattice._proof_2 top_hom.distrib_lattice._proof_3
Bot homomorphisms #
@[protected, instance]
def
bot_hom.bot_hom_class
{α : Type u_2}
{β : Type u_3}
[has_bot α]
[has_bot β] :
bot_hom_class (bot_hom α β) α β
Equations
- bot_hom.bot_hom_class = {to_fun_like := {coe := bot_hom.to_fun _inst_2, coe_injective' := _}, map_bot := _}
@[protected, instance]
def
bot_hom.has_coe_to_fun
{α : Type u_2}
{β : Type u_3}
[has_bot α]
[has_bot β] :
has_coe_to_fun (bot_hom α β) (λ (_x : bot_hom α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
@[simp]
theorem
bot_hom.comp_id
{α : Type u_2}
{β : Type u_3}
[has_bot α]
[has_bot β]
(f : bot_hom α β) :
f.comp (bot_hom.id α) = f
@[simp]
theorem
bot_hom.id_comp
{α : Type u_2}
{β : Type u_3}
[has_bot α]
[has_bot β]
(f : bot_hom α β) :
(bot_hom.id β).comp f = f
@[protected, instance]
Equations
@[protected, instance]
def
bot_hom.partial_order
{α : Type u_2}
{β : Type u_3}
[has_bot α]
[partial_order β]
[has_bot β] :
partial_order (bot_hom α β)
Equations
- bot_hom.partial_order = partial_order.lift coe_fn bot_hom.partial_order._proof_1
@[protected, instance]
def
bot_hom.semilattice_inf
{α : Type u_2}
{β : Type u_3}
[has_bot α]
[semilattice_inf β]
[order_bot β] :
semilattice_inf (bot_hom α β)
Equations
- bot_hom.semilattice_inf = function.injective.semilattice_inf coe_fn bot_hom.semilattice_inf._proof_1 bot_hom.semilattice_inf._proof_2
@[protected, instance]
def
bot_hom.semilattice_sup
{α : Type u_2}
{β : Type u_3}
[has_bot α]
[semilattice_sup β]
[order_bot β] :
semilattice_sup (bot_hom α β)
Equations
- bot_hom.semilattice_sup = function.injective.semilattice_sup coe_fn bot_hom.semilattice_sup._proof_1 bot_hom.semilattice_sup._proof_2
@[protected, instance]
Equations
- bot_hom.lattice = function.injective.lattice coe_fn bot_hom.lattice._proof_1 bot_hom.lattice._proof_2 bot_hom.lattice._proof_3
@[protected, instance]
def
bot_hom.distrib_lattice
{α : Type u_2}
{β : Type u_3}
[has_bot α]
[distrib_lattice β]
[order_bot β] :
distrib_lattice (bot_hom α β)
Equations
- bot_hom.distrib_lattice = function.injective.distrib_lattice coe_fn bot_hom.distrib_lattice._proof_1 bot_hom.distrib_lattice._proof_2 bot_hom.distrib_lattice._proof_3
Bounded order homomorphisms #
def
bounded_order_hom.to_top_hom
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β]
(f : bounded_order_hom α β) :
top_hom α β
Reinterpret a bounded_order_hom as a top_hom.
Equations
- f.to_top_hom = {to_fun := f.to_order_hom.to_fun, map_top' := _}
def
bounded_order_hom.to_bot_hom
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β]
(f : bounded_order_hom α β) :
bot_hom α β
Reinterpret a bounded_order_hom as a bot_hom.
Equations
- f.to_bot_hom = {to_fun := f.to_order_hom.to_fun, map_bot' := _}
@[protected, instance]
def
bounded_order_hom.bounded_order_hom_class
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β] :
bounded_order_hom_class (bounded_order_hom α β) α β
Equations
- bounded_order_hom.bounded_order_hom_class = {to_rel_hom_class := {to_fun_like := {coe := λ (f : bounded_order_hom α β), f.to_order_hom.to_fun, coe_injective' := _}, map_rel := _}, map_top := _, map_bot := _}
@[protected, instance]
def
bounded_order_hom.has_coe_to_fun
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β] :
has_coe_to_fun (bounded_order_hom α β) (λ (_x : bounded_order_hom α β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[simp]
theorem
bounded_order_hom.to_fun_eq_coe
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β]
{f : bounded_order_hom α β} :
f.to_order_hom.to_fun = ⇑f
@[ext]
theorem
bounded_order_hom.ext
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β]
{f g : bounded_order_hom α β}
(h : ∀ (a : α), ⇑f a = ⇑g a) :
f = g
@[protected]
def
bounded_order_hom.copy
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β]
(f : bounded_order_hom α β)
(f' : α → β)
(h : f' = ⇑f) :
Copy of a bounded_order_hom with a new to_fun equal to the old one. Useful to fix
definitional equalities.
@[protected]
id as a bounded_order_hom.
Equations
- bounded_order_hom.id α = {to_order_hom := {to_fun := order_hom.id.to_fun, monotone' := _}, map_top' := _, map_bot' := _}
@[protected, instance]
def
bounded_order_hom.inhabited
(α : Type u_2)
[preorder α]
[bounded_order α] :
inhabited (bounded_order_hom α α)
Equations
- bounded_order_hom.inhabited α = {default := bounded_order_hom.id α _inst_5}
@[simp]
theorem
bounded_order_hom.coe_id
(α : Type u_2)
[preorder α]
[bounded_order α] :
⇑(bounded_order_hom.id α) = id
@[simp]
theorem
bounded_order_hom.id_apply
{α : Type u_2}
[preorder α]
[bounded_order α]
(a : α) :
⇑(bounded_order_hom.id α) a = a
def
bounded_order_hom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[preorder β]
[preorder γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_order_hom β γ)
(g : bounded_order_hom α β) :
Composition of bounded_order_homs as a bounded_order_hom.
Equations
- f.comp g = {to_order_hom := {to_fun := (f.to_order_hom.comp g.to_order_hom).to_fun, monotone' := _}, map_top' := _, map_bot' := _}
@[simp]
theorem
bounded_order_hom.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[preorder β]
[preorder γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_order_hom β γ)
(g : bounded_order_hom α β) :
@[simp]
theorem
bounded_order_hom.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[preorder β]
[preorder γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_order_hom β γ)
(g : bounded_order_hom α β)
(a : α) :
@[simp]
theorem
bounded_order_hom.coe_comp_order_hom
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[preorder β]
[preorder γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_order_hom β γ)
(g : bounded_order_hom α β) :
@[simp]
theorem
bounded_order_hom.coe_comp_top_hom
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[preorder β]
[preorder γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_order_hom β γ)
(g : bounded_order_hom α β) :
@[simp]
theorem
bounded_order_hom.coe_comp_bot_hom
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[preorder β]
[preorder γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
(f : bounded_order_hom β γ)
(g : bounded_order_hom α β) :
@[simp]
theorem
bounded_order_hom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[preorder α]
[preorder β]
[preorder γ]
[preorder δ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
[bounded_order δ]
(f : bounded_order_hom γ δ)
(g : bounded_order_hom β γ)
(h : bounded_order_hom α β) :
@[simp]
theorem
bounded_order_hom.comp_id
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β]
(f : bounded_order_hom α β) :
f.comp (bounded_order_hom.id α) = f
@[simp]
theorem
bounded_order_hom.id_comp
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[bounded_order α]
[bounded_order β]
(f : bounded_order_hom α β) :
(bounded_order_hom.id β).comp f = f
theorem
bounded_order_hom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[preorder β]
[preorder γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
{g₁ g₂ : bounded_order_hom β γ}
{f : bounded_order_hom α β}
(hf : function.surjective ⇑f) :
theorem
bounded_order_hom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[preorder β]
[preorder γ]
[bounded_order α]
[bounded_order β]
[bounded_order γ]
{g : bounded_order_hom β γ}
{f₁ f₂ : bounded_order_hom α β}
(hg : function.injective ⇑g) :
Dual homs #
@[simp]
theorem
top_hom.dual_symm_apply_to_fun
{α : Type u_2}
{β : Type u_3}
[has_le α]
[order_top α]
[has_le β]
[order_top β]
(f : bot_hom (order_dual α) (order_dual β))
(ᾰ : order_dual α) :
@[protected]
def
top_hom.dual
{α : Type u_2}
{β : Type u_3}
[has_le α]
[order_top α]
[has_le β]
[order_top β] :
top_hom α β ≃ bot_hom (order_dual α) (order_dual β)
Reinterpret a top homomorphism as a bot homomorphism between the dual lattices.
@[simp]
theorem
top_hom.dual_id
{α : Type u_2}
[has_le α]
[order_top α] :
⇑top_hom.dual (top_hom.id α) = bot_hom.id (order_dual α)
@[simp]
theorem
top_hom.dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_le α]
[order_top α]
[has_le β]
[order_top β]
[has_le γ]
[order_top γ]
(g : top_hom β γ)
(f : top_hom α β) :
⇑top_hom.dual (g.comp f) = (⇑top_hom.dual g).comp (⇑top_hom.dual f)
@[simp]
theorem
top_hom.symm_dual_id
{α : Type u_2}
[has_le α]
[order_top α] :
⇑(top_hom.dual.symm) (bot_hom.id (order_dual α)) = top_hom.id α
@[simp]
theorem
top_hom.symm_dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_le α]
[order_top α]
[has_le β]
[order_top β]
[has_le γ]
[order_top γ]
(g : bot_hom (order_dual β) (order_dual γ))
(f : bot_hom (order_dual α) (order_dual β)) :
⇑(top_hom.dual.symm) (g.comp f) = (⇑(top_hom.dual.symm) g).comp (⇑(top_hom.dual.symm) f)
@[simp]
theorem
bot_hom.dual_symm_apply_to_fun
{α : Type u_2}
{β : Type u_3}
[has_le α]
[order_bot α]
[has_le β]
[order_bot β]
(f : top_hom (order_dual α) (order_dual β))
(ᾰ : order_dual α) :
@[protected]
def
bot_hom.dual
{α : Type u_2}
{β : Type u_3}
[has_le α]
[order_bot α]
[has_le β]
[order_bot β] :
bot_hom α β ≃ top_hom (order_dual α) (order_dual β)
Reinterpret a bot homomorphism as a top homomorphism between the dual lattices.
@[simp]
theorem
bot_hom.dual_id
{α : Type u_2}
[has_le α]
[order_bot α] :
⇑bot_hom.dual (bot_hom.id α) = top_hom.id (order_dual α)
@[simp]
theorem
bot_hom.dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_le α]
[order_bot α]
[has_le β]
[order_bot β]
[has_le γ]
[order_bot γ]
(g : bot_hom β γ)
(f : bot_hom α β) :
⇑bot_hom.dual (g.comp f) = (⇑bot_hom.dual g).comp (⇑bot_hom.dual f)
@[simp]
theorem
bot_hom.symm_dual_id
{α : Type u_2}
[has_le α]
[order_bot α] :
⇑(bot_hom.dual.symm) (top_hom.id (order_dual α)) = bot_hom.id α
@[simp]
theorem
bot_hom.symm_dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[has_le α]
[order_bot α]
[has_le β]
[order_bot β]
[has_le γ]
[order_bot γ]
(g : top_hom (order_dual β) (order_dual γ))
(f : top_hom (order_dual α) (order_dual β)) :
⇑(bot_hom.dual.symm) (g.comp f) = (⇑(bot_hom.dual.symm) g).comp (⇑(bot_hom.dual.symm) f)
@[simp]
theorem
bounded_order_hom.dual_apply_to_order_hom
{α : Type u_2}
{β : Type u_3}
[preorder α]
[bounded_order α]
[preorder β]
[bounded_order β]
(f : bounded_order_hom α β) :
@[protected]
def
bounded_order_hom.dual
{α : Type u_2}
{β : Type u_3}
[preorder α]
[bounded_order α]
[preorder β]
[bounded_order β] :
bounded_order_hom α β ≃ bounded_order_hom (order_dual α) (order_dual β)
Reinterpret a bounded order homomorphism as a bounded order homomorphism between the dual orders.
Equations
- bounded_order_hom.dual = {to_fun := λ (f : bounded_order_hom α β), {to_order_hom := ⇑order_hom.dual f.to_order_hom, map_top' := _, map_bot' := _}, inv_fun := λ (f : bounded_order_hom (order_dual α) (order_dual β)), {to_order_hom := ⇑(order_hom.dual.symm) f.to_order_hom, map_top' := _, map_bot' := _}, left_inv := _, right_inv := _}
@[simp]
theorem
bounded_order_hom.dual_symm_apply_to_order_hom
{α : Type u_2}
{β : Type u_3}
[preorder α]
[bounded_order α]
[preorder β]
[bounded_order β]
(f : bounded_order_hom (order_dual α) (order_dual β)) :
@[simp]
@[simp]
theorem
bounded_order_hom.dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[bounded_order α]
[preorder β]
[bounded_order β]
[preorder γ]
[bounded_order γ]
(g : bounded_order_hom β γ)
(f : bounded_order_hom α β) :
@[simp]
@[simp]
theorem
bounded_order_hom.symm_dual_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[preorder α]
[bounded_order α]
[preorder β]
[bounded_order β]
[preorder γ]
[bounded_order γ]
(g : bounded_order_hom (order_dual β) (order_dual γ))
(f : bounded_order_hom (order_dual α) (order_dual β)) :
⇑(bounded_order_hom.dual.symm) (g.comp f) = (⇑(bounded_order_hom.dual.symm) g).comp (⇑(bounded_order_hom.dual.symm) f)