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_familyis the indexing category used for wide (co)equalizer diagramsparallel_familyis a functor fromwalking_parallel_familyto our categoryC.- a
tridentis 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.ι.
- 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
- a
wide_equalizeris now just alimit (parallel_family f)
Each of these has a dual.
Main statements #
wide_equalizer.ι_monostates that every wide_equalizer map is a monomorphismis_iso_limit_cone_parallel_family_of_selfstates that the identity on the domain offis an equalizer offandf.
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 #
- zero : Π {J : Type w}, category_theory.limits.walking_parallel_family J
- one : Π {J : Type w}, category_theory.limits.walking_parallel_family J
The type of objects for the diagram indexing a wide (co)equalizer.
Instances for category_theory.limits.walking_parallel_family
- category_theory.limits.walking_parallel_family.has_sizeof_inst
- category_theory.limits.walking_parallel_family.inhabited
- category_theory.limits.walking_parallel_family.category
@[protected, instance]
Equations
- category_theory.limits.walking_parallel_family.decidable_eq category_theory.limits.walking_parallel_family.one category_theory.limits.walking_parallel_family.one = decidable.is_true category_theory.limits.walking_parallel_family.decidable_eq._main._proof_4
- category_theory.limits.walking_parallel_family.decidable_eq category_theory.limits.walking_parallel_family.one category_theory.limits.walking_parallel_family.zero = decidable.is_false category_theory.limits.walking_parallel_family.decidable_eq._main._proof_3
- category_theory.limits.walking_parallel_family.decidable_eq category_theory.limits.walking_parallel_family.zero category_theory.limits.walking_parallel_family.one = decidable.is_false category_theory.limits.walking_parallel_family.decidable_eq._main._proof_2
- category_theory.limits.walking_parallel_family.decidable_eq category_theory.limits.walking_parallel_family.zero category_theory.limits.walking_parallel_family.zero = decidable.is_true category_theory.limits.walking_parallel_family.decidable_eq._main._proof_1
@[protected, instance]
- id : Π {J : Type w} (X : category_theory.limits.walking_parallel_family J), category_theory.limits.walking_parallel_family.hom J X X
- line : Π {J : Type w}, J → category_theory.limits.walking_parallel_family.hom J category_theory.limits.walking_parallel_family.zero category_theory.limits.walking_parallel_family.one
The type family of morphisms for the diagram indexing a wide (co)equalizer.
Instances for category_theory.limits.walking_parallel_family.hom
- category_theory.limits.walking_parallel_family.hom.has_sizeof_inst
- category_theory.limits.walking_parallel_family.hom.inhabited
@[protected, instance]
def
category_theory.limits.walking_parallel_family.hom.decidable_eq
(J : Type w)
[a : decidable_eq J]
(ᾰ ᾰ_1 : category_theory.limits.walking_parallel_family J) :
@[protected, instance]
Satisfying the inhabited linter
def
category_theory.limits.walking_parallel_family.hom.comp
{J : Type w}
(X Y Z : category_theory.limits.walking_parallel_family J)
(f : category_theory.limits.walking_parallel_family.hom J X Y)
(g : category_theory.limits.walking_parallel_family.hom J Y Z) :
Composition of morphisms in the indexing diagram for wide (co)equalizers.
Equations
- category_theory.limits.walking_parallel_family.hom.comp category_theory.limits.walking_parallel_family.zero category_theory.limits.walking_parallel_family.one category_theory.limits.walking_parallel_family.one (category_theory.limits.walking_parallel_family.hom.line j) (category_theory.limits.walking_parallel_family.hom.id category_theory.limits.walking_parallel_family.one) = category_theory.limits.walking_parallel_family.hom.line j
- category_theory.limits.walking_parallel_family.hom.comp _x _x _x_1 (category_theory.limits.walking_parallel_family.hom.id _x) h = h
@[protected, instance]
Equations
- category_theory.limits.walking_parallel_family.category = {to_category_struct := {to_quiver := {hom := category_theory.limits.walking_parallel_family.hom J}, id := category_theory.limits.walking_parallel_family.hom.id J, comp := category_theory.limits.walking_parallel_family.hom.comp J}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
def
category_theory.limits.parallel_family
{J : Type w}
{C : Type u}
[category_theory.category C]
{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
- category_theory.limits.parallel_family f = {obj := λ (x : category_theory.limits.walking_parallel_family J), x.cases_on X Y, map := λ (x y : category_theory.limits.walking_parallel_family J) (h : x ⟶ y), category_theory.limits.parallel_family._match_1 f x y h, map_id' := _, map_comp' := _}
- category_theory.limits.parallel_family._match_1 f category_theory.limits.walking_parallel_family.zero category_theory.limits.walking_parallel_family.one (category_theory.limits.walking_parallel_family.hom.line j) = f j
- category_theory.limits.parallel_family._match_1 f _x _x (category_theory.limits.walking_parallel_family.hom.id _x) = 𝟙 (_x.cases_on X Y)
@[simp]
theorem
category_theory.limits.parallel_family_obj_zero
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y)) :
@[simp]
theorem
category_theory.limits.parallel_family_obj_one
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y)) :
@[simp]
theorem
category_theory.limits.parallel_family_map_left
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
{j : J} :
@[simp]
theorem
category_theory.limits.diagram_iso_parallel_family_hom_app
{J : Type w}
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.walking_parallel_family J ⥤ C)
(X : category_theory.limits.walking_parallel_family J) :
def
category_theory.limits.diagram_iso_parallel_family
{J : Type w}
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.walking_parallel_family J ⥤ C) :
Every functor indexing a wide (co)equalizer is naturally isomorphic (actually, equal) to a
parallel_family
@[simp]
theorem
category_theory.limits.diagram_iso_parallel_family_inv_app
{J : Type w}
{C : Type u}
[category_theory.category C]
(F : category_theory.limits.walking_parallel_family J ⥤ C)
(X : category_theory.limits.walking_parallel_family J) :
@[simp]
theorem
category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair_unit_iso
:
category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair.unit_iso = category_theory.nat_iso.of_components (λ (X : category_theory.limits.walking_parallel_family (ulift bool)), category_theory.eq_to_iso _) category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair._proof_2
walking_parallel_pair as a category is equivalent to a special case of
walking_parallel_family.
Equations
- category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair = {functor := category_theory.limits.parallel_family (λ (p : ulift bool), cond p.down category_theory.limits.walking_parallel_pair_hom.left category_theory.limits.walking_parallel_pair_hom.right), inverse := category_theory.limits.parallel_pair (category_theory.limits.walking_parallel_family.hom.line {down := bool.tt}) (category_theory.limits.walking_parallel_family.hom.line {down := bool.ff}), unit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.limits.walking_parallel_family (ulift bool)), category_theory.eq_to_iso _) category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair._proof_2, counit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.limits.walking_parallel_pair), category_theory.eq_to_iso _) category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair._proof_4, functor_unit_iso_comp' := category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair._proof_5}
@[simp]
theorem
category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair_counit_iso
:
category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair.counit_iso = category_theory.nat_iso.of_components (λ (X : category_theory.limits.walking_parallel_pair), category_theory.eq_to_iso _) category_theory.limits.walking_parallel_family_equiv_walking_parallel_pair._proof_4
@[reducible]
def
category_theory.limits.trident
{J : Type w}
{C : Type u}
[category_theory.category C]
{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}
[category_theory.category C]
{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]
def
category_theory.limits.trident.ι
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(t : category_theory.limits.trident f) :
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]
def
category_theory.limits.cotrident.π
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(t : category_theory.limits.cotrident f) :
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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(t : category_theory.limits.trident f) :
@[simp]
theorem
category_theory.limits.cotrident.π_eq_app_one
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(t : category_theory.limits.cotrident f) :
@[simp]
theorem
category_theory.limits.trident.app_zero
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(s : category_theory.limits.trident f)
(j : J) :
@[simp]
theorem
category_theory.limits.trident.app_zero_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(s : category_theory.limits.trident f)
(j : J)
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.cotrident.app_one_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(s : category_theory.limits.cotrident f)
(j : J)
{X' : C}
(f' : ((category_theory.functor.const (category_theory.limits.walking_parallel_family J)).obj s.X).obj category_theory.limits.walking_parallel_family.one ⟶ X') :
@[simp]
theorem
category_theory.limits.cotrident.app_one
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(s : category_theory.limits.cotrident f)
(j : J) :
noncomputable
def
category_theory.limits.trident.of_ι
{J : Type w}
{C : Type u}
[category_theory.category C]
{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
- category_theory.limits.trident.of_ι ι w = {X := P, π := {app := λ (X_1 : category_theory.limits.walking_parallel_family J), X_1.cases_on ι (ι ≫ f (classical.arbitrary J)), naturality' := _}}
@[simp]
theorem
category_theory.limits.trident.of_ι_π_app
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{P : C}
(ι : P ⟶ X)
(w : ∀ (j₁ j₂ : J), ι ≫ f j₁ = ι ≫ f j₂)
(X_1 : category_theory.limits.walking_parallel_family J) :
(category_theory.limits.trident.of_ι ι w).π.app X_1 = X_1.cases_on ι (ι ≫ f (classical.arbitrary J))
noncomputable
def
category_theory.limits.cotrident.of_π
{J : Type w}
{C : Type u}
[category_theory.category C]
{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
- category_theory.limits.cotrident.of_π π w = {X := P, ι := {app := λ (X_1 : category_theory.limits.walking_parallel_family J), X_1.cases_on (f (classical.arbitrary J) ≫ π) π, naturality' := _}}
@[simp]
theorem
category_theory.limits.cotrident.of_π_ι_app
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{P : C}
(π : Y ⟶ P)
(w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π)
(X_1 : category_theory.limits.walking_parallel_family J) :
(category_theory.limits.cotrident.of_π π w).ι.app X_1 = X_1.cases_on (f (classical.arbitrary J) ≫ π) π
theorem
category_theory.limits.trident.condition
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(j₁ j₂ : J)
(t : category_theory.limits.trident f) :
theorem
category_theory.limits.cotrident.condition_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(j₁ j₂ : J)
(t : category_theory.limits.cotrident f)
{X' : C}
(f' : ((category_theory.functor.const (category_theory.limits.walking_parallel_family J)).obj t.X).obj category_theory.limits.walking_parallel_family.one ⟶ X') :
theorem
category_theory.limits.cotrident.condition
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
(j₁ j₂ : J)
(t : category_theory.limits.cotrident f) :
theorem
category_theory.limits.trident.equalizer_ext
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
(s : category_theory.limits.trident f)
{W : C}
{k l : W ⟶ s.X}
(h : k ≫ s.ι = l ≫ s.ι)
(j : category_theory.limits.walking_parallel_family 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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
(s : category_theory.limits.cotrident f)
{W : C}
{k l : s.X ⟶ W}
(h : s.π ≫ k = s.π ≫ l)
(j : category_theory.limits.walking_parallel_family J) :
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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{s : category_theory.limits.trident f}
(hs : category_theory.limits.is_limit s)
{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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{s : category_theory.limits.cotrident f}
(hs : category_theory.limits.is_colimit s)
{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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{s : category_theory.limits.trident f}
(hs : category_theory.limits.is_limit s)
{W : C}
(k : W ⟶ X)
(h : ∀ (j₁ j₂ : J), k ≫ f j₁ = k ≫ f j₂) :
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
- category_theory.limits.trident.is_limit.lift' hs k h = ⟨hs.lift (category_theory.limits.trident.of_ι k h), _⟩
noncomputable
def
category_theory.limits.cotrident.is_colimit.desc'
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{s : category_theory.limits.cotrident f}
(hs : category_theory.limits.is_colimit s)
{W : C}
(k : Y ⟶ W)
(h : ∀ (j₁ j₂ : J), f j₁ ≫ k = f j₂ ≫ 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
- category_theory.limits.cotrident.is_colimit.desc' hs k h = ⟨hs.desc (category_theory.limits.cotrident.of_π k h), _⟩
def
category_theory.limits.trident.is_limit.mk
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
(t : category_theory.limits.trident f)
(lift : Π (s : category_theory.limits.trident f), s.X ⟶ t.X)
(fac : ∀ (s : category_theory.limits.trident f), lift s ≫ t.ι = s.ι)
(uniq : ∀ (s : category_theory.limits.trident f) (m : s.X ⟶ t.X), (∀ (j : category_theory.limits.walking_parallel_family 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
def
category_theory.limits.trident.is_limit.mk'
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
(t : category_theory.limits.trident f)
(create : Π (s : category_theory.limits.trident f), {l // l ≫ t.ι = s.ι ∧ ∀ {m : ((category_theory.functor.const (category_theory.limits.walking_parallel_family J)).obj s.X).obj category_theory.limits.walking_parallel_family.zero ⟶ ((category_theory.functor.const (category_theory.limits.walking_parallel_family J)).obj t.X).obj category_theory.limits.walking_parallel_family.zero}, m ≫ t.ι = s.ι → m = 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
- category_theory.limits.trident.is_limit.mk' t create = category_theory.limits.trident.is_limit.mk t (λ (s : category_theory.limits.trident f), (create s).val) _ _
def
category_theory.limits.cotrident.is_colimit.mk
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
(t : category_theory.limits.cotrident f)
(desc : Π (s : category_theory.limits.cotrident f), t.X ⟶ s.X)
(fac : ∀ (s : category_theory.limits.cotrident f), t.π ≫ desc s = s.π)
(uniq : ∀ (s : category_theory.limits.cotrident f) (m : t.X ⟶ s.X), (∀ (j : category_theory.limits.walking_parallel_family 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
def
category_theory.limits.cotrident.is_colimit.mk'
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
(t : category_theory.limits.cotrident f)
(create : Π (s : category_theory.limits.cotrident f), {l // t.π ≫ l = s.π ∧ ∀ {m : ((category_theory.functor.const (category_theory.limits.walking_parallel_family J)).obj t.X).obj category_theory.limits.walking_parallel_family.one ⟶ ((category_theory.functor.const (category_theory.limits.walking_parallel_family J)).obj s.X).obj category_theory.limits.walking_parallel_family.one}, t.π ≫ m = s.π → m = 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
- category_theory.limits.cotrident.is_colimit.mk' t create = category_theory.limits.cotrident.is_colimit.mk t (λ (s : category_theory.limits.cotrident f), (create s).val) _ _
@[simp]
theorem
category_theory.limits.trident.is_limit.hom_iso_apply_coe
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{t : category_theory.limits.trident f}
(ht : category_theory.limits.is_limit t)
(Z : C)
(k : Z ⟶ t.X) :
noncomputable
def
category_theory.limits.trident.is_limit.hom_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{t : category_theory.limits.trident f}
(ht : category_theory.limits.is_limit t)
(Z : C) :
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.
@[simp]
theorem
category_theory.limits.trident.is_limit.hom_iso_symm_apply
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{t : category_theory.limits.trident f}
(ht : category_theory.limits.is_limit t)
(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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{t : category_theory.limits.trident f}
(ht : category_theory.limits.is_limit t)
{Z Z' : C}
(q : Z' ⟶ Z)
(k : Z ⟶ t.X) :
↑(⇑(category_theory.limits.trident.is_limit.hom_iso ht Z') (q ≫ k)) = q ≫ ↑(⇑(category_theory.limits.trident.is_limit.hom_iso ht Z) 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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{t : category_theory.limits.cotrident f}
(ht : category_theory.limits.is_colimit t)
(Z : C)
(k : t.X ⟶ Z) :
noncomputable
def
category_theory.limits.cotrident.is_colimit.hom_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{t : category_theory.limits.cotrident f}
(ht : category_theory.limits.is_colimit t)
(Z : C) :
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.
@[simp]
theorem
category_theory.limits.cotrident.is_colimit.hom_iso_symm_apply
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{t : category_theory.limits.cotrident f}
(ht : category_theory.limits.is_colimit t)
(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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{t : category_theory.limits.cotrident f}
{Z Z' : C}
(q : Z ⟶ Z')
(ht : category_theory.limits.is_colimit t)
(k : t.X ⟶ Z) :
↑(⇑(category_theory.limits.cotrident.is_colimit.hom_iso ht Z') (k ≫ q)) = ↑(⇑(category_theory.limits.cotrident.is_colimit.hom_iso ht Z) k) ≫ q
The bijection of cotrident.is_colimit.hom_iso is natural in Z.
def
category_theory.limits.cone.of_trident
{J : Type w}
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_parallel_family J ⥤ C}
(t : category_theory.limits.trident (λ (j : J), F.map (category_theory.limits.walking_parallel_family.hom.line j))) :
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
- category_theory.limits.cone.of_trident t = {X := t.X, π := {app := λ (X : category_theory.limits.walking_parallel_family J), t.π.app X ≫ category_theory.eq_to_hom _, naturality' := _}}
def
category_theory.limits.cocone.of_cotrident
{J : Type w}
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_parallel_family J ⥤ C}
(t : category_theory.limits.cotrident (λ (j : J), F.map (category_theory.limits.walking_parallel_family.hom.line j))) :
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
- category_theory.limits.cocone.of_cotrident t = {X := t.X, ι := {app := λ (X : category_theory.limits.walking_parallel_family J), category_theory.eq_to_hom _ ≫ t.ι.app X, naturality' := _}}
@[simp]
theorem
category_theory.limits.cone.of_trident_π
{J : Type w}
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_parallel_family J ⥤ C}
(t : category_theory.limits.trident (λ (j : J), F.map (category_theory.limits.walking_parallel_family.hom.line j)))
(j : category_theory.limits.walking_parallel_family J) :
(category_theory.limits.cone.of_trident t).π.app j = t.π.app j ≫ category_theory.eq_to_hom _
@[simp]
theorem
category_theory.limits.cocone.of_cotrident_ι
{J : Type w}
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_parallel_family J ⥤ C}
(t : category_theory.limits.cotrident (λ (j : J), F.map (category_theory.limits.walking_parallel_family.hom.line j)))
(j : category_theory.limits.walking_parallel_family J) :
def
category_theory.limits.trident.of_cone
{J : Type w}
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_parallel_family J ⥤ C}
(t : category_theory.limits.cone F) :
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
- category_theory.limits.trident.of_cone t = {X := t.X, π := {app := λ (X : category_theory.limits.walking_parallel_family J), t.π.app X ≫ category_theory.eq_to_hom _, naturality' := _}}
def
category_theory.limits.cotrident.of_cocone
{J : Type w}
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_parallel_family J ⥤ C}
(t : category_theory.limits.cocone F) :
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
- category_theory.limits.cotrident.of_cocone t = {X := t.X, ι := {app := λ (X : category_theory.limits.walking_parallel_family J), category_theory.eq_to_hom _ ≫ t.ι.app X, naturality' := _}}
@[simp]
theorem
category_theory.limits.trident.of_cone_π
{J : Type w}
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_parallel_family J ⥤ C}
(t : category_theory.limits.cone F)
(j : category_theory.limits.walking_parallel_family J) :
(category_theory.limits.trident.of_cone t).π.app j = t.π.app j ≫ category_theory.eq_to_hom _
@[simp]
theorem
category_theory.limits.cotrident.of_cocone_ι
{J : Type w}
{C : Type u}
[category_theory.category C]
{F : category_theory.limits.walking_parallel_family J ⥤ C}
(t : category_theory.limits.cocone F)
(j : category_theory.limits.walking_parallel_family J) :
def
category_theory.limits.trident.mk_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
{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
- category_theory.limits.trident.mk_hom k w = {hom := k, w' := _}
@[simp]
theorem
category_theory.limits.trident.mk_hom_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
{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.ι) :
def
category_theory.limits.trident.ext
{J : Type w}
{C : Type u}
[category_theory.category C]
{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
- category_theory.limits.trident.ext i w = {hom := category_theory.limits.trident.mk_hom i.hom w, inv := category_theory.limits.trident.mk_hom i.inv _, hom_inv_id' := _, inv_hom_id' := _}
def
category_theory.limits.cotrident.mk_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
{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
- category_theory.limits.cotrident.mk_hom k w = {hom := k, w' := _}
@[simp]
theorem
category_theory.limits.cotrident.mk_hom_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
{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}
[category_theory.category C]
{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
- category_theory.limits.cotrident.ext i w = {hom := category_theory.limits.cotrident.mk_hom i.hom w, inv := category_theory.limits.cotrident.mk_hom i.inv _, hom_inv_id' := _, inv_hom_id' := _}
@[reducible]
def
category_theory.limits.has_wide_equalizer
{J : Type w}
{C : Type u}
[category_theory.category C]
{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}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_equalizer f] :
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}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_equalizer f] :
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}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_equalizer f] :
A wide equalizer cone for a parallel family f.
@[simp]
theorem
category_theory.limits.wide_equalizer.trident_ι
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_equalizer f] :
@[simp]
theorem
category_theory.limits.wide_equalizer.trident_π_app_zero
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_equalizer f] :
theorem
category_theory.limits.wide_equalizer.condition_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_equalizer f]
(j₁ j₂ : J)
{X' : C}
(f' : Y ⟶ X') :
category_theory.limits.wide_equalizer.ι f ≫ f j₁ ≫ f' = category_theory.limits.wide_equalizer.ι f ≫ f j₂ ≫ f'
theorem
category_theory.limits.wide_equalizer.condition
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_equalizer f]
(j₁ j₂ : J) :
noncomputable
def
category_theory.limits.wide_equalizer_is_wide_equalizer
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_equalizer f]
[nonempty J] :
The wide_equalizer built from wide_equalizer.ι f is limiting.
Equations
- category_theory.limits.wide_equalizer_is_wide_equalizer f = (category_theory.limits.limit.is_limit (category_theory.limits.parallel_family (λ (j₁ : J), f j₁))).of_iso_limit (category_theory.limits.trident.ext (category_theory.iso.refl (category_theory.limits.limit.cone (category_theory.limits.parallel_family (λ (j₁ : J), f j₁))).X) _)
@[reducible]
noncomputable
def
category_theory.limits.wide_equalizer.lift
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_equalizer f]
[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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_equalizer f]
[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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_equalizer f]
[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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_equalizer f]
[nonempty J]
{W : C}
(k : W ⟶ X)
(h : ∀ (j₁ j₂ : J), k ≫ f j₁ = k ≫ f j₂) :
{l // l ≫ category_theory.limits.wide_equalizer.ι f = k}
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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_equalizer f]
[nonempty J]
{W : C}
{k l : W ⟶ category_theory.limits.wide_equalizer f}
(h : k ≫ category_theory.limits.wide_equalizer.ι f = l ≫ category_theory.limits.wide_equalizer.ι f) :
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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_equalizer f]
[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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{c : category_theory.limits.cone (category_theory.limits.parallel_family f)}
(i : category_theory.limits.is_limit c) :
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}
[category_theory.category C]
{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}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_coequalizer f] :
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}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_coequalizer f] :
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}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_coequalizer f] :
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}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_coequalizer f] :
@[simp]
theorem
category_theory.limits.wide_coequalizer.cotrident_ι_app_one
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_coequalizer f] :
theorem
category_theory.limits.wide_coequalizer.condition
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_coequalizer f]
(j₁ j₂ : J) :
theorem
category_theory.limits.wide_coequalizer.condition_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_coequalizer f]
(j₁ j₂ : J)
{X' : C}
(f' : category_theory.limits.wide_coequalizer f ⟶ X') :
f j₁ ≫ category_theory.limits.wide_coequalizer.π f ≫ f' = f j₂ ≫ category_theory.limits.wide_coequalizer.π f ≫ f'
noncomputable
def
category_theory.limits.wide_coequalizer_is_wide_coequalizer
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
(f : J → (X ⟶ Y))
[category_theory.limits.has_wide_coequalizer f]
[nonempty J] :
The cotrident built from wide_coequalizer.π f is colimiting.
Equations
- category_theory.limits.wide_coequalizer_is_wide_coequalizer f = (category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_family (λ (j₁ : J), f j₁))).of_iso_colimit (category_theory.limits.cotrident.ext (category_theory.iso.refl (category_theory.limits.colimit.cocone (category_theory.limits.parallel_family (λ (j₁ : J), f j₁))).X) _)
@[reducible]
noncomputable
def
category_theory.limits.wide_coequalizer.desc
{J : Type w}
{C : Type u}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_coequalizer f]
[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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_coequalizer f]
[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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_coequalizer f]
[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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_coequalizer f]
[nonempty J]
{W : C}
(k : Y ⟶ W)
(h : ∀ (j₁ j₂ : J), f j₁ ≫ k = f j₂ ≫ k) :
{l // category_theory.limits.wide_coequalizer.π f ≫ l = k}
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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_coequalizer f]
[nonempty J]
{W : C}
{k l : category_theory.limits.wide_coequalizer f ⟶ W}
(h : category_theory.limits.wide_coequalizer.π f ≫ k = category_theory.limits.wide_coequalizer.π f ≫ l) :
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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[category_theory.limits.has_wide_coequalizer f]
[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}
[category_theory.category C]
{X Y : C}
{f : J → (X ⟶ Y)}
[nonempty J]
{c : category_theory.limits.cocone (category_theory.limits.parallel_family f)}
(i : category_theory.limits.is_colimit c) :
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)
[category_theory.category C]
[∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, category_theory.limits.has_limit (category_theory.limits.parallel_family f)] :
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)
[category_theory.category C]
[∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, category_theory.limits.has_colimit (category_theory.limits.parallel_family f)] :
If C has all colimits of diagrams parallel_family f, then it has all wide coequalizers
@[protected, instance]
@[protected, instance]