Documentation

Mathlib.Topology.Order.Hom.Esakia

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 #

Typeclasses #

References #

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
Instances For
    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
    Instances For
      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 :

      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 bf a f b
      • exists_map_eq_of_map_le : ∀ (f : F) ⦃a : α⦄ ⦃b : β⦄, f a b∃ (c : α), a c f c = b
      Instances
        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 :

        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
          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 α β] :
          Equations
          • =
          instance instCoeTCPseudoEpimorphismOfPseudoEpimorphismClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [Preorder α] [Preorder β] [PseudoEpimorphismClass F α β] :
          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 α β] :
          Equations
          • =

          Pseudo-epimorphisms #

          instance PseudoEpimorphism.instFunLike {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
          Equations
          • PseudoEpimorphism.instFunLike = { coe := fun (f : PseudoEpimorphism α β) => f.toFun, coe_injective' := }
          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) :

          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' := }
          Instances For
            @[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

            id as a PseudoEpimorphism.

            Equations
            Instances For
              @[simp]
              theorem PseudoEpimorphism.coe_id (α : Type u_2) [Preorder α] :
              @[simp]
              theorem PseudoEpimorphism.coe_id_orderHom (α : Type u_2) [Preorder α] :
              (PseudoEpimorphism.id α) = OrderHom.id
              @[simp]
              theorem PseudoEpimorphism.id_apply {α : Type u_2} [Preorder α] (a : α) :
              def PseudoEpimorphism.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) :

              Composition of PseudoEpimorphisms as a PseudoEpimorphism.

              Equations
              • g.comp f = { toOrderHom := g.comp f.toOrderHom, exists_map_eq_of_map_le' := }
              Instances For
                @[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 #

                Equations
                • f.toPseudoEpimorphism = { toOrderHom := f.toOrderHom, exists_map_eq_of_map_le' := }
                Instances For
                  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 β] :
                  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' := }
                  Instances For
                    @[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
                    Instances For
                      Equations
                      @[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
                      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' := }
                      Instances For
                        @[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₂