HepLean Documentation

Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Constructing equalizers from pullbacks and binary products. #

If a category has pullbacks and binary products, then it has equalizers.

TODO: generalize universe

source
@[reducible, inline]
abbrev CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.constructEqualizer {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
C

Define the equalizing object

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
    CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.constructEqualizer F ⟶ F.obj CategoryTheory.Limits.WalkingParallelPair.zero

    Define the equalizing morphism

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
      CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst F = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.zero)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.zero)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
      source
      @[reducible, inline]
      abbrev CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
      CategoryTheory.Limits.Cone F

      Define the equalizing cone

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerConeIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone F)

        Show the equalizing cone is a limit

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] :
          CategoryTheory.Limits.HasEqualizers C

          Any category with pullbacks and binary products, has equalizers.

          source
          theorem CategoryTheory.Limits.preservesEqualizers_of_preservesPullbacks_and_binaryProducts {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G] :
          CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G

          A functor that preserves pullbacks and binary products also presrves equalizers.

          source
          @[reducible, inline]
          abbrev CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.constructCoequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
          C

          Define the equalizing object

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[reducible, inline]
            abbrev CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
            F.obj CategoryTheory.Limits.WalkingParallelPair.one ⟶ CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.constructCoequalizer F

            Define the equalizing morphism

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
              CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl F = CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.one)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.one)) (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
              source
              @[reducible, inline]
              abbrev CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
              CategoryTheory.Limits.Cocone F

              Define the equalizing cocone

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCoconeIsColimit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C) :
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone F)

                Show the equalizing cocone is a colimit

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem CategoryTheory.Limits.hasCoequalizers_of_hasPushouts_and_binary_coproducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] :
                  CategoryTheory.Limits.HasCoequalizers C

                  Any category with pullbacks and binary products, has equalizers.

                  source
                  theorem CategoryTheory.Limits.preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G] :
                  CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G

                  A functor that preserves pushouts and binary coproducts also presrves coequalizers.