topology.order.hom.esakia

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

Type (max u_6 u_7)

to_order_hom : α →o β
exists_map_eq_of_map_le' : ∀ ⦃a : α⦄ ⦃b : β⦄, self.to_order_hom.to_fun a ≤ b → (∃ (c : α), a ≤ c ∧ self.to_order_hom.to_fun c = b)

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

Instances for pseudo_epimorphism

pseudo_epimorphism.has_sizeof_inst
pseudo_epimorphism.has_coe_t
pseudo_epimorphism.pseudo_epimorphism_class
pseudo_epimorphism.has_coe_to_fun
pseudo_epimorphism.inhabited

structure esakia_hom (α : Type u_6) (β : Type u_7) [topological_space α] [preorder α] [topological_space β] [preorder β] :

Type (max u_6 u_7)

to_continuous_order_hom : α →Co β
exists_map_eq_of_map_le' : ∀ ⦃a : α⦄ ⦃b : β⦄, self.to_continuous_order_hom.to_order_hom.to_fun a ≤ b → (∃ (c : α), a ≤ c ∧ self.to_continuous_order_hom.to_order_hom.to_fun c = b)

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

Instances for esakia_hom

source

@[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)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective pseudo_epimorphism_class.coe
map_rel : ∀ (f : F) {a b : α}, a ≤ b → ⇑f a ≤ ⇑f b
exists_map_eq_of_map_le : ∀ (f : F) ⦃a : α⦄ ⦃b : β⦄, ⇑f a ≤ b → (∃ (c : α), a ≤ c ∧ ⇑f c = b)

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

source

@[instance]

def pseudo_epimorphism_class.to_rel_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [preorder α] [preorder β] [self : pseudo_epimorphism_class F α β] :

rel_hom_class F has_le.le has_le.le

source

@[instance]

def esakia_hom_class.to_continuous_order_hom_class (F : Type u_6) (α : out_param (Type u_7)) (β : out_param (Type u_8)) [topological_space α] [preorder α] [topological_space β] [preorder β] [self : esakia_hom_class F α β] :

continuous_order_hom_class F α β

source

@[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)

coe : F → Π (a : α), (λ (_x : α), β) a
coe_injective' : function.injective esakia_hom_class.coe
map_rel : ∀ (f : F) {a b : α}, a ≤ b → ⇑f a ≤ ⇑f b
map_continuous : ∀ (f : F), continuous ⇑f
exists_map_eq_of_map_le : ∀ (f : F) ⦃a : α⦄ ⦃b : β⦄, ⇑f a ≤ b → (∃ (c : α), a ≤ c ∧ ⇑f c = b)

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

esakia_hom.esakia_hom_class

Instances of other typeclasses for esakia_hom_class

esakia_hom_class.has_sizeof_inst

source

@[protected, instance]

def pseudo_epimorphism_class.to_top_hom_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [partial_order α] [order_top α] [preorder β] [order_top β] [pseudo_epimorphism_class F α β] :

top_hom_class F α β

Equations

pseudo_epimorphism_class.to_top_hom_class = {coe := pseudo_epimorphism_class.coe _inst_5, coe_injective' := _, map_top := _}

source

@[protected, instance]

def order_iso_class.to_pseudo_epimorphism_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [order_iso_class F α β] :

pseudo_epimorphism_class F α β

Equations

order_iso_class.to_pseudo_epimorphism_class = {coe := rel_hom_class.coe order_iso_class.to_order_hom_class, coe_injective' := _, map_rel := _, exists_map_eq_of_map_le := _}

source

@[protected, instance]

def esakia_hom_class.to_pseudo_epimorphism_class {F : Type u_1} {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] [esakia_hom_class F α β] :

pseudo_epimorphism_class F α β

Equations

esakia_hom_class.to_pseudo_epimorphism_class = {coe := esakia_hom_class.coe _inst_5, coe_injective' := _, map_rel := _, exists_map_eq_of_map_le := _}

source

@[protected, instance]

def pseudo_epimorphism.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] [pseudo_epimorphism_class F α β] :

has_coe_t F (pseudo_epimorphism α β)

Equations

pseudo_epimorphism.has_coe_t = {coe := λ (f : F), {to_order_hom := ↑f, exists_map_eq_of_map_le' := _}}

source

@[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 α β] :

has_coe_t F (esakia_hom α β)

Equations

esakia_hom.has_coe_t = {coe := λ (f : F), {to_continuous_order_hom := ↑f, exists_map_eq_of_map_le' := _}}

source

@[protected, instance]

def pseudo_epimorphism.pseudo_epimorphism_class {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] :

pseudo_epimorphism_class (pseudo_epimorphism α β) α β

Equations

pseudo_epimorphism.pseudo_epimorphism_class = {coe := λ (f : pseudo_epimorphism α β), f.to_order_hom.to_fun, coe_injective' := _, map_rel := _, exists_map_eq_of_map_le := _}

source

@[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

pseudo_epimorphism.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem pseudo_epimorphism.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {f : pseudo_epimorphism α β} :

f.to_order_hom.to_fun = ⇑f

source

@[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

source

@[protected]

def pseudo_epimorphism.copy {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : pseudo_epimorphism α β) (f' : α → β) (h : f' = ⇑f) :

pseudo_epimorphism α β

Copy of a pseudo_epimorphism with a new to_fun 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, exists_map_eq_of_map_le' := _}

source

@[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'

source

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

source

@[protected]

def pseudo_epimorphism.id (α : Type u_2) [preorder α] :

pseudo_epimorphism α α

id as a pseudo_epimorphism.

Equations

pseudo_epimorphism.id α = {to_order_hom := order_hom.id _inst_1, exists_map_eq_of_map_le' := _}

source

@[protected, instance]

def pseudo_epimorphism.inhabited (α : Type u_2) [preorder α] :

inhabited (pseudo_epimorphism α α)

Equations

pseudo_epimorphism.inhabited α = {default := pseudo_epimorphism.id α _inst_1}

source

@[simp]

theorem pseudo_epimorphism.coe_id (α : Type u_2) [preorder α] :

⇑(pseudo_epimorphism.id α) = id

source

@[simp]

theorem pseudo_epimorphism.coe_id_order_hom (α : Type u_2) [preorder α] :

↑(pseudo_epimorphism.id α) = order_hom.id

source

@[simp]

theorem pseudo_epimorphism.id_apply {α : Type u_2} [preorder α] (a : α) :

⇑(pseudo_epimorphism.id α) a = a

source

def pseudo_epimorphism.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [preorder α] [preorder β] [preorder γ] (g : pseudo_epimorphism β γ) (f : pseudo_epimorphism α β) :

pseudo_epimorphism α γ

Composition of pseudo_epimorphisms as a pseudo_epimorphism.

Equations

g.comp f = {to_order_hom := g.to_order_hom.comp f.to_order_hom, exists_map_eq_of_map_le' := _}

source

@[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

source

@[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

source

@[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)

source

@[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)

source

@[simp]

theorem pseudo_epimorphism.comp_id {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : pseudo_epimorphism α β) :

f.comp (pseudo_epimorphism.id α) = f

source

@[simp]

theorem pseudo_epimorphism.id_comp {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] (f : pseudo_epimorphism α β) :

(pseudo_epimorphism.id β).comp f = f

source

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₂

source

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₂

source

def esakia_hom.to_pseudo_epimorphism {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] (f : esakia_hom α β) :

pseudo_epimorphism α β

Reinterpret an esakia_hom as a pseudo_epimorphism.

Equations

f.to_pseudo_epimorphism = {to_order_hom := f.to_continuous_order_hom.to_order_hom, exists_map_eq_of_map_le' := _}

source

@[protected, instance]

def esakia_hom.esakia_hom_class {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] :

esakia_hom_class (esakia_hom α β) α β

Equations

esakia_hom.esakia_hom_class = {coe := λ (f : esakia_hom α β), f.to_continuous_order_hom.to_order_hom.to_fun, coe_injective' := _, map_rel := _, map_continuous := _, exists_map_eq_of_map_le := _}

source

@[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

esakia_hom.has_coe_to_fun = fun_like.has_coe_to_fun

source

@[simp]

theorem esakia_hom.to_fun_eq_coe {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] {f : esakia_hom α β} :

f.to_continuous_order_hom.to_order_hom.to_fun = ⇑f

source

@[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

source

@[protected]

def esakia_hom.copy {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] (f : esakia_hom α β) (f' : α → β) (h : f' = ⇑f) :

esakia_hom α β

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

Equations

f.copy f' h = {to_continuous_order_hom := f.to_continuous_order_hom.copy f' h, exists_map_eq_of_map_le' := _}

source

@[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'

source

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

source

@[protected]

def esakia_hom.id (α : Type u_2) [topological_space α] [preorder α] :

esakia_hom α α

id as an esakia_hom.

Equations

esakia_hom.id α = {to_continuous_order_hom := continuous_order_hom.id α _inst_2, exists_map_eq_of_map_le' := _}

source

@[protected, instance]

def esakia_hom.inhabited (α : Type u_2) [topological_space α] [preorder α] :

inhabited (esakia_hom α α)

Equations

esakia_hom.inhabited α = {default := esakia_hom.id α _inst_2}

source

@[simp]

theorem esakia_hom.coe_id (α : Type u_2) [topological_space α] [preorder α] :

⇑(esakia_hom.id α) = id

source

@[simp]

theorem esakia_hom.coe_id_continuous_order_hom (α : Type u_2) [topological_space α] [preorder α] :

↑(esakia_hom.id α) = continuous_order_hom.id α

source

@[simp]

theorem esakia_hom.coe_id_pseudo_epimorphism (α : Type u_2) [topological_space α] [preorder α] :

↑(esakia_hom.id α) = pseudo_epimorphism.id α

source

@[simp]

theorem esakia_hom.id_apply {α : Type u_2} [topological_space α] [preorder α] (a : α) :

⇑(esakia_hom.id α) a = a

source

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 α β) :

esakia_hom α γ

Composition of esakia_homs as an esakia_hom.

Equations

g.comp f = {to_continuous_order_hom := g.to_continuous_order_hom.comp f.to_continuous_order_hom, exists_map_eq_of_map_le' := _}

source

@[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

source

@[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)

source

@[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

source

@[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

source

@[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)

source

@[simp]

theorem esakia_hom.comp_id {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] (f : esakia_hom α β) :

f.comp (esakia_hom.id α) = f

source

@[simp]

theorem esakia_hom.id_comp {α : Type u_2} {β : Type u_3} [topological_space α] [preorder α] [topological_space β] [preorder β] (f : esakia_hom α β) :

(esakia_hom.id β).comp f = f

source

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₂

source

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₂

mathlib3 documentation

Esakia morphisms #

Types of morphisms #

Typeclasses #

References #

Pseudo-epimorphisms #

Esakia morphisms #