Continuous order homomorphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines continuous order homomorphisms, that is maps which are both continuous and monotone. They are also called Priestley homomorphisms because they are the morphisms of the category of Priestley spaces.
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 #
continuous_order_hom: Continuous monotone functions, aka Priestley homomorphisms.
Typeclasses #
structure
continuous_order_hom
(α : Type u_6)
(β : Type u_7)
[preorder α]
[preorder β]
[topological_space α]
[topological_space β] :
Type (max u_6 u_7)
- to_order_hom : α →o β
- continuous_to_fun : continuous self.to_order_hom.to_fun
The type of continuous monotone maps from α to β, aka Priestley homomorphisms.
Instances for continuous_order_hom
@[instance]
def
continuous_order_hom_class.to_rel_hom_class
(F : Type u_6)
(α : out_param (Type u_7))
(β : out_param (Type u_8))
[preorder α]
[preorder β]
[topological_space α]
[topological_space β]
[self : continuous_order_hom_class F α β] :
@[class]
structure
continuous_order_hom_class
(F : Type u_6)
(α : out_param (Type u_7))
(β : out_param (Type u_8))
[preorder α]
[preorder β]
[topological_space α]
[topological_space β] :
Type (max u_6 u_7 u_8)
- coe : F → Π (a : α), (λ (_x : α), β) a
- coe_injective' : function.injective continuous_order_hom_class.coe
- map_rel : ∀ (f : F) {a b : α}, a ≤ b → ⇑f a ≤ ⇑f b
- map_continuous : ∀ (f : F), continuous ⇑f
continuous_order_hom_class F α β states that F is a type of continuous monotone maps.
You should extend this class when you extend continuous_order_hom.
Instances of this typeclass
Instances of other typeclasses for continuous_order_hom_class
- continuous_order_hom_class.has_sizeof_inst
@[protected, instance]
def
continuous_order_hom_class.to_continuous_map_class
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[topological_space α]
[topological_space β]
[continuous_order_hom_class F α β] :
continuous_map_class F α β
Equations
- continuous_order_hom_class.to_continuous_map_class = {coe := continuous_order_hom_class.coe _inst_5, coe_injective' := _, map_continuous := _}
@[protected, instance]
def
continuous_order_hom.has_coe_t
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[preorder α]
[preorder β]
[topological_space α]
[topological_space β]
[continuous_order_hom_class F α β] :
Equations
- continuous_order_hom.has_coe_t = {coe := λ (f : F), {to_order_hom := {to_fun := ⇑f, monotone' := _}, continuous_to_fun := _}}
Top homomorphisms #
def
continuous_order_hom.to_continuous_map
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
(f : α →Co β) :
Reinterpret a continuous_order_hom as a continuous_map.
Equations
- f.to_continuous_map = {to_fun := f.to_order_hom.to_fun, continuous_to_fun := _}
@[protected, instance]
def
continuous_order_hom.continuous_order_hom_class
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β] :
continuous_order_hom_class (α →Co β) α β
Equations
- continuous_order_hom.continuous_order_hom_class = {coe := λ (f : α →Co β), f.to_order_hom.to_fun, coe_injective' := _, map_rel := _, map_continuous := _}
@[protected, instance]
def
continuous_order_hom.has_coe_to_fun
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β] :
has_coe_to_fun (α →Co β) (λ (_x : α →Co β), α → β)
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
@[simp]
theorem
continuous_order_hom.to_fun_eq_coe
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
{f : α →Co β} :
f.to_order_hom.to_fun = ⇑f
@[ext]
theorem
continuous_order_hom.ext
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
{f g : α →Co β}
(h : ∀ (a : α), ⇑f a = ⇑g a) :
f = g
@[protected]
def
continuous_order_hom.copy
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
(f : α →Co β)
(f' : α → β)
(h : f' = ⇑f) :
α →Co β
Copy of a continuous_order_hom with a new continuous_map equal to the old one. Useful to fix
definitional equalities.
Equations
- f.copy f' h = {to_order_hom := f.to_order_hom.copy f' h, continuous_to_fun := _}
@[simp]
theorem
continuous_order_hom.coe_copy
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
(f : α →Co β)
(f' : α → β)
(h : f' = ⇑f) :
theorem
continuous_order_hom.copy_eq
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
(f : α →Co β)
(f' : α → β)
(h : f' = ⇑f) :
@[protected]
id as a continuous_order_hom.
Equations
- continuous_order_hom.id α = {to_order_hom := order_hom.id _inst_2, continuous_to_fun := _}
@[protected, instance]
Equations
- continuous_order_hom.inhabited α = {default := continuous_order_hom.id α _inst_2}
@[simp]
@[simp]
theorem
continuous_order_hom.id_apply
{α : Type u_2}
[topological_space α]
[preorder α]
(a : α) :
⇑(continuous_order_hom.id α) a = a
def
continuous_order_hom.comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
[topological_space γ]
[preorder γ]
(f : β →Co γ)
(g : α →Co β) :
α →Co γ
Composition of continuous_order_homs as a continuous_order_hom.
Equations
- f.comp g = {to_order_hom := f.to_order_hom.comp g.to_order_hom, continuous_to_fun := _}
@[simp]
theorem
continuous_order_hom.coe_comp
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
[topological_space γ]
[preorder γ]
(f : β →Co γ)
(g : α →Co β) :
@[simp]
theorem
continuous_order_hom.comp_apply
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
[topological_space γ]
[preorder γ]
(f : β →Co γ)
(g : α →Co β)
(a : α) :
@[simp]
theorem
continuous_order_hom.comp_assoc
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
{δ : Type u_5}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
[topological_space γ]
[preorder γ]
[topological_space δ]
[preorder δ]
(f : γ →Co δ)
(g : β →Co γ)
(h : α →Co β) :
@[simp]
theorem
continuous_order_hom.comp_id
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
(f : α →Co β) :
f.comp (continuous_order_hom.id α) = f
@[simp]
theorem
continuous_order_hom.id_comp
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
(f : α →Co β) :
(continuous_order_hom.id β).comp f = f
theorem
continuous_order_hom.cancel_right
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
[topological_space γ]
[preorder γ]
{g₁ g₂ : β →Co γ}
{f : α →Co β}
(hf : function.surjective ⇑f) :
theorem
continuous_order_hom.cancel_left
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β]
[topological_space γ]
[preorder γ]
{g : β →Co γ}
{f₁ f₂ : α →Co β}
(hg : function.injective ⇑g) :
@[protected, instance]
def
continuous_order_hom.preorder
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[preorder β] :
Equations
@[protected, instance]
def
continuous_order_hom.partial_order
{α : Type u_2}
{β : Type u_3}
[topological_space α]
[preorder α]
[topological_space β]
[partial_order β] :
partial_order (α →Co β)
Equations
- continuous_order_hom.partial_order = partial_order.lift coe_fn continuous_order_hom.partial_order._proof_1