Documentation

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Equalizers and coequalizers #

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

An equalizer is the categorical generalization of the subobject {a ∈ A | f(a) = g(a)} known from abelian groups or modules. It is a limit cone over the diagram formed by f and g.

A coequalizer is the dual concept.

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 (co)equalizer.

Instances For
    Equations
    • CategoryTheory.Limits.instDecidableEqWalkingParallelPairHom = CategoryTheory.Limits.decEqWalkingParallelPairHom✝

    The functor WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ sending left to left and right to right.

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

      The equivalence WalkingParallelPair ⥤ WalkingParallelPairᵒᵖ sending left to left and right to right.

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

        parallelPair f g is the diagram in C consisting of the two morphisms f and g with common domain and codomain.

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

          Construct a morphism between parallel pairs.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def CategoryTheory.Limits.parallelPair.eqOfHomEq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {f' : X Y} {g' : X Y} (hf : f = f') (hg : g = g') :

            Construct a natural isomorphism between parallelPair f g and parallelPair f' g' given equalities f = f' and g = g'.

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

              A fork on f and g is just a Cone (parallelPair f g).

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

                A cofork on f and g is just a Cocone (parallelPair f g).

                Equations
                Instances For

                  A fork t on the parallel pair f g : X ⟶ Y consists of two morphisms t.π.app zero : t.pt ⟶ X and t.π.app one : t.pt ⟶ Y. Of these, only the first one is interesting, and we give it the shorter name Fork.ι t.

                  Equations
                  Instances For

                    A cofork t on the parallelPair f g : X ⟶ Y consists of two morphisms t.ι.app zero : X ⟶ t.pt and t.ι.app one : Y ⟶ t.pt. Of these, only the second one is interesting, and we give it the shorter name Cofork.π t.

                    Equations
                    Instances For

                      A fork on f g : X ⟶ Y is determined by the morphism ι : P ⟶ X satisfying ι ≫ f = ι ≫ g.

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

                        A cofork on f g : X ⟶ Y is determined by the morphism π : Y ⟶ P satisfying f ≫ π = g ≫ π.

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

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

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

                          theorem CategoryTheory.Limits.Fork.IsLimit.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {s : CategoryTheory.Limits.Fork f g} (hs : CategoryTheory.Limits.IsLimit s) {W : C} {k : W s.pt} {l : W s.pt} (h : CategoryTheory.CategoryStruct.comp k s = CategoryTheory.CategoryStruct.comp l s) :
                          k = l

                          If s is a limit fork over f and g, then a morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ s.pt such that l ≫ fork.ι s = k.

                          Equations
                          Instances For

                            If s is a limit fork over f and g, then a morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ s.pt such that l ≫ fork.ι s = k.

                            Equations
                            Instances For

                              If s is a colimit cofork over f and g, then a morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : s.pt ⟶ W such that cofork.π s ≫ l = k.

                              Equations
                              Instances For

                                If s is a colimit cofork over f and g, then a morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : s.pt ⟶ W such that cofork.π s ≫ l = k.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.Limits.Fork.IsLimit.mk_lift {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} (t : CategoryTheory.Limits.Fork f g) (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t = s) (uniq : ∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt t.pt), CategoryTheory.CategoryStruct.comp m t = sm = lift s) (s : CategoryTheory.Limits.Fork f g) :
                                  (CategoryTheory.Limits.Fork.IsLimit.mk t lift fac uniq).lift s = lift s
                                  def CategoryTheory.Limits.Fork.IsLimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} (t : CategoryTheory.Limits.Fork f g) (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt t.pt) (fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t = s) (uniq : ∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt t.pt), CategoryTheory.CategoryStruct.comp m t = sm = lift s) :

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

                                  Equations
                                  Instances For
                                    def CategoryTheory.Limits.Cofork.IsColimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} (t : CategoryTheory.Limits.Cofork f g) (desc : (s : CategoryTheory.Limits.Cofork f g) → t.pt s.pt) (fac : ∀ (s : CategoryTheory.Limits.Cofork f g), CategoryTheory.CategoryStruct.comp t (desc s) = s) (uniq : ∀ (s : CategoryTheory.Limits.Cofork f g) (m : t.pt s.pt), CategoryTheory.CategoryStruct.comp t m = sm = desc s) :

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

                                    Equations
                                    Instances For

                                      This is another convenient method to verify that a fork 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
                                        noncomputable def CategoryTheory.Limits.Fork.IsLimit.ofExistsUnique {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {t : CategoryTheory.Limits.Fork f g} (hs : ∀ (s : CategoryTheory.Limits.Fork f g), ∃! l : s.pt t.pt, CategoryTheory.CategoryStruct.comp l t = s) :

                                        Noncomputably make a limit cone from the existence of unique factorizations.

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

                                          Noncomputably make a colimit cocone from the existence of unique factorizations.

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

                                            Given a limit cone for the pair f g : X ⟶ Y, for any Z, morphisms from Z to its point are in bijection with morphisms h : Z ⟶ X such that h ≫ f = h ≫ g. Further, this bijection is natural in Z: see Fork.IsLimit.homIso_natural. This is a special case of IsLimit.homIso', often useful to construct adjunctions.

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

                                              Given a colimit cocone for the pair f g : X ⟶ Y, for any Z, morphisms from the cocone point to Z are in bijection with morphisms h : Y ⟶ Z such that f ≫ h = g ≫ h. Further, this bijection is natural in Z: see Cofork.IsColimit.homIso_natural. This is a special case of IsColimit.homIso', often useful to construct adjunctions.

                                              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 equalizers. Given F : WalkingParallelPair ⥤ C, which is really the same as parallelPair (F.map left) (F.map right), and a fork on F.map left and F.map right, we get a cone on F.

                                                If you're thinking about using this, have a look at hasEqualizers_of_hasLimit_parallelPair, 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 : WalkingParallelPair ⥤ C, which is really the same as parallelPair (F.map left) (F.map right), and a cofork on F.map left and F.map right, we get a cocone on F.

                                                  If you're thinking about using this, have a look at hasCoequalizers_of_hasColimit_parallelPair, 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 : WalkingParallelPair ⥤ C, which is really the same as parallelPair (F.map left) (F.map right) and a cone on F, we get a fork on F.map left and F.map right.

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

                                                      Given F : WalkingParallelPair ⥤ C, which is really the same as parallelPair (F.map left) (F.map right) and a cocone on F, we get a cofork on F.map left and F.map right.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem CategoryTheory.Limits.Fork.mkHom_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {s : CategoryTheory.Limits.Fork f g} {t : CategoryTheory.Limits.Fork f g} (k : s.pt t.pt) (w : CategoryTheory.CategoryStruct.comp k t = s) :
                                                        def CategoryTheory.Limits.Fork.mkHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {s : CategoryTheory.Limits.Fork f g} {t : CategoryTheory.Limits.Fork f g} (k : s.pt t.pt) (w : CategoryTheory.CategoryStruct.comp k t = s) :
                                                        s t

                                                        Helper function for constructing morphisms between equalizer forks.

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

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

                                                          Equations
                                                          Instances For

                                                            Every fork is isomorphic to one of the form Fork.of_ι _ _.

                                                            Equations
                                                            Instances For
                                                              def CategoryTheory.Limits.Fork.isLimitOfIsos {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {X' : C} {Y' : C} (c : CategoryTheory.Limits.Fork f g) (hc : CategoryTheory.Limits.IsLimit c) {f' : X' Y'} {g' : X' Y'} (c' : CategoryTheory.Limits.Fork f' g') (e₀ : X X') (e₁ : Y Y') (e : c.pt c'.pt) (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom) _auto✝) (comm₃ : autoParam (CategoryTheory.CategoryStruct.comp e.hom c' = CategoryTheory.CategoryStruct.comp c e₀.hom) _auto✝) :

                                                              Given two forks with isomorphic components in such a way that the natural diagrams commute, then if one is a limit, then the other one is as well.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[simp]
                                                                def CategoryTheory.Limits.Cofork.mkHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {s : CategoryTheory.Limits.Cofork f g} {t : CategoryTheory.Limits.Cofork f g} (k : s.pt t.pt) (w : CategoryTheory.CategoryStruct.comp s k = t) :
                                                                s t

                                                                Helper function for constructing morphisms between coequalizer coforks.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem CategoryTheory.Limits.Fork.hom_comp_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {s : CategoryTheory.Limits.Fork f✝ g} {t : CategoryTheory.Limits.Fork f✝ g} (f : s t) :
                                                                  @[simp]
                                                                  theorem CategoryTheory.Limits.Fork.π_comp_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {s : CategoryTheory.Limits.Cofork f✝ g} {t : CategoryTheory.Limits.Cofork f✝ g} (f : s t) :
                                                                  def CategoryTheory.Limits.Cofork.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} {s : CategoryTheory.Limits.Cofork f g} {t : CategoryTheory.Limits.Cofork f g} (i : s.pt t.pt) (w : autoParam (CategoryTheory.CategoryStruct.comp s i.hom = t) _auto✝) :
                                                                  s t

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

                                                                  Equations
                                                                  Instances For

                                                                    Every cofork is isomorphic to one of the form Cofork.ofπ _ _.

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

                                                                      HasEqualizer f g represents a particular choice of limiting cone for the parallel pair of morphisms f and g.

                                                                      Equations
                                                                      Instances For
                                                                        @[reducible, inline]
                                                                        noncomputable abbrev CategoryTheory.Limits.equalizer {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasEqualizer f g] :
                                                                        C

                                                                        If an equalizer of f and g exists, we can access an arbitrary choice of such by saying equalizer f g.

                                                                        Equations
                                                                        Instances For
                                                                          @[reducible, inline]

                                                                          If an equalizer of f and g exists, we can access the inclusion equalizer f g ⟶ X by saying equalizer.ι f g.

                                                                          Equations
                                                                          Instances For
                                                                            @[reducible, inline]

                                                                            An equalizer cone for a parallel pair f and g

                                                                            Equations
                                                                            Instances For

                                                                              The equalizer built from equalizer.ι f g 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 k ≫ f = k ≫ g factors through the equalizer of f and g via equalizer.lift : W ⟶ equalizer f g.

                                                                                Equations
                                                                                Instances For

                                                                                  A morphism k : W ⟶ X satisfying k ≫ f = k ≫ g induces a morphism l : W ⟶ equalizer f g satisfying l ≫ equalizer.ι f g = k.

                                                                                  Equations
                                                                                  Instances For

                                                                                    Two maps into an equalizer are equal if they are equal when composed with the equalizer map.

                                                                                    An equalizer morphism is a monomorphism

                                                                                    Equations
                                                                                    • =

                                                                                    The equalizer morphism in any limit cone is a monomorphism.

                                                                                    def CategoryTheory.Limits.idFork {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} (h : f = g) :

                                                                                    The identity determines a cone on the equalizer diagram of f and g if f = g.

                                                                                    Equations
                                                                                    Instances For

                                                                                      The identity on X is an equalizer of (f, g), if f = g.

                                                                                      Equations
                                                                                      Instances For

                                                                                        Every equalizer of (f, g), where f = g, is an isomorphism.

                                                                                        The equalizer of (f, g), where f = g, is an isomorphism.

                                                                                        Every equalizer of (f, f) is an isomorphism.

                                                                                        An equalizer that is an epimorphism is an isomorphism.

                                                                                        theorem CategoryTheory.Limits.eq_of_epi_fork_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} (t : CategoryTheory.Limits.Fork f g) [CategoryTheory.Epi t] :
                                                                                        f = g

                                                                                        Two morphisms are equal if there is a fork whose inclusion is epi.

                                                                                        If the equalizer of two morphisms is an epimorphism, then the two morphisms are equal.

                                                                                        The equalizer inclusion for (f, f) is an isomorphism.

                                                                                        Equations
                                                                                        • =

                                                                                        The equalizer of a morphism with itself is isomorphic to the source.

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

                                                                                          HasCoequalizer f g represents a particular choice of colimiting cocone for the parallel pair of morphisms f and g.

                                                                                          Equations
                                                                                          Instances For
                                                                                            @[reducible, inline]
                                                                                            noncomputable abbrev CategoryTheory.Limits.coequalizer {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) (g : X Y) [CategoryTheory.Limits.HasCoequalizer f g] :
                                                                                            C

                                                                                            If a coequalizer of f and g exists, we can access an arbitrary choice of such by saying coequalizer f g.

                                                                                            Equations
                                                                                            Instances For
                                                                                              @[reducible, inline]

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

                                                                                              Equations
                                                                                              Instances For
                                                                                                @[reducible, inline]

                                                                                                An arbitrary choice of coequalizer cocone for a parallel pair f and g.

                                                                                                Equations
                                                                                                Instances For

                                                                                                  The cofork built from coequalizer.π f g 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 f ≫ k = g ≫ k factors through the coequalizer of f and g via coequalizer.desc : coequalizer f g ⟶ W.

                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      Any morphism k : Y ⟶ W satisfying f ≫ k = g ≫ k induces a morphism l : coequalizer f g ⟶ W satisfying coequalizer.π ≫ g = l.

                                                                                                      Equations
                                                                                                      Instances For

                                                                                                        Two maps from a coequalizer are equal if they are equal when composed with the coequalizer map

                                                                                                        A coequalizer morphism is an epimorphism

                                                                                                        Equations
                                                                                                        • =

                                                                                                        The coequalizer morphism in any colimit cocone is an epimorphism.

                                                                                                        def CategoryTheory.Limits.idCofork {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} (h : f = g) :

                                                                                                        The identity determines a cocone on the coequalizer diagram of f and g, if f = g.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          The identity on Y is a coequalizer of (f, g), where f = g.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            Every coequalizer of (f, g), where f = g, is an isomorphism.

                                                                                                            The coequalizer of (f, g), where f = g, is an isomorphism.

                                                                                                            A coequalizer that is a monomorphism is an isomorphism.

                                                                                                            Two morphisms are equal if there is a cofork whose projection is mono.

                                                                                                            If the coequalizer of two morphisms is a monomorphism, then the two morphisms are equal.

                                                                                                            The coequalizer projection for (f, f) is an isomorphism.

                                                                                                            Equations
                                                                                                            • =

                                                                                                            The coequalizer of a morphism with itself is isomorphic to the target.

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              The comparison morphism for the equalizer of f,g. This is an isomorphism iff G preserves the equalizer of f,g; see CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean

                                                                                                              Equations
                                                                                                              Instances For

                                                                                                                A split mono f equalizes (retraction f ≫ f) and (𝟙 Y). Here we build the cone, and show in isSplitMonoEqualizes that it is a limit cone.

                                                                                                                Equations
                                                                                                                Instances For

                                                                                                                  A split mono f equalizes (retraction f ≫ f) and (𝟙 Y).

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

                                                                                                                    We show that the converse to isSplitMonoEqualizes is true: Whenever f equalizes (r ≫ f) and (𝟙 Y), then r is a retraction of f.

                                                                                                                    Equations
                                                                                                                    Instances For

                                                                                                                      The fork obtained by postcomposing an equalizer fork with a monomorphism is an equalizer.

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

                                                                                                                        An equalizer of an idempotent morphism and the identity is split mono.

                                                                                                                        Equations
                                                                                                                        Instances For

                                                                                                                          The equalizer of an idempotent morphism and the identity is split mono.

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

                                                                                                                            A split epi f coequalizes (f ≫ section_ f) and (𝟙 X). Here we build the cocone, and show in isSplitEpiCoequalizes that it is a colimit cocone.

                                                                                                                            Equations
                                                                                                                            Instances For

                                                                                                                              A split epi f coequalizes (f ≫ section_ f) and (𝟙 X).

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

                                                                                                                                We show that the converse to isSplitEpiEqualizes is true: Whenever f coequalizes (f ≫ s) and (𝟙 X), then s is a section of f.

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  The cofork obtained by precomposing a coequalizer cofork with an epimorphism is a coequalizer.

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

                                                                                                                                    The coequalizer of an idempotent morphism and the identity is split epi.

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