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
    instance ωCPO.instCoeSortType :
    CoeSort ωCPO (Type u_1)
    Equations
      source
      @[reducible, inline]
      abbrev ωCPO.of (α : Type u_1) [OmegaCompletePartialOrder α] :
      ωCPO

      Construct a bundled ωCPO from the underlying type and typeclass.

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

                The pi-type gives a cone for a product.

                Equations
                  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.

                    Equations
                      Instances For
                        source
                        instance ωCPO.HasProducts.instHasProduct (J : Type v) (f : J → ωCPO) :
                        CategoryTheory.Limits.HasProduct f
                        source
                        instance ωCPO.omegaCompletePartialOrderEqualizer {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f g : α →𝒄 β) :
                        OmegaCompletePartialOrder { a : α // f a = g a }
                        Equations
                          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.

                          Equations
                            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.

                              Equations
                                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.

                                  Equations
                                    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