mathlib3 documentation

topology.order.hom.esakia

Esakia morphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines pseudo-epimorphisms and Esakia morphisms.

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 #

Typeclasses #

References #

structure pseudo_epimorphism (α : Type u_6) (β : Type u_7) [preorder α] [preorder β] :
Type (max u_6 u_7)

The type of pseudo-epimorphisms, aka p-morphisms, aka bounded maps, from α to β.

Instances for pseudo_epimorphism
structure esakia_hom (α : Type u_6) (β : Type u_7) [topological_space α] [preorder α] [topological_space β] [preorder β] :
Type (max u_6 u_7)

The type of Esakia morphisms, aka continuous pseudo-epimorphisms, from α to β.

Instances for esakia_hom
@[class]
structure pseudo_epimorphism_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] :
Type (max u_6 u_7 u_8)

pseudo_epimorphism_class F α β states that F is a type of -preserving morphisms.

You should extend this class when you extend pseudo_epimorphism.

Instances of this typeclass
Instances of other typeclasses for pseudo_epimorphism_class
  • pseudo_epimorphism_class.has_sizeof_inst
@[class]
structure esakia_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [topological_space α] [preorder α] [topological_space β] [preorder β] :
Type (max u_6 u_7 u_8)

esakia_hom_class F α β states that F is a type of lattice morphisms.

You should extend this class when you extend esakia_hom.

Instances of this typeclass
Instances of other typeclasses for esakia_hom_class
  • esakia_hom_class.has_sizeof_inst
@[protected, instance]
def pseudo_epimorphism.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [pseudo_epimorphism_class F α β] :
Equations
@[protected, instance]
def esakia_hom.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] [esakia_hom_class F α β] :
Equations

Pseudo-epimorphisms #

@[protected, instance]
def pseudo_epimorphism.has_coe_to_fun {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :
has_coe_to_fun (pseudo_epimorphism α β) (λ (_x : pseudo_epimorphism α β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem pseudo_epimorphism.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f : pseudo_epimorphism α β} :
@[ext]
theorem pseudo_epimorphism.ext {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f g : pseudo_epimorphism α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def pseudo_epimorphism.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : pseudo_epimorphism α β) (f' : α β) (h : f' = f) :

Copy of a pseudo_epimorphism with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem pseudo_epimorphism.coe_copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : pseudo_epimorphism α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem pseudo_epimorphism.copy_eq {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : pseudo_epimorphism α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected, instance]
Equations
@[simp]
@[simp]
theorem pseudo_epimorphism.id_apply {α : Type u_2} [preorder α] (a : α) :
def pseudo_epimorphism.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) :

Composition of pseudo_epimorphisms as a pseudo_epimorphism.

Equations
@[simp]
theorem pseudo_epimorphism.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) :
(g.comp f) = g f
@[simp]
theorem pseudo_epimorphism.coe_comp_order_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) :
(g.comp f) = g.comp f
@[simp]
theorem pseudo_epimorphism.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) (a : α) :
(g.comp f) a = g (f a)
@[simp]
theorem pseudo_epimorphism.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [preorder α] [preorder β] [preorder γ] [preorder δ] (h : pseudo_epimorphism γ δ) (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) :
(h.comp g).comp f = h.comp (g.comp f)
@[simp]
theorem pseudo_epimorphism.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : pseudo_epimorphism α β) :
@[simp]
theorem pseudo_epimorphism.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : pseudo_epimorphism α β) :
theorem pseudo_epimorphism.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] {g₁ g₂ : pseudo_epimorphism β γ} {f : pseudo_epimorphism α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem pseudo_epimorphism.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] {g : pseudo_epimorphism β γ} {f₁ f₂ : pseudo_epimorphism α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂

Esakia morphisms #

@[protected, instance]
def esakia_hom.has_coe_to_fun {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] :
has_coe_to_fun (esakia_hom α β) (λ (_x : esakia_hom α β), α β)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[ext]
theorem esakia_hom.ext {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] {f g : esakia_hom α β} (h : (a : α), f a = g a) :
f = g
@[protected]
def esakia_hom.copy {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] (f : esakia_hom α β) (f' : α β) (h : f' = f) :

Copy of an esakia_hom with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
@[simp]
theorem esakia_hom.coe_copy {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] (f : esakia_hom α β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
theorem esakia_hom.copy_eq {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] (f : esakia_hom α β) (f' : α β) (h : f' = f) :
f.copy f' h = f
@[protected, instance]
Equations
@[simp]
theorem esakia_hom.coe_id (α : Type u_2) [topological_space α] [preorder α] :
@[simp]
theorem esakia_hom.id_apply {α : Type u_2} [topological_space α] [preorder α] (a : α) :
def esakia_hom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [preorder α] [topological_space β] [preorder β] [topological_space γ] [preorder γ] (g : esakia_hom β γ) (f : esakia_hom α β) :

Composition of esakia_homs as an esakia_hom.

Equations
@[simp]
theorem esakia_hom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [preorder α] [topological_space β] [preorder β] [topological_space γ] [preorder γ] (g : esakia_hom β γ) (f : esakia_hom α β) :
(g.comp f) = g f
@[simp]
theorem esakia_hom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [preorder α] [topological_space β] [preorder β] [topological_space γ] [preorder γ] (g : esakia_hom β γ) (f : esakia_hom α β) (a : α) :
(g.comp f) a = g (f a)
@[simp]
theorem esakia_hom.coe_comp_continuous_order_hom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [preorder α] [topological_space β] [preorder β] [topological_space γ] [preorder γ] (g : esakia_hom β γ) (f : esakia_hom α β) :
(g.comp f) = g.comp f
@[simp]
theorem esakia_hom.coe_comp_pseudo_epimorphism {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [preorder α] [topological_space β] [preorder β] [topological_space γ] [preorder γ] (g : esakia_hom β γ) (f : esakia_hom α β) :
(g.comp f) = g.comp f
@[simp]
theorem esakia_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 δ] (h : esakia_hom γ δ) (g : esakia_hom β γ) (f : esakia_hom α β) :
(h.comp g).comp f = h.comp (g.comp f)
@[simp]
theorem esakia_hom.comp_id {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] (f : esakia_hom α β) :
@[simp]
theorem esakia_hom.id_comp {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] (f : esakia_hom α β) :
theorem esakia_hom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [preorder α] [topological_space β] [preorder β] [topological_space γ] [preorder γ] {g₁ g₂ : esakia_hom β γ} {f : esakia_hom α β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem esakia_hom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [topological_space α] [preorder α] [topological_space β] [preorder β] [topological_space γ] [preorder γ] {g : esakia_hom β γ} {f₁ f₂ : esakia_hom α β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂