Documentation

Mathlib.CategoryTheory.Limits.Shapes.Types

Special shapes for limits in Type. #

The general shape (co)limits defined in CategoryTheory.Limits.Types are intended for use through the limits API, and the actual implementation should mostly be considered "sealed".

In this file, we provide definitions of the "standard" special shapes of limits in Type, giving the expected definitional implementation:

We first construct terms of IsLimit and LimitCone, and then provide isomorphisms with the types generated by the HasLimit API.

As an example, when setting up the monoidal category structure on Type we use the Types.terminalLimitCone and Types.binaryProductLimitCone definitions.

@[simp]
theorem CategoryTheory.Limits.Types.pi_lift_π_apply {β : Type v} [Small.{u, v} β] (f : βType u) {P : Type u} (s : (b : β) → P f b) (b : β) (x : P) :

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift.

theorem CategoryTheory.Limits.Types.pi_lift_π_apply' {β : Type v} (f : βType v) {P : Type v} (s : (b : β) → P f b) (b : β) (x : P) :

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift, with specialized universes.

@[simp]
theorem CategoryTheory.Limits.Types.pi_map_π_apply {β : Type v} [Small.{u, v} β] {f : βType u} {g : βType u} (α : (j : β) → f j g j) (b : β) (x : ∏ᶜ f) :

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map.

theorem CategoryTheory.Limits.Types.pi_map_π_apply' {β : Type v} {f : βType v} {g : βType v} (α : (j : β) → f j g j) (b : β) (x : ∏ᶜ f) :

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map, with specialized universes.

The category of types has PUnit as a terminal object.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The terminal object in Type u is PUnit.

    Equations
    Instances For

      A type is terminal if and only if it contains exactly one element.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        A type is terminal if and only if it is isomorphic to PUnit.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The category of types has PEmpty as an initial object.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            The initial object in Type u is PEmpty.

            Equations
            Instances For

              An object in Type u is initial if and only if it is empty.

              The product type X × Y forms a cone for the binary product of X and Y.

              Equations
              Instances For

                The product type X × Y is a binary product for X and Y.

                Equations
                Instances For

                  The category of types has X × Y, the usual cartesian product, as the binary product of X and Y.

                  Equations
                  Instances For
                    noncomputable def CategoryTheory.Limits.Types.binaryProductIso (X : Type u) (Y : Type u) :
                    X Y X × Y

                    The categorical binary product in Type u is cartesian product.

                    Equations
                    Instances For

                      The functor which sends X, Y to the product type X × Y.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        The product functor given by the instance HasBinaryProducts (Type u) is isomorphic to the explicit binary product functor given by the product type.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The sum type X ⊕ Y forms a cocone for the binary coproduct of X and Y.

                          Equations
                          Instances For

                            The sum type X ⊕ Y is a binary coproduct for X and Y.

                            Equations
                            Instances For

                              The category of types has X ⊕ Y, as the binary coproduct of X and Y.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                Any monomorphism in Type is a coproduct injection.

                                Equations
                                Instances For

                                  The category of types has Π j, f j as the product of a type family f : J → TypeMax.{v, u}.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    noncomputable def CategoryTheory.Limits.Types.productIso {J : Type v} (F : JTypeMax) :
                                    ∏ᶜ F (j : J) → F j

                                    The categorical product in TypeMax.{v, u} is the type theoretic product Π j, F j.

                                    Equations
                                    Instances For

                                      A variant of productLimitCone using a Small hypothesis rather than a function to TypeMax.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        noncomputable def CategoryTheory.Limits.Types.Small.productIso {J : Type v} (F : JType u) [Small.{u, v} J] :
                                        ∏ᶜ F Shrink.{u, max u v} ((j : J) → F j)

                                        The categorical product in Type u indexed in Type v is the type theoretic product Π j, F j, after shrinking back to Type u.

                                        Equations
                                        Instances For
                                          @[simp]

                                          The category of types has Σ j, f j as the coproduct of a type family f : J → Type.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            noncomputable def CategoryTheory.Limits.Types.coproductIso {J : Type v} (F : JTypeMax) :
                                            F (j : J) × F j

                                            The categorical coproduct in Type u is the type theoretic coproduct Σ j, F j.

                                            Equations
                                            Instances For
                                              noncomputable def CategoryTheory.Limits.Types.typeEqualizerOfUnique {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) {g : Y Z} {h : Y Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) (t : ∀ (y : Y), g y = h y∃! x : X, f x = y) :

                                              Show the given fork in Type u is an equalizer given that any element in the "difference kernel" comes from X. The converse of unique_of_type_equalizer.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem CategoryTheory.Limits.Types.unique_of_type_equalizer {X : Type u} {Y : Type u} {Z : Type u} (f : X Y) {g : Y Z} {h : Y Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) (y : Y) (hy : g y = h y) :
                                                ∃! x : X, f x = y

                                                The converse of type_equalizer_of_unique.

                                                Show that the subtype {x : Y // g x = h x} is an equalizer for the pair (g,h).

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  noncomputable def CategoryTheory.Limits.Types.equalizerIso {Y : Type u} {Z : Type u} (g : Y Z) (h : Y Z) :
                                                  CategoryTheory.Limits.equalizer g h { x : Y // g x = h x }

                                                  The categorical equalizer in Type u is {x : Y // g x = h x}.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_apply {Y : Type u} {Z : Type u} (g : Y Z) (h : Y Z) (x : { x : Y // g x = h x }) :
                                                    inductive CategoryTheory.Limits.Types.CoequalizerRel {X : Type u} {Y : Type u} (f : X Y) (g : X Y) :
                                                    YYProp

                                                    (Implementation) The relation to be quotiented to obtain the coequalizer.

                                                    Instances For

                                                      Show that the quotient by the relation generated by f(x) ~ g(x) is a coequalizer for the pair (f, g).

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        If π : Y ⟶ Z is an equalizer for (f, g), and U ⊆ Y such that f ⁻¹' U = g ⁻¹' U, then π ⁻¹' (π '' U) = U.

                                                        @[reducible, inline]
                                                        abbrev CategoryTheory.Limits.Types.PullbackObj {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :

                                                        The usual explicit pullback in the category of types, as a subtype of the product. The full LimitCone data is bundled as pullbackLimitCone f g.

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]
                                                          abbrev CategoryTheory.Limits.Types.pullbackCone {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :

                                                          The explicit pullback cone on PullbackObj f g. This is bundled with the IsLimit data as pullbackLimitCone f g.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[simp]
                                                            theorem CategoryTheory.Limits.Types.pullbackLimitCone_isLimit {X : Type u} {Y : Type u} {Z : Type u} (f : X Z) (g : Y Z) :
                                                            (CategoryTheory.Limits.Types.pullbackLimitCone f g).isLimit = (CategoryTheory.Limits.Types.pullbackCone f g).isLimitAux (fun (s : CategoryTheory.Limits.PullbackCone f g) (x : s.pt) => (s.fst x, s.snd x), )

                                                            The explicit pullback in the category of types, bundled up as a LimitCone for given f and g.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For

                                                              A limit pullback cone in the category of types identifies to the explicit pullback.

                                                              Equations
                                                              Instances For
                                                                theorem CategoryTheory.Limits.PullbackCone.IsLimit.type_ext {X : Type v} {Y : Type v} {S : Type v} {f : X S} {g : Y S} {c : CategoryTheory.Limits.PullbackCone f g} (hc : CategoryTheory.Limits.IsLimit c) {x : c.pt} {y : c.pt} (h₁ : c.fst x = c.fst y) (h₂ : c.snd x = c.snd y) :
                                                                x = y

                                                                The pullback given by the instance HasPullbacks (Type u) is isomorphic to the explicit pullback object given by PullbackObj.

                                                                Equations
                                                                Instances For
                                                                  inductive CategoryTheory.Limits.Types.Pushout.Rel {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :
                                                                  X₁ X₂X₁ X₂Prop

                                                                  The pushout of two maps f : S ⟶ X₁ and g : S ⟶ X₂ is the quotient by the equivalence relation on X₁ ⊕ X₂ generated by this relation.

                                                                  Instances For
                                                                    def CategoryTheory.Limits.Types.Pushout {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

                                                                    Construction of the pushout in the category of types, as a quotient of X₁ ⊕ X₂.

                                                                    Equations
                                                                    Instances For
                                                                      inductive CategoryTheory.Limits.Types.Pushout.Rel' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :
                                                                      X₁ X₂X₁ X₂Prop

                                                                      In case f : S ⟶ X₁ is a monomorphism, this relation is the equivalence relation generated by Pushout.Rel f g.

                                                                      Instances For
                                                                        def CategoryTheory.Limits.Types.Pushout' {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

                                                                        The quotient of X₁ ⊕ X₂ by the relation PushoutRel' f g.

                                                                        Equations
                                                                        Instances For
                                                                          def CategoryTheory.Limits.Types.Pushout.inl {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

                                                                          The left inclusion in the constructed pushout Pushout f g.

                                                                          Equations
                                                                          Instances For
                                                                            def CategoryTheory.Limits.Types.Pushout.inr {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) :

                                                                            The right inclusion in the constructed pushout Pushout f g.

                                                                            Equations
                                                                            Instances For

                                                                              The cocone cocone f g is colimit.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inl_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) (x₁ : X₁) (y₁ : X₁) :
                                                                                CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl x₁) (Sum.inl y₁) x₁ = y₁ ∃ (x₀ : S) (y₀ : S) (_ : g x₀ = g y₀), x₁ = f x₀ y₁ = f y₀
                                                                                @[simp]
                                                                                theorem CategoryTheory.Limits.Types.Pushout.inl_rel'_inr_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) (x₁ : X₁) (x₂ : X₂) :
                                                                                CategoryTheory.Limits.Types.Pushout.Rel' f g (Sum.inl x₁) (Sum.inr x₂) ∃ (s : S), x₁ = f s x₂ = g s
                                                                                @[simp]
                                                                                theorem CategoryTheory.Limits.Types.Pushout.inr_rel'_inr_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) (x₂ : X₂) (y₂ : X₂) :
                                                                                theorem CategoryTheory.Limits.Types.Pushout.Rel'.symm {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S X₁} {g : S X₂} {x : X₁ X₂} {y : X₁ X₂} (h : CategoryTheory.Limits.Types.Pushout.Rel' f g x y) :

                                                                                The obvious equivalence Pushout f g ≃ Pushout' f g.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  theorem CategoryTheory.Limits.Types.Pushout.inl_eq_inr_iff {S : Type u} {X₁ : Type u} {X₂ : Type u} (f : S X₁) (g : S X₂) [CategoryTheory.Mono f] (x₁ : X₁) (x₂ : X₂) :
                                                                                  theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_imp_of_iso {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S X₁} {g : S X₂} {c : CategoryTheory.Limits.PushoutCocone f g} {c' : CategoryTheory.Limits.PushoutCocone f g} (e : c c') (x₁ : X₁) (x₂ : X₂) (h : c.inl x₁ = c.inr x₂) :
                                                                                  c'.inl x₁ = c'.inr x₂
                                                                                  theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_iso {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S X₁} {g : S X₂} {c : CategoryTheory.Limits.PushoutCocone f g} {c' : CategoryTheory.Limits.PushoutCocone f g} (e : c c') (x₁ : X₁) (x₂ : X₂) :
                                                                                  c.inl x₁ = c.inr x₂ c'.inl x₁ = c'.inr x₂
                                                                                  theorem CategoryTheory.Limits.Types.pushoutCocone_inl_eq_inr_iff_of_isColimit {S : Type u} {X₁ : Type u} {X₂ : Type u} {f : S X₁} {g : S X₂} {c : CategoryTheory.Limits.PushoutCocone f g} (hc : CategoryTheory.Limits.IsColimit c) (h₁ : Function.Injective f) (x₁ : X₁) (x₂ : X₂) :
                                                                                  c.inl x₁ = c.inr x₂ ∃ (s : S), f s = x₁ g s = x₂
                                                                                  theorem CategoryTheory.Limits.MulticospanIndex.sections.ext_iff {I : CategoryTheory.Limits.MulticospanIndex (Type u)} (x : I.sections) (y : I.sections) :
                                                                                  x = y x.val = y.val
                                                                                  theorem CategoryTheory.Limits.MulticospanIndex.sections.ext {I : CategoryTheory.Limits.MulticospanIndex (Type u)} (x : I.sections) (y : I.sections) (val : x.val = y.val) :
                                                                                  x = y

                                                                                  Given I : MulticospanIndex (Type u), this is a type which identifies to the sections of the functor I.multicospan.

                                                                                  • val : (i : I.L) → I.left i

                                                                                    The data of an element in I.left i for each i : I.L.

                                                                                  • property : ∀ (r : I.R), I.fst r (self.val (I.fstTo r)) = I.snd r (self.val (I.sndTo r))
                                                                                  Instances For
                                                                                    theorem CategoryTheory.Limits.MulticospanIndex.sections.property {I : CategoryTheory.Limits.MulticospanIndex (Type u)} (self : I.sections) (r : I.R) :
                                                                                    I.fst r (self.val (I.fstTo r)) = I.snd r (self.val (I.sndTo r))
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.Limits.MulticospanIndex.sectionsEquiv_symm_apply_val (I : CategoryTheory.Limits.MulticospanIndex (Type u)) (s : I.multicospan.sections) (i : I.L) :
                                                                                    (I.sectionsEquiv.symm s).val i = s (CategoryTheory.Limits.WalkingMulticospan.left i)

                                                                                    The bijection I.sections ≃ I.multicospan.sections when I : MulticospanIndex (Type u) is a multiequalizer diagram in the category of types.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem CategoryTheory.Limits.Multifork.toSections_val {I : CategoryTheory.Limits.MulticospanIndex (Type u)} (c : CategoryTheory.Limits.Multifork I) (x : c.pt) (i : I.L) :
                                                                                      (c.toSections x).val i = c i x

                                                                                      Given a multiequalizer diagram I : MulticospanIndex (Type u) in the category of types and c a multifork for I, this is the canonical map c.pt → I.sections.

                                                                                      Equations
                                                                                      • c.toSections x = { val := fun (i : I.L) => c i x, property := }
                                                                                      Instances For

                                                                                        A multifork c : Multifork I in the category of types is limit iff the map c.toSections : c.pt → I.sections is a bijection.

                                                                                        The bijection I.sections ≃ c.pt when c : Multifork I is a limit multifork in the category of types.

                                                                                        Equations
                                                                                        Instances For