Esakia morphisms #

This file defines pseudo-epimorphisms and Esakia morphisms.

We use the DFunLike 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 #

PseudoEpimorphism: Pseudo-epimorphisms. Maps f such that f a ≤ b implies the existence of a' such that a ≤ a' and f a' = b.
EsakiaHom: Esakia morphisms. Continuous pseudo-epimorphisms.

Typeclasses #

References #

Wikipedia, Esakia space

source

structure PseudoEpimorphism (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] extends α →o β :

Type (max u_6 u_7)

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

toFun : α → β
monotone' : Monotone self.toFun
exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : self.toFun a ≤ b → ∃ (c : α), a ≤ c ∧ self.toFun c = b

Instances For

source

structure EsakiaHom (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] extends α →Co β :

Type (max u_6 u_7)

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

toFun : α → β
monotone' : Monotone self.toFun
continuous_toFun : Continuous self.toFun
exists_map_eq_of_map_le' ⦃a : α⦄ ⦃b : β⦄ : self.toFun a ≤ b → ∃ (c : α), a ≤ c ∧ self.toFun c = b

Instances For

source

class PseudoEpimorphismClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [Preorder α] [Preorder β] [FunLike F α β] extends RelHomClass F (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : β) => x1 ≤ x2 :

Prop

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

You should extend this class when you extend PseudoEpimorphism.

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

Instances

source

class EsakiaHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [FunLike F α β] extends ContinuousOrderHomClass F α β :

Prop

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

You should extend this class when you extend EsakiaHom.

map_continuous (f : F) : Continuous ⇑f
map_monotone (f : F) : Monotone ⇑f
exists_map_eq_of_map_le (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ (c : α), a ≤ c ∧ f c = b

Instances

source

@[instance 100]

instance PseudoEpimorphismClass.toTopHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [PartialOrder α] [OrderTop α] [Preorder β] [OrderTop β] [PseudoEpimorphismClass F α β] :

TopHomClass F α β

source

@[instance 100]

instance EsakiaHomClass.toPseudoEpimorphismClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [EsakiaHomClass F α β] :

PseudoEpimorphismClass F α β

source

instance instCoeTCPseudoEpimorphismOfPseudoEpimorphismClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Preorder β] [PseudoEpimorphismClass F α β] :

CoeTC F (PseudoEpimorphism α β)

Equations

source

instance instCoeTCEsakiaHomOfEsakiaHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [EsakiaHomClass F α β] :

CoeTC F (EsakiaHom α β)

Equations

source

@[instance 100]

instance OrderIsoClass.toPseudoEpimorphismClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [EquivLike F α β] [OrderIsoClass F α β] :

PseudoEpimorphismClass F α β

Pseudo-epimorphisms #

source

instance PseudoEpimorphism.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :

FunLike (PseudoEpimorphism α β) α β

Equations

source

instance PseudoEpimorphism.instPseudoEpimorphismClass {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :

PseudoEpimorphismClass (PseudoEpimorphism α β) α β

source

@[simp]

theorem PseudoEpimorphism.toOrderHom_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : PseudoEpimorphism α β) :

⇑f.toOrderHom = ⇑f

source

theorem PseudoEpimorphism.toFun_eq_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f : PseudoEpimorphism α β} :

f.toFun = ⇑f

source

theorem PseudoEpimorphism.ext {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : PseudoEpimorphism α β} (h : ∀ (a : α), f a = g a) :

f = g

source

theorem PseudoEpimorphism.ext_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {f g : PseudoEpimorphism α β} :

f = g ↔ ∀ (a : α), f a = g a

source

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

PseudoEpimorphism α β

Copy of a PseudoEpimorphism with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations

Instances For

source

@[simp]

theorem PseudoEpimorphism.coe_copy {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = ⇑f) :

⇑(f.copy f' h) = f'

source

theorem PseudoEpimorphism.copy_eq {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (f : PseudoEpimorphism α β) (f' : α → β) (h : f' = ⇑f) :

f.copy f' h = f

source

def PseudoEpimorphism.id (α : Type u_2) [Preorder α] :

PseudoEpimorphism α α

id as a PseudoEpimorphism.

Equations

Instances For

source

instance PseudoEpimorphism.instInhabited (α : Type u_2) [Preorder α] :

Inhabited (PseudoEpimorphism α α)

Equations

source

@[simp]

theorem PseudoEpimorphism.coe_id (α : Type u_2) [Preorder α] :

⇑(PseudoEpimorphism.id α) = id

source

@[simp]

theorem PseudoEpimorphism.coe_id_orderHom (α : Type u_2) [Preorder α] :

↑(PseudoEpimorphism.id α) = OrderHom.id

source

@[simp]

theorem PseudoEpimorphism.id_apply {α : Type u_2} [Preorder α] (a : α) :

(PseudoEpimorphism.id α) a = a

source

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

PseudoEpimorphism α γ

Composition of PseudoEpimorphisms as a PseudoEpimorphism.

Equations

Instances For

source

@[simp]

theorem PseudoEpimorphism.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :

⇑(g.comp f) = ⇑g ∘ ⇑f

source

@[simp]

theorem PseudoEpimorphism.coe_comp_orderHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :

↑(g.comp f) = (↑g).comp ↑f

source

@[simp]

theorem PseudoEpimorphism.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) (a : α) :

(g.comp f) a = g (f a)

source

@[simp]

theorem PseudoEpimorphism.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (h : PseudoEpimorphism γ δ) (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :

(h.comp g).comp f = h.comp (g.comp f)

source

@[simp]

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

f.comp (PseudoEpimorphism.id α) = f

source

@[simp]

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

(PseudoEpimorphism.id β).comp f = f

source

@[simp]

theorem PseudoEpimorphism.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] {g₁ g₂ : PseudoEpimorphism β γ} {f : PseudoEpimorphism α β} (hf : Function.Surjective ⇑f) :

g₁.comp f = g₂.comp f ↔ g₁ = g₂

source

@[simp]

theorem PseudoEpimorphism.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] {g : PseudoEpimorphism β γ} {f₁ f₂ : PseudoEpimorphism α β} (hg : Function.Injective ⇑g) :

g.comp f₁ = g.comp f₂ ↔ f₁ = f₂