# mathlib3documentation

category_theory.limits.shapes.wide_equalizers

# Wide equalizers and wide coequalizers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• `walking_parallel_family` is the indexing category used for wide (co)equalizer diagrams
• `parallel_family` is a functor from `walking_parallel_family` to our category `C`.
• a `trident` is a cone over a parallel family.
• there is really only one interesting morphism in a trident: the arrow from the vertex of the trident to the domain of f and g. It is called `trident.ι`.
• a `wide_equalizer` is now just a `limit (parallel_family f)`

Each of these has a dual.

## Main statements #

• `wide_equalizer.ι_mono` states that every wide_equalizer map is a monomorphism
• `is_iso_limit_cone_parallel_family_of_self` states that the identity on the domain of `f` is an equalizer of `f` and `f`.

## Implementation notes #

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

## References #

• zero :
• one :

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

Instances for `category_theory.limits.walking_parallel_family`
@[protected, instance]
Equations
• = decidable.is_true category_theory.limits.walking_parallel_family.decidable_eq._main._proof_4
• = decidable.is_false category_theory.limits.walking_parallel_family.decidable_eq._main._proof_3
• = decidable.is_false category_theory.limits.walking_parallel_family.decidable_eq._main._proof_2
• = decidable.is_true category_theory.limits.walking_parallel_family.decidable_eq._main._proof_1
@[protected, instance]
Equations

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

Instances for `category_theory.limits.walking_parallel_family.hom`
@[protected, instance]
@[protected, instance]

Satisfying the inhabited linter

Equations

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

Equations
@[protected, instance]
Equations
@[simp]
def category_theory.limits.parallel_family {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) :

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

Equations
@[simp]
theorem category_theory.limits.parallel_family_obj_zero {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) :
@[simp]
theorem category_theory.limits.parallel_family_obj_one {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) :
@[simp]
theorem category_theory.limits.parallel_family_map_left {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) {j : J} :
@[simp]

Every functor indexing a wide (co)equalizer is naturally isomorphic (actually, equal) to a `parallel_family`

Equations
@[simp]

`walking_parallel_pair` as a category is equivalent to a special case of `walking_parallel_family`.

Equations
@[reducible]
def category_theory.limits.trident {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) :
Type (max w u v)

A trident on `f` is just a `cone (parallel_family f)`.

@[reducible]
def category_theory.limits.cotrident {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) :
Type (max w u v)

A cotrident on `f` and `g` is just a `cocone (parallel_family f)`.

@[reducible]

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

@[reducible]

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

@[simp]
theorem category_theory.limits.trident.ι_eq_app_zero {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)}  :
@[simp]
theorem category_theory.limits.cotrident.π_eq_app_one {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)}  :
@[simp]
theorem category_theory.limits.trident.app_zero {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} (j : J) :
@[simp]
theorem category_theory.limits.trident.app_zero_assoc {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} (j : J) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.cotrident.app_one_assoc {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} (j : J) {X' : C}  :
@[simp]
theorem category_theory.limits.cotrident.app_one {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} (j : J) :
noncomputable def category_theory.limits.trident.of_ι {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {P : C} (ι : P X) (w : (j₁ j₂ : J), ι f j₁ = ι f j₂) :

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

Equations
@[simp]
theorem category_theory.limits.trident.of_ι_X {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {P : C} (ι : P X) (w : (j₁ j₂ : J), ι f j₁ = ι f j₂) :
@[simp]
theorem category_theory.limits.trident.of_ι_π_app {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {P : C} (ι : P X) (w : (j₁ j₂ : J), ι f j₁ = ι f j₂)  :
X_1 = X_1.cases_on ι f
@[simp]
theorem category_theory.limits.cotrident.of_π_X {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {P : C} (π : Y P) (w : (j₁ j₂ : J), f j₁ π = f j₂ π) :
noncomputable def category_theory.limits.cotrident.of_π {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {P : C} (π : Y P) (w : (j₁ j₂ : J), f j₁ π = f j₂ π) :

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

Equations
@[simp]
theorem category_theory.limits.cotrident.of_π_ι_app {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {P : C} (π : Y P) (w : (j₁ j₂ : J), f j₁ π = f j₂ π)  :
X_1 = X_1.cases_on (f π) π
theorem category_theory.limits.trident.ι_of_ι {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {P : C} (ι : P X) (w : (j₁ j₂ : J), ι f j₁ = ι f j₂) :
theorem category_theory.limits.cotrident.π_of_π {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {P : C} (π : Y P) (w : (j₁ j₂ : J), f j₁ π = f j₂ π) :
theorem category_theory.limits.trident.condition_assoc {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} (j₁ j₂ : J) {X' : C} (f' : Y X') :
t.ι f j₁ f' = t.ι f j₂ f'
theorem category_theory.limits.trident.condition {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} (j₁ j₂ : J)  :
t.ι f j₁ = t.ι f j₂
theorem category_theory.limits.cotrident.condition_assoc {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} (j₁ j₂ : J) {X' : C}  :
f j₁ t.π f' = f j₂ t.π f'
theorem category_theory.limits.cotrident.condition {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} (j₁ j₂ : J)  :
f j₁ t.π = f j₂ t.π
theorem category_theory.limits.trident.equalizer_ext {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} {k l : W s.X} (h : k s.ι = l s.ι)  :
k s.π.app j = l s.π.app j

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

theorem category_theory.limits.cotrident.coequalizer_ext {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} {k l : s.X W} (h : s.π k = s.π l)  :
s.ι.app j k = s.ι.app j l

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

theorem category_theory.limits.trident.is_limit.hom_ext {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} {k l : W s.X} (h : k s.ι = l s.ι) :
k = l
theorem category_theory.limits.cotrident.is_colimit.hom_ext {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} {k l : s.X W} (h : s.π k = s.π l) :
k = l
noncomputable def category_theory.limits.trident.is_limit.lift' {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : W X) (h : (j₁ j₂ : J), k f j₁ = k f j₂) :
{l // 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
noncomputable def category_theory.limits.cotrident.is_colimit.desc' {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : Y W) (h : (j₁ j₂ : J), f j₁ k = f j₂ k) :
{l // 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
def category_theory.limits.trident.is_limit.mk {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (lift : Π (s : , s.X t.X) (fac : (s : , lift s t.ι = s.ι) (uniq : (s : (m : s.X t.X), ( (j : , 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
def category_theory.limits.trident.is_limit.mk' {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (create : Π (s : , {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
• = (λ (s : , (create s).val) _ _
def category_theory.limits.cotrident.is_colimit.mk {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (desc : Π (s : , t.X s.X) (fac : (s : , t.π desc s = s.π) (uniq : (s : (m : t.X s.X), ( (j : , 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
def category_theory.limits.cotrident.is_colimit.mk' {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (create : Π (s : , {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
• = (λ (s : , (create s).val) _ _
@[simp]
theorem category_theory.limits.trident.is_limit.hom_iso_apply_coe {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (Z : C) (k : Z t.X) :
= k t.ι
noncomputable def category_theory.limits.trident.is_limit.hom_iso {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (Z : C) :
(Z t.X) {h // (j₁ j₂ : J), h f j₁ = 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.is_limit.hom_iso_natural`.

Equations
@[simp]
theorem category_theory.limits.trident.is_limit.hom_iso_symm_apply {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (Z : C) (h : {h // (j₁ j₂ : J), h f j₁ = h f j₂}) :
theorem category_theory.limits.trident.is_limit.hom_iso_natural {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {Z Z' : C} (q : Z' Z) (k : Z t.X) :
(q k)) =

The bijection of `trident.is_limit.hom_iso` is natural in `Z`.

@[simp]
theorem category_theory.limits.cotrident.is_colimit.hom_iso_apply_coe {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (Z : C) (k : t.X Z) :
= t.π k
noncomputable def category_theory.limits.cotrident.is_colimit.hom_iso {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (Z : C) :
(t.X Z) {h // (j₁ j₂ : J), f j₁ h = 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.is_colimit.hom_iso_natural`.

Equations
@[simp]
theorem category_theory.limits.cotrident.is_colimit.hom_iso_symm_apply {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] (Z : C) (h : {h // (j₁ j₂ : J), f j₁ h = f j₂ h}) :
theorem category_theory.limits.cotrident.is_colimit.hom_iso_natural {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {Z Z' : C} (q : Z Z') (k : t.X Z) :
(k q)) =

The bijection of `cotrident.is_colimit.hom_iso` is natural in `Z`.

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

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

Equations

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

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

Equations
@[simp]
theorem category_theory.limits.cone.of_trident_π {J : Type w} {C : Type u} (t : category_theory.limits.trident (λ (j : J), )  :
@[simp]

Given `F : walking_parallel_family ⥤ C`, which is really the same as `parallel_family (λ j, F.map (line j))` and a cone on `F`, we get a trident on `λ j, F.map (line j)`.

Equations

Given `F : walking_parallel_family ⥤ C`, which is really the same as `parallel_family (F.map left) (F.map right)` and a cocone on `F`, we get a cotrident on `λ j, F.map (line j)`.

Equations
@[simp]
@[simp]
def category_theory.limits.trident.mk_hom {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {s t : category_theory.limits.trident f} (k : s.X t.X) (w : k t.ι = s.ι) :
s t

Helper function for constructing morphisms between wide equalizer tridents.

Equations
@[simp]
theorem category_theory.limits.trident.mk_hom_hom {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {s t : category_theory.limits.trident f} (k : s.X t.X) (w : k t.ι = s.ι) :
@[simp]
theorem category_theory.limits.trident.ext_hom {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {s t : category_theory.limits.trident f} (i : s.X t.X) (w : i.hom t.ι = s.ι) :
@[simp]
theorem category_theory.limits.trident.ext_inv {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {s t : category_theory.limits.trident f} (i : s.X t.X) (w : i.hom t.ι = s.ι) :
def category_theory.limits.trident.ext {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {s t : category_theory.limits.trident f} (i : s.X t.X) (w : i.hom t.ι = s.ι) :
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
def category_theory.limits.cotrident.mk_hom {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {s t : category_theory.limits.cotrident f} (k : s.X t.X) (w : s.π k = t.π) :
s t

Helper function for constructing morphisms between coequalizer cotridents.

Equations
@[simp]
theorem category_theory.limits.cotrident.mk_hom_hom {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {s t : category_theory.limits.cotrident f} (k : s.X t.X) (w : s.π k = t.π) :
def category_theory.limits.cotrident.ext {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {s t : category_theory.limits.cotrident f} (i : s.X t.X) (w : s.π i.hom = t.π) :
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
@[reducible]
def category_theory.limits.has_wide_equalizer {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) :
Prop

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

@[reducible]
noncomputable def category_theory.limits.wide_equalizer {J : Type w} {C : Type u} {X Y : C} (f : J (X Y))  :
C

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

@[reducible]
noncomputable def category_theory.limits.wide_equalizer.ι {J : Type w} {C : Type u} {X Y : C} (f : J (X Y))  :

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

@[reducible]
noncomputable def category_theory.limits.wide_equalizer.trident {J : Type w} {C : Type u} {X Y : C} (f : J (X Y))  :

A wide equalizer cone for a parallel family `f`.

@[simp]
theorem category_theory.limits.wide_equalizer.trident_ι {J : Type w} {C : Type u} {X Y : C} (f : J (X Y))  :
@[simp]
theorem category_theory.limits.wide_equalizer.condition_assoc {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) (j₁ j₂ : J) {X' : C} (f' : Y X') :
=
theorem category_theory.limits.wide_equalizer.condition {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) (j₁ j₂ : J) :
noncomputable def category_theory.limits.wide_equalizer_is_wide_equalizer {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) [nonempty J] :

The wide_equalizer built from `wide_equalizer.ι f` is limiting.

Equations
@[reducible]
noncomputable def category_theory.limits.wide_equalizer.lift {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : W X) (h : (j₁ j₂ : J), k f j₁ = k f j₂) :

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

@[simp]
theorem category_theory.limits.wide_equalizer.lift_ι {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : W X) (h : (j₁ j₂ : J), k f j₁ = k f j₂) :
@[simp]
theorem category_theory.limits.wide_equalizer.lift_ι_assoc {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : W X) (h : (j₁ j₂ : J), k f j₁ = k f j₂) {X' : C} (f' : X X') :
noncomputable def category_theory.limits.wide_equalizer.lift' {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : W X) (h : (j₁ j₂ : J), k f j₁ = k f j₂) :
{l //

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

Equations
@[ext]
theorem category_theory.limits.wide_equalizer.hom_ext {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} {k l : W }  :
k = l

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

@[protected, instance]
def category_theory.limits.wide_equalizer.ι_mono {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] :

A wide equalizer morphism is a monomorphism

theorem category_theory.limits.mono_of_is_limit_parallel_family {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J]  :

The wide equalizer morphism in any limit cone is a monomorphism.

@[reducible]
def category_theory.limits.has_wide_coequalizer {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) :
Prop

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

@[reducible]
noncomputable def category_theory.limits.wide_coequalizer {J : Type w} {C : Type u} {X Y : C} (f : J (X Y))  :
C

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

@[reducible]
noncomputable def category_theory.limits.wide_coequalizer.π {J : Type w} {C : Type u} {X Y : C} (f : J (X Y))  :

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

@[reducible]
noncomputable def category_theory.limits.wide_coequalizer.cotrident {J : Type w} {C : Type u} {X Y : C} (f : J (X Y))  :

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

@[simp]
theorem category_theory.limits.wide_coequalizer.cotrident_π {J : Type w} {C : Type u} {X Y : C} (f : J (X Y))  :
@[simp]
theorem category_theory.limits.wide_coequalizer.condition {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) (j₁ j₂ : J) :
theorem category_theory.limits.wide_coequalizer.condition_assoc {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) (j₁ j₂ : J) {X' : C} (f' : X') :
=
noncomputable def category_theory.limits.wide_coequalizer_is_wide_coequalizer {J : Type w} {C : Type u} {X Y : C} (f : J (X Y)) [nonempty J] :

The cotrident built from `wide_coequalizer.π f` is colimiting.

Equations
@[reducible]
noncomputable def category_theory.limits.wide_coequalizer.desc {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : Y W) (h : (j₁ j₂ : J), f j₁ k = f j₂ k) :

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

@[simp]
theorem category_theory.limits.wide_coequalizer.π_desc_assoc {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : Y W) (h : (j₁ j₂ : J), f j₁ k = f j₂ k) {X' : C} (f' : W X') :
@[simp]
theorem category_theory.limits.wide_coequalizer.π_desc {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : Y W) (h : (j₁ j₂ : J), f j₁ k = f j₂ k) :
noncomputable def category_theory.limits.wide_coequalizer.desc' {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} (k : Y W) (h : (j₁ j₂ : J), f j₁ k = f j₂ k) :
{l //

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

Equations
@[ext]
theorem category_theory.limits.wide_coequalizer.hom_ext {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] {W : C} {k l : W}  :
k = l

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

@[protected, instance]
def category_theory.limits.wide_coequalizer.π_epi {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J] :

A wide coequalizer morphism is an epimorphism

theorem category_theory.limits.epi_of_is_colimit_parallel_family {J : Type w} {C : Type u} {X Y : C} {f : J (X Y)} [nonempty J]  :

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

@[reducible]

`has_wide_equalizers` represents a choice of wide equalizer for every family of morphisms

@[reducible]

`has_wide_coequalizers` represents a choice of wide coequalizer for every family of morphisms

theorem category_theory.limits.has_wide_equalizers_of_has_limit_parallel_family (C : Type u) [ {J : Type w} {X Y : C} {f : J (X Y)}, ] :

If `C` has all limits of diagrams `parallel_family f`, then it has all wide equalizers

theorem category_theory.limits.has_wide_coequalizers_of_has_colimit_parallel_family (C : Type u) [ {J : Type w} {X Y : C} {f : J (X Y)}, ] :

If `C` has all colimits of diagrams `parallel_family f`, then it has all wide coequalizers

@[protected, instance]
@[protected, instance]