Documentation

Mathlib.Topology.Order.Hom.Basic

Continuous order homomorphisms #

This file defines continuous order homomorphisms, that is maps which are both continuous and monotone. They are also called Priestley homomorphisms because they are the morphisms of the category of Priestley spaces.

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 #

Typeclasses #

structure ContinuousOrderHom (α : Type u_6) (β : Type u_7) [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] extends OrderHom :
Type (max u_6 u_7)

The type of continuous monotone maps from α to β, aka Priestley homomorphisms.

Instances For
    theorem ContinuousOrderHom.continuous_toFun {α : Type u_6} {β : Type u_7} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] (self : α →Co β) :
    Continuous self.toFun
    class ContinuousOrderHomClass (F : Type u_6) (α : outParam (Type u_7)) (β : outParam (Type u_8)) [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] extends ContinuousMapClass :

    ContinuousOrderHomClass F α β states that F is a type of continuous monotone maps.

    You should extend this class when you extend ContinuousOrderHom.

    Instances
      theorem ContinuousOrderHomClass.map_monotone {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [self : ContinuousOrderHomClass F α β] (f : F) :
      @[instance 100]
      instance ContinuousOrderHomClass.toOrderHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousOrderHomClass F α β] :
      Equations
      • =
      def ContinuousOrderHomClass.toContinuousOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousOrderHomClass F α β] (f : F) :
      α →Co β

      Turn an element of a type F satisfying ContinuousOrderHomClass F α β into an actual ContinuousOrderHom. This is declared as the default coercion from F to α →Co β.

      Equations
      • f = { toFun := f, monotone' := , continuous_toFun := }
      Instances For
        instance ContinuousOrderHomClass.instCoeTCContinuousOrderHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β] [ContinuousOrderHomClass F α β] :
        CoeTC F (α →Co β)
        Equations
        • ContinuousOrderHomClass.instCoeTCContinuousOrderHom = { coe := ContinuousOrderHomClass.toContinuousOrderHom }

        Top homomorphisms #

        def ContinuousOrderHom.toContinuousMap {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) :
        C(α, β)

        Reinterpret a ContinuousOrderHom as a ContinuousMap.

        Equations
        • f.toContinuousMap = { toFun := f.toFun, continuous_toFun := }
        Instances For
          instance ContinuousOrderHom.instFunLike {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] :
          FunLike (α →Co β) α β
          Equations
          • ContinuousOrderHom.instFunLike = { coe := fun (f : α →Co β) => f.toFun, coe_injective' := }
          @[simp]
          theorem ContinuousOrderHom.coe_toOrderHom {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) :
          f.toOrderHom = f
          theorem ContinuousOrderHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] {f : α →Co β} :
          f.toFun = f
          theorem ContinuousOrderHom.ext {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] {f : α →Co β} {g : α →Co β} (h : ∀ (a : α), f a = g a) :
          f = g
          def ContinuousOrderHom.copy {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) (f' : αβ) (h : f' = f) :
          α →Co β

          Copy of a ContinuousOrderHom with a new ContinuousMap equal to the old one. Useful to fix definitional equalities.

          Equations
          • f.copy f' h = { toOrderHom := f.copy f' h, continuous_toFun := }
          Instances For
            @[simp]
            theorem ContinuousOrderHom.coe_copy {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) (f' : αβ) (h : f' = f) :
            (f.copy f' h) = f'
            theorem ContinuousOrderHom.copy_eq {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) (f' : αβ) (h : f' = f) :
            f.copy f' h = f
            def ContinuousOrderHom.id (α : Type u_2) [TopologicalSpace α] [Preorder α] :
            α →Co α

            id as a ContinuousOrderHom.

            Equations
            Instances For
              @[simp]
              @[simp]
              theorem ContinuousOrderHom.id_apply {α : Type u_2} [TopologicalSpace α] [Preorder α] (a : α) :
              def ContinuousOrderHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] (f : β →Co γ) (g : α →Co β) :
              α →Co γ

              Composition of ContinuousOrderHoms as a ContinuousOrderHom.

              Equations
              • f.comp g = { toOrderHom := f.comp g.toOrderHom, continuous_toFun := }
              Instances For
                @[simp]
                theorem ContinuousOrderHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] (f : β →Co γ) (g : α →Co β) :
                (f.comp g) = f g
                @[simp]
                theorem ContinuousOrderHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] (f : β →Co γ) (g : α →Co β) (a : α) :
                (f.comp g) a = f (g a)
                @[simp]
                theorem ContinuousOrderHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] [TopologicalSpace δ] [Preorder δ] (f : γ →Co δ) (g : β →Co γ) (h : α →Co β) :
                (f.comp g).comp h = f.comp (g.comp h)
                @[simp]
                theorem ContinuousOrderHom.comp_id {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) :
                f.comp (ContinuousOrderHom.id α) = f
                @[simp]
                theorem ContinuousOrderHom.id_comp {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] (f : α →Co β) :
                (ContinuousOrderHom.id β).comp f = f
                @[simp]
                theorem ContinuousOrderHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] {g₁ : β →Co γ} {g₂ : β →Co γ} {f : α →Co β} (hf : Function.Surjective f) :
                g₁.comp f = g₂.comp f g₁ = g₂
                @[simp]
                theorem ContinuousOrderHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] [TopologicalSpace γ] [Preorder γ] {g : β →Co γ} {f₁ : α →Co β} {f₂ : α →Co β} (hg : Function.Injective g) :
                g.comp f₁ = g.comp f₂ f₁ = f₂
                instance ContinuousOrderHom.instPreorder {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [Preorder α] [TopologicalSpace β] [Preorder β] :
                Preorder (α →Co β)
                Equations
                Equations