Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat: port Topology.Order.Hom.Esakia #3108

Closed
wants to merge 15 commits into from
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2696,6 +2696,7 @@ import Mathlib.Topology.OmegaCompletePartialOrder
import Mathlib.Topology.Order
import Mathlib.Topology.Order.Basic
import Mathlib.Topology.Order.Hom.Basic
import Mathlib.Topology.Order.Hom.Esakia
import Mathlib.Topology.Order.Lattice
import Mathlib.Topology.Order.LowerTopology
import Mathlib.Topology.Order.Priestley
Expand Down
24 changes: 17 additions & 7 deletions Mathlib/Topology/Order/Hom/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -56,23 +56,33 @@ class ContinuousOrderHomClass (F : Type _) (α β : outParam <| Type _) [Preorde
map_monotone (f : F) : Monotone f
#align continuous_order_hom_class ContinuousOrderHomClass

end
-- Porting note: namespaced these results since there are more than 3 now
namespace ContinuousOrderHomClass

variable [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β]
[ContinuousOrderHomClass F α β]

-- See note [lower instance priority]
instance (priority := 100) ContinuousOrderHomClass.toOrderHomClass [Preorder α] [Preorder β]
[TopologicalSpace α] [TopologicalSpace β] [ContinuousOrderHomClass F α β] :
instance (priority := 100) toOrderHomClass :
OrderHomClass F α β :=
{ ‹ContinuousOrderHomClass F α β› with
map_rel := ContinuousOrderHomClass.map_monotone }
#align continuous_order_hom_class.to_continuous_map_class ContinuousOrderHomClass.toContinuousMapClass

instance [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β]
[ContinuousOrderHomClass F α β] : CoeTC F (α →Co β) :=
⟨fun f =>
-- Porting note: following `OrderHomClass.toOrderHom` design, introduced a wrapper
-- for the original coercion. The original one directly exposed
-- ContinuousOrderHom.mk which allowed simp to apply more eagerly than in all
-- the other results in `Topology.Order.Hom.Esakia`.
@[coe]
def toContinuousOrderHom (f : F) : α →Co β :=
{ toFun := f
monotone' := ContinuousOrderHomClass.map_monotone f
continuous_toFun := map_continuous f }⟩
continuous_toFun := map_continuous f }

instance : CoeTC F (α →Co β) :=
⟨toContinuousOrderHom⟩

end ContinuousOrderHomClass
/-! ### Top homomorphisms -/


Expand Down