Documentation

Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Wide equalizers and wide coequalizers #

This file defines wide (co)equalizers as special cases of (co)limits.

A wide equalizer for the family of morphisms X ⟶ Y indexed by J is the categorical generalization of the subobject {a ∈ A | ∀ j₁ j₂, f(j₁, a) = f(j₂, a)}. Note that if J has fewer than two morphisms this condition is trivial, so some lemmas and definitions assume J is nonempty.

Main definitions #

Each of these has a dual.

Main statements #

Implementation notes #

As with the other special shapes in the limits library, all the definitions here are given as abbreviations of the general statements for limits, so all the simp lemmas and theorems about general limits can be used.

References #

The type of objects for the diagram indexing a wide (co)equalizer.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • CategoryTheory.Limits.instInhabitedWalkingParallelFamily = { default := CategoryTheory.Limits.WalkingParallelFamily.zero }

    The type family of morphisms for the diagram indexing a wide (co)equalizer.

    Instances For
      Equations
      • CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom = CategoryTheory.Limits.WalkingParallelFamily.decEqHom✝
      instance CategoryTheory.Limits.instInhabitedHomZero (J : Type v) :
      Inhabited (CategoryTheory.Limits.WalkingParallelFamily.Hom J CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.zero)

      Satisfying the inhabited linter

      Equations

      Composition of morphisms in the indexing diagram for wide (co)equalizers.

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

        parallelFamily f is the diagram in C consisting of the given family of morphisms, each with common domain and codomain.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Limits.parallelFamily_obj_zero {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J(X Y)) :
          (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.zero = X
          @[simp]
          theorem CategoryTheory.Limits.parallelFamily_obj_one {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J(X Y)) :
          (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.one = Y

          WalkingParallelPair as a category is equivalent to a special case of WalkingParallelFamily.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[reducible, inline]
            abbrev CategoryTheory.Limits.Trident {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J(X Y)) :
            Type (max (max w u) v)

            A trident on f is just a Cone (parallelFamily f).

            Equations
            Instances For
              @[reducible, inline]
              abbrev CategoryTheory.Limits.Cotrident {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J(X Y)) :
              Type (max (max w u) v)

              A cotrident on f and g is just a Cocone (parallelFamily f).

              Equations
              Instances For
                @[reducible, inline]
                abbrev CategoryTheory.Limits.Trident.ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (t : CategoryTheory.Limits.Trident f) :
                ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.zero (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.zero

                A trident t on the parallel family f : J → (X ⟶ Y) consists of two morphisms t.π.app zero : t.X ⟶ X and t.π.app one : t.X ⟶ Y. Of these, only the first one is interesting, and we give it the shorter name Trident.ι t.

                Equations
                • t = t.app CategoryTheory.Limits.WalkingParallelFamily.zero
                Instances For
                  @[reducible, inline]
                  abbrev CategoryTheory.Limits.Cotrident.π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (t : CategoryTheory.Limits.Cotrident f) :
                  (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.one ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one

                  A cotrident t on the parallel family f : J → (X ⟶ Y) consists of two morphisms t.ι.app zero : X ⟶ t.X and t.ι.app one : Y ⟶ t.X. Of these, only the second one is interesting, and we give it the shorter name Cotrident.π t.

                  Equations
                  • t = t.app CategoryTheory.Limits.WalkingParallelFamily.one
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Limits.Trident.ι_eq_app_zero {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (t : CategoryTheory.Limits.Trident f) :
                    t = t.app CategoryTheory.Limits.WalkingParallelFamily.zero
                    @[simp]
                    theorem CategoryTheory.Limits.Cotrident.π_eq_app_one {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (t : CategoryTheory.Limits.Cotrident f) :
                    t = t.app CategoryTheory.Limits.WalkingParallelFamily.one
                    @[simp]
                    theorem CategoryTheory.Limits.Trident.app_zero_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (s : CategoryTheory.Limits.Trident f) (j : J) {Z : C} (h : Y Z) :
                    CategoryTheory.CategoryStruct.comp (s.app CategoryTheory.Limits.WalkingParallelFamily.zero) (CategoryTheory.CategoryStruct.comp (f j) h) = CategoryTheory.CategoryStruct.comp (s.app CategoryTheory.Limits.WalkingParallelFamily.one) h
                    @[simp]
                    theorem CategoryTheory.Limits.Trident.app_zero {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (s : CategoryTheory.Limits.Trident f) (j : J) :
                    CategoryTheory.CategoryStruct.comp (s.app CategoryTheory.Limits.WalkingParallelFamily.zero) (f j) = s.app CategoryTheory.Limits.WalkingParallelFamily.one
                    @[simp]
                    theorem CategoryTheory.Limits.Cotrident.app_one_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (s : CategoryTheory.Limits.Cotrident f) (j : J) {Z : C} (h : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one Z) :
                    CategoryTheory.CategoryStruct.comp (f j) (CategoryTheory.CategoryStruct.comp (s.app CategoryTheory.Limits.WalkingParallelFamily.one) h) = CategoryTheory.CategoryStruct.comp (s.app CategoryTheory.Limits.WalkingParallelFamily.zero) h
                    @[simp]
                    theorem CategoryTheory.Limits.Cotrident.app_one {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (s : CategoryTheory.Limits.Cotrident f) (j : J) :
                    CategoryTheory.CategoryStruct.comp (f j) (s.app CategoryTheory.Limits.WalkingParallelFamily.one) = s.app CategoryTheory.Limits.WalkingParallelFamily.zero
                    @[simp]
                    theorem CategoryTheory.Limits.Trident.ofι_pt {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {P : C} (ι : P X) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) :
                    def CategoryTheory.Limits.Trident.ofι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {P : C} (ι : P X) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) :

                    A trident on f : J → (X ⟶ Y) is determined by the morphism ι : P ⟶ X satisfying ∀ j₁ j₂, ι ≫ f j₁ = ι ≫ f j₂.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Limits.Cotrident.ofπ_pt {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {P : C} (π : Y P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) :
                      def CategoryTheory.Limits.Cotrident.ofπ {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {P : C} (π : Y P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) :

                      A cotrident on f : J → (X ⟶ Y) is determined by the morphism π : Y ⟶ P satisfying ∀ j₁ j₂, f j₁ ≫ π = f j₂ ≫ π.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        theorem CategoryTheory.Limits.Trident.ι_ofι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {P : C} (ι : P X) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) :
                        theorem CategoryTheory.Limits.Cotrident.π_ofπ {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {P : C} (π : Y P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) :
                        theorem CategoryTheory.Limits.Trident.condition {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (j₁ : J) (j₂ : J) (t : CategoryTheory.Limits.Trident f) :
                        theorem CategoryTheory.Limits.Cotrident.condition_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (j₁ : J) (j₂ : J) (t : CategoryTheory.Limits.Cotrident f) {Z : C} (h : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one Z) :
                        theorem CategoryTheory.Limits.Cotrident.condition {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} (j₁ : J) (j₂ : J) (t : CategoryTheory.Limits.Cotrident f) :

                        To check whether two maps are equalized by both maps of a trident, it suffices to check it for the first map

                        To check whether two maps are coequalized by both maps of a cotrident, it suffices to check it for the second map

                        def CategoryTheory.Limits.Trident.IsLimit.lift' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W X) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) :
                        { l : W s.pt // CategoryTheory.CategoryStruct.comp l s = k }

                        If s is a limit trident over f, then a morphism k : W ⟶ X satisfying ∀ j₁ j₂, k ≫ f j₁ = k ≫ f j₂ induces a morphism l : W ⟶ s.X such that l ≫ Trident.ι s = k.

                        Equations
                        Instances For
                          def CategoryTheory.Limits.Cotrident.IsColimit.desc' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {s : CategoryTheory.Limits.Cotrident f} (hs : CategoryTheory.Limits.IsColimit s) {W : C} (k : Y W) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) :
                          { l : s.pt W // CategoryTheory.CategoryStruct.comp s l = k }

                          If s is a colimit cotrident over f, then a morphism k : Y ⟶ W satisfying ∀ j₁ j₂, f j₁ ≫ k = f j₂ ≫ k induces a morphism l : s.X ⟶ W such that Cotrident.π s ≫ l = k.

                          Equations
                          Instances For
                            def CategoryTheory.Limits.Trident.IsLimit.mk {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] (t : CategoryTheory.Limits.Trident f) (lift : (s : CategoryTheory.Limits.Trident f) → s.pt t.pt) (fac : ∀ (s : CategoryTheory.Limits.Trident f), CategoryTheory.CategoryStruct.comp (lift s) t = s) (uniq : ∀ (s : CategoryTheory.Limits.Trident f) (m : s.pt t.pt), (∀ (j : CategoryTheory.Limits.WalkingParallelFamily J), CategoryTheory.CategoryStruct.comp m (t.app j) = s.app j)m = lift s) :

                            This is a slightly more convenient method to verify that a trident is a limit cone. It only asks for a proof of facts that carry any mathematical content

                            Equations
                            Instances For
                              def CategoryTheory.Limits.Trident.IsLimit.mk' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] (t : CategoryTheory.Limits.Trident f) (create : (s : CategoryTheory.Limits.Trident f) → { l : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj CategoryTheory.Limits.WalkingParallelFamily.zero ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.zero // CategoryTheory.CategoryStruct.comp l t = s ∀ {m : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj CategoryTheory.Limits.WalkingParallelFamily.zero ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.zero}, CategoryTheory.CategoryStruct.comp m t = sm = l }) :

                              This is another convenient method to verify that a trident is a limit cone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

                              Equations
                              Instances For
                                def CategoryTheory.Limits.Cotrident.IsColimit.mk {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] (t : CategoryTheory.Limits.Cotrident f) (desc : (s : CategoryTheory.Limits.Cotrident f) → t.pt s.pt) (fac : ∀ (s : CategoryTheory.Limits.Cotrident f), CategoryTheory.CategoryStruct.comp t (desc s) = s) (uniq : ∀ (s : CategoryTheory.Limits.Cotrident f) (m : t.pt s.pt), (∀ (j : CategoryTheory.Limits.WalkingParallelFamily J), CategoryTheory.CategoryStruct.comp (t.app j) m = s.app j)m = desc s) :

                                This is a slightly more convenient method to verify that a cotrident is a colimit cocone. It only asks for a proof of facts that carry any mathematical content

                                Equations
                                Instances For
                                  def CategoryTheory.Limits.Cotrident.IsColimit.mk' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] (t : CategoryTheory.Limits.Cotrident f) (create : (s : CategoryTheory.Limits.Cotrident f) → { l : t.pt s.pt // CategoryTheory.CategoryStruct.comp t l = s ∀ {m : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one}, CategoryTheory.CategoryStruct.comp t m = sm = l }) :

                                  This is another convenient method to verify that a cotrident is a colimit cocone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

                                  Equations
                                  Instances For
                                    def CategoryTheory.Limits.Trident.IsLimit.homIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) :
                                    (Z t.pt) { h : Z X // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp h (f j₁) = CategoryTheory.CategoryStruct.comp h (f j₂) }

                                    Given a limit cone for the family f : J → (X ⟶ Y), for any Z, morphisms from Z to its point are in bijection with morphisms h : Z ⟶ X such that ∀ j₁ j₂, h ≫ f j₁ = h ≫ f j₂. Further, this bijection is natural in Z: see Trident.Limits.homIso_natural.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def CategoryTheory.Limits.Cotrident.IsColimit.homIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {t : CategoryTheory.Limits.Cotrident f} (ht : CategoryTheory.Limits.IsColimit t) (Z : C) :
                                      (t.pt Z) { h : Y Z // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) h = CategoryTheory.CategoryStruct.comp (f j₂) h }

                                      Given a colimit cocone for the family f : J → (X ⟶ Y), for any Z, morphisms from the cocone point to Z are in bijection with morphisms h : Z ⟶ X such that ∀ j₁ j₂, f j₁ ≫ h = f j₂ ≫ h. Further, this bijection is natural in Z: see Cotrident.IsColimit.homIso_natural.

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

                                        This is a helper construction that can be useful when verifying that a category has certain wide equalizers. Given F : WalkingParallelFamily ⥤ C, which is really the same as parallelFamily (fun j ↦ F.map (line j)), and a trident on fun j ↦ F.map (line j), we get a cone on F.

                                        If you're thinking about using this, have a look at hasWideEqualizers_of_hasLimit_parallelFamily, which you may find to be an easier way of achieving your goal.

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

                                          This is a helper construction that can be useful when verifying that a category has all coequalizers. Given F : WalkingParallelFamily ⥤ C, which is really the same as parallelFamily (fun j ↦ F.map (line j)), and a cotrident on fun j ↦ F.map (line j) we get a cocone on F.

                                          If you're thinking about using this, have a look at hasWideCoequalizers_of_hasColimit_parallelFamily, which you may find to be an easier way of achieving your goal.

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

                                            Given F : WalkingParallelFamily ⥤ C, which is really the same as parallelFamily (fun j ↦ F.map (line j)) and a cone on F, we get a trident on fun j ↦ F.map (line j).

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

                                              Given F : WalkingParallelFamily ⥤ C, which is really the same as parallelFamily (F.map left) (F.map right) and a cocone on F, we get a cotrident on fun j ↦ F.map (line j).

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

                                                Helper function for constructing morphisms between wide equalizer tridents.

                                                Equations
                                                Instances For
                                                  def CategoryTheory.Limits.Trident.ext {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} {t : CategoryTheory.Limits.Trident f} (i : s.pt t.pt) (w : autoParam (CategoryTheory.CategoryStruct.comp i.hom t = s) _auto✝) :
                                                  s t

                                                  To construct an isomorphism between tridents, it suffices to give an isomorphism between the cone points and check that it commutes with the ι morphisms.

                                                  Equations
                                                  Instances For

                                                    Helper function for constructing morphisms between coequalizer cotridents.

                                                    Equations
                                                    Instances For
                                                      def CategoryTheory.Limits.Cotrident.ext {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {s : CategoryTheory.Limits.Cotrident f} {t : CategoryTheory.Limits.Cotrident f} (i : s.pt t.pt) (w : autoParam (CategoryTheory.CategoryStruct.comp s i.hom = t) _auto✝) :
                                                      s t

                                                      To construct an isomorphism between cotridents, it suffices to give an isomorphism between the cocone points and check that it commutes with the π morphisms.

                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        abbrev CategoryTheory.Limits.HasWideEqualizer {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J(X Y)) :

                                                        HasWideEqualizer f represents a particular choice of limiting cone for the parallel family of morphisms f.

                                                        Equations
                                                        Instances For
                                                          @[reducible, inline]

                                                          If a wide equalizer of f exists, we can access an arbitrary choice of such by saying wideEqualizer f.

                                                          Equations
                                                          Instances For
                                                            @[reducible, inline]

                                                            If a wide equalizer of f exists, we can access the inclusion wideEqualizer f ⟶ X by saying wideEqualizer.ι f.

                                                            Equations
                                                            Instances For

                                                              The wideEqualizer built from wideEqualizer.ι f is limiting.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[reducible, inline]

                                                                A morphism k : W ⟶ X satisfying ∀ j₁ j₂, k ≫ f j₁ = k ≫ f j₂ factors through the wide equalizer of f via wideEqualizer.lift : W ⟶ wideEqualizer f.

                                                                Equations
                                                                Instances For

                                                                  A morphism k : W ⟶ X satisfying ∀ j₁ j₂, k ≫ f j₁ = k ≫ f j₂ induces a morphism l : W ⟶ wideEqualizer f satisfying l ≫ wideEqualizer.ι f = k.

                                                                  Equations
                                                                  Instances For

                                                                    A wide equalizer morphism is a monomorphism

                                                                    Equations
                                                                    • =
                                                                    @[reducible, inline]
                                                                    abbrev CategoryTheory.Limits.HasWideCoequalizer {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J(X Y)) :

                                                                    HasWideCoequalizer f g represents a particular choice of colimiting cocone for the parallel family of morphisms f.

                                                                    Equations
                                                                    Instances For
                                                                      @[reducible, inline]

                                                                      If a wide coequalizer of f, we can access an arbitrary choice of such by saying wideCoequalizer f.

                                                                      Equations
                                                                      Instances For
                                                                        @[reducible, inline]

                                                                        If a wideCoequalizer of f exists, we can access the corresponding projection by saying wideCoequalizer.π f.

                                                                        Equations
                                                                        Instances For
                                                                          @[reducible, inline]

                                                                          An arbitrary choice of coequalizer cocone for a parallel family f.

                                                                          Equations
                                                                          Instances For

                                                                            The cotrident built from wideCoequalizer.π f is colimiting.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              @[reducible, inline]

                                                                              Any morphism k : Y ⟶ W satisfying ∀ j₁ j₂, f j₁ ≫ k = f j₂ ≫ k factors through the wide coequalizer of f via wideCoequalizer.desc : wideCoequalizer f ⟶ W.

                                                                              Equations
                                                                              Instances For

                                                                                Any morphism k : Y ⟶ W satisfying ∀ j₁ j₂, f j₁ ≫ k = f j₂ ≫ k induces a morphism l : wideCoequalizer f ⟶ W satisfying wideCoequalizer.π ≫ g = l.

                                                                                Equations
                                                                                Instances For

                                                                                  A wide coequalizer morphism is an epimorphism

                                                                                  Equations
                                                                                  • =
                                                                                  theorem CategoryTheory.Limits.epi_of_isColimit_parallelFamily {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J(X Y)} [Nonempty J] {c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.parallelFamily f)} (i : CategoryTheory.Limits.IsColimit c) :
                                                                                  CategoryTheory.Epi (c.app CategoryTheory.Limits.WalkingParallelFamily.one)

                                                                                  The wide coequalizer morphism in any colimit cocone is an epimorphism.

                                                                                  @[reducible, inline]

                                                                                  HasWideEqualizers represents a choice of wide equalizer for every family of morphisms

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[reducible, inline]

                                                                                    HasWideCoequalizers represents a choice of wide coequalizer for every family of morphisms

                                                                                    Equations
                                                                                    Instances For