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

• PseudoEpimorphismClass
• EsakiaHomClass

References

• Wikipedia, Esakia space

structure PseudoEpimorphism (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] extends OrderHom : 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

theorem PseudoEpimorphism.exists_map_eq_of_map_le' {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] (self : PseudoEpimorphism α β) ⦃a : α⦄ ⦃b : β⦄ : self.toFun a ≤ b → ∃ (c : α), a ≤ c ∧ self.toFun c = b

structure EsakiaHom (α : Type u_6) (β : Type u_7) [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] extends ContinuousOrderHom : 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

theorem EsakiaHom.exists_map_eq_of_map_le' {α : Type u_6} {β : Type u_7} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (self : EsakiaHom α β) ⦃a : α⦄ ⦃b : β⦄ : self.toFun a ≤ b → ∃ (c : α), a ≤ c ∧ self.toFun c = b

class PseudoEpimorphismClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [Preorder α] [Preorder β] [FunLike F α β] extends RelHomClass : 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

theorem PseudoEpimorphismClass.exists_map_eq_of_map_le {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [Preorder α] [Preorder β] [FunLike F α β] [self : PseudoEpimorphismClass F α β] (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ (c : α), a ≤ c ∧ f c = b

class EsakiaHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [FunLike F α β] extends ContinuousOrderHomClass : 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

theorem EsakiaHomClass.exists_map_eq_of_map_le {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [FunLike F α β] [self : EsakiaHomClass F α β] (f : F) ⦃a : α⦄ ⦃b : β⦄ : f a ≤ b → ∃ (c : α), a ≤ c ∧ f c = b

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• instCoeTCPseudoEpimorphismOfPseudoEpimorphismClass = { coe := fun (f : F) => { toOrderHom := ↑f, exists_map_eq_of_map_le' := ⋯ } }

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

Equations

• instCoeTCEsakiaHomOfEsakiaHomClass = { coe := fun (f : F) => { toContinuousOrderHom := ↑f, exists_map_eq_of_map_le' := ⋯ } }

@[instance 100]

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

Equations

• ⋯ = ⋯

Pseudo-epimorphisms

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

Equations

• PseudoEpimorphism.instFunLike = { coe := fun (f : PseudoEpimorphism α β) => f.toFun, coe_injective' := ⋯ }

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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

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

• f.copy f' h = { toOrderHom := f.copy f' h, exists_map_eq_of_map_le' := ⋯ }

@[simp]

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

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

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

id as a PseudoEpimorphism.

Equations

• PseudoEpimorphism.id α = { toOrderHom := OrderHom.id, exists_map_eq_of_map_le' := ⋯ }

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

Equations

• PseudoEpimorphism.instInhabited α = { default := PseudoEpimorphism.id α }

@[simp]

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

@[simp]

theorem PseudoEpimorphism.coe_id_orderHom (α : Type u_2) [Preorder α] : ↑(PseudoEpimorphism.id α) = OrderHom.id

@[simp]

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

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

• g.comp f = { toOrderHom := g.comp f.toOrderHom, exists_map_eq_of_map_le' := ⋯ }

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Esakia morphisms

def EsakiaHom.toPseudoEpimorphism {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : EsakiaHom α β) : PseudoEpimorphism α β

Equations

• f.toPseudoEpimorphism = { toOrderHom := f.toOrderHom, exists_map_eq_of_map_le' := ⋯ }

instance EsakiaHom.instFunLike {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] : FunLike (EsakiaHom α β) α β

Equations

• EsakiaHom.instFunLike = { coe := fun (f : EsakiaHom α β) => f.toFun, coe_injective' := ⋯ }

instance EsakiaHom.instEsakiaHomClass {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] : EsakiaHomClass (EsakiaHom α β) α β

Equations

• ⋯ = ⋯

@[simp]

theorem EsakiaHom.toContinuousOrderHom_coe {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] {f : EsakiaHom α β} : ⇑f.toContinuousOrderHom = ⇑f

theorem EsakiaHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] {f : EsakiaHom α β} : f.toFun = ⇑f

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

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

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

Equations

• f.copy f' h = { toContinuousOrderHom := f.copy f' h, exists_map_eq_of_map_le' := ⋯ }

@[simp]

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

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

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

id as an EsakiaHom.

Equations

• EsakiaHom.id α = { toContinuousOrderHom := ContinuousOrderHom.id α, exists_map_eq_of_map_le' := ⋯ }

instance EsakiaHom.instInhabited (α : Type u_2) [TopologicalSpace α] [Preorder α] : Inhabited (EsakiaHom α α)

Equations

• EsakiaHom.instInhabited α = { default := EsakiaHom.id α }

@[simp]

theorem EsakiaHom.coe_id (α : Type u_2) [TopologicalSpace α] [Preorder α] : ⇑(EsakiaHom.id α) = id

@[simp]

theorem EsakiaHom.coe_id_pseudoEpimorphism (α : Type u_2) [TopologicalSpace α] [Preorder α] : { toOrderHom := ↑(EsakiaHom.id α), exists_map_eq_of_map_le' := ⋯ } = PseudoEpimorphism.id α

@[simp]

theorem EsakiaHom.id_apply {α : Type u_2} [TopologicalSpace α] [Preorder α] (a : α) : (EsakiaHom.id α) a = a

@[simp]

theorem EsakiaHom.coe_id_continuousOrderHom {α : Type u_2} [TopologicalSpace α] [Preorder α] : ↑(EsakiaHom.id α) = ContinuousOrderHom.id α

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

Composition of EsakiaHoms as an EsakiaHom.

Equations

• g.comp f = { toContinuousOrderHom := g.comp f.toContinuousOrderHom, exists_map_eq_of_map_le' := ⋯ }

@[simp]

theorem EsakiaHom.coe_comp_continuousOrderHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] (g : EsakiaHom β γ) (f : EsakiaHom α β) : ↑(g.comp f) = (↑g).comp ↑f

@[simp]

theorem EsakiaHom.coe_comp_pseudoEpimorphism {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] (g : EsakiaHom β γ) (f : EsakiaHom α β) : { toOrderHom := ↑(g.comp f), exists_map_eq_of_map_le' := ⋯ } = { toOrderHom := ↑g, exists_map_eq_of_map_le' := ⋯ }.comp { toOrderHom := ↑f, exists_map_eq_of_map_le' := ⋯ }

@[simp]

theorem EsakiaHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] (g : EsakiaHom β γ) (f : EsakiaHom α β) : ⇑(g.comp f) = ⇑g ∘ ⇑f

@[simp]

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

@[simp]

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

@[simp]

theorem EsakiaHom.comp_id {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : EsakiaHom α β) : f.comp (EsakiaHom.id α) = f

@[simp]

theorem EsakiaHom.id_comp {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : EsakiaHom α β) : (EsakiaHom.id β).comp f = f

@[simp]

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

@[simp]

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