Documentation

Mathlib.Order.Category.OmegaCompletePartialOrder

Category of types with an omega complete partial order #

In this file, we bundle the class OmegaCompletePartialOrder into a concrete category and prove that continuous functions also form an OmegaCompletePartialOrder.

Main definitions #

source
structure ωCPO :
Type (u + 1)

The category of types with an omega complete partial order.

Instances For
    source
    @[implicit_reducible]
    instance ωCPO.instCoeSortType :
    CoeSort ωCPO (Type u_1)
    source
    theorem ωCPO.coe_of (α : Type u_1) [OmegaCompletePartialOrder α] :
    { carrier := α, str := inst✝ }.carrier = α
    source
    @[implicit_reducible]
    instance ωCPO.instLargeCategory :
    CategoryTheory.LargeCategory ωCPO
    source
    @[implicit_reducible]
    instance ωCPO.instConcreteCategoryContinuousHomCarrier :
    CategoryTheory.ConcreteCategory ωCPO fun (x1 x2 : ωCPO) => x1.carrier →𝒄 x2.carrier
    source
    @[implicit_reducible]
    instance ωCPO.instInhabited :
    Inhabited ωCPO
    source
    def ωCPO.HasProducts.product {J : Type v} (f : J → ωCPO) :
    CategoryTheory.Limits.Fan f

    The pi-type gives a cone for a product.

    Instances For
      source
      def ωCPO.HasProducts.isProduct (J : Type v) (f : J → ωCPO) :
      CategoryTheory.Limits.IsLimit (product f)

      The pi-type is a limit cone for the product.

      Instances For
        source
        instance ωCPO.HasProducts.instHasProduct (J : Type v) (f : J → ωCPO) :
        CategoryTheory.Limits.HasProduct f
        source
        @[implicit_reducible]
        instance ωCPO.omegaCompletePartialOrderEqualizer {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f g : α →𝒄 β) :
        OmegaCompletePartialOrder { a : α // f a = g a }
        source
        def ωCPO.HasEqualizers.equalizerι {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f g : α →𝒄 β) :
        { a : α // f a = g a } →𝒄 α

        The equalizer inclusion function as a ContinuousHom.

        Instances For
          source
          def ωCPO.HasEqualizers.equalizer {X Y : ωCPO} (f g : X ⟶ Y) :
          CategoryTheory.Limits.Fork f g

          A construction of the equalizer fork.

          Instances For
            source
            def ωCPO.HasEqualizers.isEqualizer {X Y : ωCPO} (f g : X ⟶ Y) :
            CategoryTheory.Limits.IsLimit (equalizer f g)

            The equalizer fork is a limit.

            Instances For
              source
              instance ωCPO.instHasProducts :
              CategoryTheory.Limits.HasProducts ωCPO
              source
              instance ωCPO.instHasLimitWalkingParallelPairParallelPair {X Y : ωCPO} (f g : X ⟶ Y) :
              CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)
              source
              instance ωCPO.instHasEqualizers :
              CategoryTheory.Limits.HasEqualizers ωCPO
              source
              instance ωCPO.instHasLimits :
              CategoryTheory.Limits.HasLimits ωCPO