Wide equalizers and wide coequalizers

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

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

Main definitions

• WalkingParallelFamily is the indexing category used for wide (co)equalizer diagrams
• parallelFamily is a functor from WalkingParallelFamily 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 wideEqualizer is now just a limit (parallelFamily f)

Each of these has a dual.

Main statements

• wideEqualizer.ι_mono states that every wideEqualizer map is a monomorphism

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

• [F. Borceux, Handbook of Categorical Algebra 1][borceux-vol1]

inductive CategoryTheory.Limits.WalkingParallelFamily (J : Type w) : Type w

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

• zero: {J : Type w} → CategoryTheory.Limits.WalkingParallelFamily J
• one: {J : Type w} → CategoryTheory.Limits.WalkingParallelFamily J

instance CategoryTheory.Limits.instDecidableEqWalkingParallelFamily {J : Type w} : DecidableEq (CategoryTheory.Limits.WalkingParallelFamily J)

Equations

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

instance CategoryTheory.Limits.instInhabitedWalkingParallelFamily {J : Type w} : Inhabited (CategoryTheory.Limits.WalkingParallelFamily J)

Equations

• CategoryTheory.Limits.instInhabitedWalkingParallelFamily = { default := CategoryTheory.Limits.WalkingParallelFamily.zero }

inductive CategoryTheory.Limits.WalkingParallelFamily.Hom (J : Type w) : CategoryTheory.Limits.WalkingParallelFamily J → CategoryTheory.Limits.WalkingParallelFamily J → Type w

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

• id: {J : Type w} → (X : CategoryTheory.Limits.WalkingParallelFamily J) → CategoryTheory.Limits.WalkingParallelFamily.Hom J X X
• line: {J : Type w} → J → CategoryTheory.Limits.WalkingParallelFamily.Hom J CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.one

instance CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom : {J : Type u_1} → {a a_1 : CategoryTheory.Limits.WalkingParallelFamily J} → [inst : DecidableEq J] → DecidableEq (CategoryTheory.Limits.WalkingParallelFamily.Hom J a a_1)

Equations

• CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom = CategoryTheory.Limits.WalkingParallelFamily.decEqHom✝

instance CategoryTheory.Limits.instInhabitedHomZero (J : Type v) : Inhabited (CategoryTheory.Limits.WalkingParallelFamily.Hom J CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.zero)

Satisfying the inhabited linter

Equations

• CategoryTheory.Limits.instInhabitedHomZero J = { default := CategoryTheory.Limits.WalkingParallelFamily.Hom.id CategoryTheory.Limits.WalkingParallelFamily.zero }

def CategoryTheory.Limits.WalkingParallelFamily.Hom.comp {J : Type w} {X : CategoryTheory.Limits.WalkingParallelFamily J} {Y : CategoryTheory.Limits.WalkingParallelFamily J} {Z : CategoryTheory.Limits.WalkingParallelFamily J} : CategoryTheory.Limits.WalkingParallelFamily.Hom J X Y → CategoryTheory.Limits.WalkingParallelFamily.Hom J Y Z → CategoryTheory.Limits.WalkingParallelFamily.Hom J X Z

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

Equations

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

instance CategoryTheory.Limits.WalkingParallelFamily.category {J : Type w} : CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingParallelFamily J)

Equations

• CategoryTheory.Limits.WalkingParallelFamily.category = CategoryTheory.Category.mk

@[simp]

theorem CategoryTheory.Limits.WalkingParallelFamily.hom_id {J : Type w} (X : CategoryTheory.Limits.WalkingParallelFamily J) : CategoryTheory.Limits.WalkingParallelFamily.Hom.id X = CategoryTheory.CategoryStruct.id X

def CategoryTheory.Limits.parallelFamily {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.parallelFamily_obj_zero {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) : (CategoryTheory.Limits.parallelFamily f).toPrefunctor.obj CategoryTheory.Limits.WalkingParallelFamily.zero = X

@[simp]

theorem CategoryTheory.Limits.parallelFamily_obj_one {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) : (CategoryTheory.Limits.parallelFamily f).toPrefunctor.obj CategoryTheory.Limits.WalkingParallelFamily.one = Y

@[simp]

theorem CategoryTheory.Limits.parallelFamily_map_left {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) {j : J} : (CategoryTheory.Limits.parallelFamily f).toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j) = f j

@[simp]

theorem CategoryTheory.Limits.diagramIsoParallelFamily_hom_app {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C) (X : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.diagramIsoParallelFamily F).hom.app X = CategoryTheory.eqToHom (_ : F.toPrefunctor.obj X = (CategoryTheory.Limits.parallelFamily fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)).toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.Limits.diagramIsoParallelFamily_inv_app {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C) (X : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.diagramIsoParallelFamily F).inv.app X = CategoryTheory.eqToHom (_ : (CategoryTheory.Limits.parallelFamily fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)).toPrefunctor.obj X = F.toPrefunctor.obj X)

def CategoryTheory.Limits.diagramIsoParallelFamily {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C) : F ≅ CategoryTheory.Limits.parallelFamily fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_obj (x : CategoryTheory.Limits.WalkingParallelPair) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.inverse.toPrefunctor.obj x = match x with | CategoryTheory.Limits.WalkingParallelPair.zero => CategoryTheory.Limits.WalkingParallelFamily.zero | CategoryTheory.Limits.WalkingParallelPair.one => CategoryTheory.Limits.WalkingParallelFamily.one

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_map : ∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y), CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.inverse.toPrefunctor.map h = match X, Y, h with | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => CategoryTheory.CategoryStruct.id (match x with | CategoryTheory.Limits.WalkingParallelPair.zero => CategoryTheory.Limits.WalkingParallelFamily.zero | CategoryTheory.Limits.WalkingParallelPair.one => CategoryTheory.Limits.WalkingParallelFamily.one) | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.left => CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := true } | .(CategoryTheory.Limits.WalkingParallelPair.zero), .(CategoryTheory.Limits.WalkingParallelPair.one), CategoryTheory.Limits.WalkingParallelPairHom.right => CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := false }

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_map {x : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)} {y : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)} (h : x ⟶ y) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.functor.toPrefunctor.map h = match x, y, h with | x, .(x), CategoryTheory.Limits.WalkingParallelFamily.Hom.id .(x) => CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.WalkingParallelFamily.rec CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one x) | .(CategoryTheory.Limits.WalkingParallelFamily.zero), .(CategoryTheory.Limits.WalkingParallelFamily.one), CategoryTheory.Limits.WalkingParallelFamily.Hom.line j => bif j.down then CategoryTheory.Limits.WalkingParallelPairHom.left else CategoryTheory.Limits.WalkingParallelPairHom.right

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_obj (x : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.functor.toPrefunctor.obj x = CategoryTheory.Limits.WalkingParallelFamily.rec CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one x

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app (X : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.unitIso.hom.app X = CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.id (CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool))).toPrefunctor.obj X = (CategoryTheory.Functor.comp (CategoryTheory.Limits.parallelFamily fun (p : ULift.{w, 0} Bool) => bif p.down then CategoryTheory.Limits.WalkingParallelPairHom.left else CategoryTheory.Limits.WalkingParallelPairHom.right) (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := true }) (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := false }))).toPrefunctor.obj X)

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app (X : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.unitIso.inv.app X = CategoryTheory.eqToHom (_ : (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := true }) (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := false })).toPrefunctor.obj ((CategoryTheory.Limits.parallelFamily fun (p : ULift.{w, 0} Bool) => bif p.down then CategoryTheory.Limits.WalkingParallelPairHom.left else CategoryTheory.Limits.WalkingParallelPairHom.right).toPrefunctor.obj X) = X)

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app (X : CategoryTheory.Limits.WalkingParallelPair) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.counitIso.inv.app X = CategoryTheory.eqToHom (_ : X = (CategoryTheory.Limits.parallelFamily fun (p : ULift.{w, 0} Bool) => bif p.down then CategoryTheory.Limits.WalkingParallelPairHom.left else CategoryTheory.Limits.WalkingParallelPairHom.right).toPrefunctor.obj ((CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := true }) (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := false })).toPrefunctor.obj X))

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app (X : CategoryTheory.Limits.WalkingParallelPair) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.counitIso.hom.app X = CategoryTheory.eqToHom (_ : (CategoryTheory.Functor.comp (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := true }) (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := false })) (CategoryTheory.Limits.parallelFamily fun (p : ULift.{w, 0} Bool) => bif p.down then CategoryTheory.Limits.WalkingParallelPairHom.left else CategoryTheory.Limits.WalkingParallelPairHom.right)).toPrefunctor.obj X = (CategoryTheory.Functor.id CategoryTheory.Limits.WalkingParallelPair).toPrefunctor.obj X)

def CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool) ≌ CategoryTheory.Limits.WalkingParallelPair

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

Equations

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

@[inline, reducible]

abbrev CategoryTheory.Limits.Trident {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) : Type (max (max w u) v)

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

Equations

• CategoryTheory.Limits.Trident f = CategoryTheory.Limits.Cone (CategoryTheory.Limits.parallelFamily f)

@[inline, reducible]

abbrev CategoryTheory.Limits.Cotrident {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) : Type (max (max w u) v)

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

Equations

• CategoryTheory.Limits.Cotrident f = CategoryTheory.Limits.Cocone (CategoryTheory.Limits.parallelFamily f)

@[inline, reducible]

abbrev CategoryTheory.Limits.Trident.ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (t : CategoryTheory.Limits.Trident f) : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).toPrefunctor.obj t.pt).toPrefunctor.obj CategoryTheory.Limits.WalkingParallelFamily.zero ⟶ (CategoryTheory.Limits.parallelFamily f).toPrefunctor.obj CategoryTheory.Limits.WalkingParallelFamily.zero

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

Equations

• CategoryTheory.Limits.Trident.ι t = t.π.app CategoryTheory.Limits.WalkingParallelFamily.zero

@[inline, reducible]

abbrev CategoryTheory.Limits.Cotrident.π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (t : CategoryTheory.Limits.Cotrident f) : (CategoryTheory.Limits.parallelFamily f).toPrefunctor.obj CategoryTheory.Limits.WalkingParallelFamily.one ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).toPrefunctor.obj t.pt).toPrefunctor.obj CategoryTheory.Limits.WalkingParallelFamily.one

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

Equations

• CategoryTheory.Limits.Cotrident.π t = t.ι.app CategoryTheory.Limits.WalkingParallelFamily.one

@[simp]

theorem CategoryTheory.Limits.Trident.ι_eq_app_zero {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (t : CategoryTheory.Limits.Trident f) : CategoryTheory.Limits.Trident.ι t = t.π.app CategoryTheory.Limits.WalkingParallelFamily.zero

@[simp]

theorem CategoryTheory.Limits.Cotrident.π_eq_app_one {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (t : CategoryTheory.Limits.Cotrident f) : CategoryTheory.Limits.Cotrident.π t = t.ι.app CategoryTheory.Limits.WalkingParallelFamily.one

@[simp]

theorem CategoryTheory.Limits.Trident.app_zero_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (s : CategoryTheory.Limits.Trident f) (j : J) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero) (CategoryTheory.CategoryStruct.comp (f j) h) = CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.one) h

@[simp]

theorem CategoryTheory.Limits.Trident.app_zero {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (s : CategoryTheory.Limits.Trident f) (j : J) : CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero) (f j) = s.π.app CategoryTheory.Limits.WalkingParallelFamily.one

@[simp]

theorem CategoryTheory.Limits.Cotrident.app_one_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (s : CategoryTheory.Limits.Cotrident f) (j : J) {Z : C} (h : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).toPrefunctor.obj s.pt).toPrefunctor.obj CategoryTheory.Limits.WalkingParallelFamily.one ⟶ Z) : CategoryTheory.CategoryStruct.comp (f j) (CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.one) h) = CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.zero) h

@[simp]

theorem CategoryTheory.Limits.Cotrident.app_one {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (s : CategoryTheory.Limits.Cotrident f) (j : J) : CategoryTheory.CategoryStruct.comp (f j) (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.one) = s.ι.app CategoryTheory.Limits.WalkingParallelFamily.zero

@[simp]

theorem CategoryTheory.Limits.Trident.ofι_π_app {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X✝ ⟶ Y)} [Nonempty J] {P : C} (ι : P ⟶ X✝) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) (X : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Trident.ofι ι w).π.app X = CategoryTheory.Limits.WalkingParallelFamily.casesOn X ι (CategoryTheory.CategoryStruct.comp ι (f (Classical.arbitrary J)))

@[simp]

theorem CategoryTheory.Limits.Trident.ofι_pt {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (ι : P ⟶ X) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) : (CategoryTheory.Limits.Trident.ofι ι w).pt = P

def CategoryTheory.Limits.Trident.ofι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (ι : P ⟶ X) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) : CategoryTheory.Limits.Trident f

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.Cotrident.ofπ_ι_app {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X✝ ⟶ Y)} [Nonempty J] {P : C} (π : Y ⟶ P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) (X : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Cotrident.ofπ π w).ι.app X = CategoryTheory.Limits.WalkingParallelFamily.casesOn X (CategoryTheory.CategoryStruct.comp (f (Classical.arbitrary J)) π) π

@[simp]

theorem CategoryTheory.Limits.Cotrident.ofπ_pt {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (π : Y ⟶ P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) : (CategoryTheory.Limits.Cotrident.ofπ π w).pt = P

def CategoryTheory.Limits.Cotrident.ofπ {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (π : Y ⟶ P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) : CategoryTheory.Limits.Cotrident f

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

Equations

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

theorem CategoryTheory.Limits.Trident.ι_ofι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (ι : P ⟶ X) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) : CategoryTheory.Limits.Trident.ι (CategoryTheory.Limits.Trident.ofι ι w) = ι

theorem CategoryTheory.Limits.Cotrident.π_ofπ {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (π : Y ⟶ P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) : CategoryTheory.Limits.Cotrident.π (CategoryTheory.Limits.Cotrident.ofπ π w) = π

theorem CategoryTheory.Limits.Trident.condition_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (j₁ : J) (j₂ : J) (t : CategoryTheory.Limits.Trident f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Trident.ι t) (CategoryTheory.CategoryStruct.comp (f j₁) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Trident.ι t) (CategoryTheory.CategoryStruct.comp (f j₂) h)

theorem CategoryTheory.Limits.Trident.condition {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (j₁ : J) (j₂ : J) (t : CategoryTheory.Limits.Trident f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Trident.ι t) (f j₁) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Trident.ι t) (f j₂)

theorem CategoryTheory.Limits.Cotrident.condition_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (j₁ : J) (j₂ : J) (t : CategoryTheory.Limits.Cotrident f) {Z : C} (h : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).toPrefunctor.obj t.pt).toPrefunctor.obj CategoryTheory.Limits.WalkingParallelFamily.one ⟶ Z) : CategoryTheory.CategoryStruct.comp (f j₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π t) h) = CategoryTheory.CategoryStruct.comp (f j₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π t) h)

theorem CategoryTheory.Limits.Cotrident.condition {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} (j₁ : J) (j₂ : J) (t : CategoryTheory.Limits.Cotrident f) : CategoryTheory.CategoryStruct.comp (f j₁) (CategoryTheory.Limits.Cotrident.π t) = CategoryTheory.CategoryStruct.comp (f j₂) (CategoryTheory.Limits.Cotrident.π t)

theorem CategoryTheory.Limits.Trident.equalizer_ext {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] (s : CategoryTheory.Limits.Trident f) {W : C} {k : W ⟶ s.pt} {l : W ⟶ s.pt} (h : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.Trident.ι s) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.Trident.ι s)) (j : CategoryTheory.Limits.WalkingParallelFamily J) : CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp 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 CategoryTheory.Limits.Cotrident.coequalizer_ext {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] (s : CategoryTheory.Limits.Cotrident f) {W : C} {k : s.pt ⟶ W} {l : s.pt ⟶ W} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π s) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π s) l) (j : CategoryTheory.Limits.WalkingParallelFamily J) : CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (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 CategoryTheory.Limits.Trident.IsLimit.hom_ext {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} {k : W ⟶ s.pt} {l : W ⟶ s.pt} (h : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.Trident.ι s) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.Trident.ι s)) : k = l

theorem CategoryTheory.Limits.Cotrident.IsColimit.hom_ext {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Cotrident f} (hs : CategoryTheory.Limits.IsColimit s) {W : C} {k : s.pt ⟶ W} {l : s.pt ⟶ W} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π s) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π s) l) : k = l

def CategoryTheory.Limits.Trident.IsLimit.lift' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) : { l : W ⟶ s.pt // CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.Trident.ι 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

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

def CategoryTheory.Limits.Cotrident.IsColimit.desc' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Cotrident f} (hs : CategoryTheory.Limits.IsColimit s) {W : C} (k : Y ⟶ W) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) : { l : s.pt ⟶ W // CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π 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

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

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

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

• CategoryTheory.Limits.Trident.IsLimit.mk t lift fac uniq = CategoryTheory.Limits.IsLimit.mk lift

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

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

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

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

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

• CategoryTheory.Limits.Cotrident.IsColimit.mk t desc fac uniq = CategoryTheory.Limits.IsColimit.mk desc

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

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

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

@[simp]

theorem CategoryTheory.Limits.Trident.IsLimit.homIso_symm_apply {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) (h : { h : Z ⟶ X // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp h (f j₁) = CategoryTheory.CategoryStruct.comp h (f j₂) }) : (CategoryTheory.Limits.Trident.IsLimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Trident.IsLimit.lift' ht ↑h (_ : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (↑h) (f j₁) = CategoryTheory.CategoryStruct.comp (↑h) (f j₂)))

@[simp]

theorem CategoryTheory.Limits.Trident.IsLimit.homIso_apply_coe {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) (k : Z ⟶ t.pt) : ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.Trident.ι t)

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

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

Equations

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

theorem CategoryTheory.Limits.Trident.IsLimit.homIso_natural {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) {Z : C} {Z' : C} (q : Z' ⟶ Z) (k : Z ⟶ t.pt) : ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp q k)) = CategoryTheory.CategoryStruct.comp q ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z) k)

The bijection of Trident.IsLimit.homIso is natural in Z.

@[simp]

theorem CategoryTheory.Limits.Cotrident.IsColimit.homIso_symm_apply {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Cotrident f} (ht : CategoryTheory.Limits.IsColimit t) (Z : C) (h : { h : Y ⟶ Z // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) h = CategoryTheory.CategoryStruct.comp (f j₂) h }) : (CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Cotrident.IsColimit.desc' ht ↑h (_ : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) ↑h = CategoryTheory.CategoryStruct.comp (f j₂) ↑h))

@[simp]

theorem CategoryTheory.Limits.Cotrident.IsColimit.homIso_apply_coe {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Cotrident f} (ht : CategoryTheory.Limits.IsColimit t) (Z : C) (k : t.pt ⟶ Z) : ↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π t) k

def CategoryTheory.Limits.Cotrident.IsColimit.homIso {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Cotrident f} (ht : CategoryTheory.Limits.IsColimit t) (Z : C) : (t.pt ⟶ Z) ≃ { h : Y ⟶ Z // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) h = CategoryTheory.CategoryStruct.comp (f j₂) h }

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

Equations

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

theorem CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Cotrident f} {Z : C} {Z' : C} (q : Z ⟶ Z') (ht : CategoryTheory.Limits.IsColimit t) (k : t.pt ⟶ Z) : ↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp k q)) = CategoryTheory.CategoryStruct.comp (↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z) k)) q

The bijection of Cotrident.IsColimit.homIso is natural in Z.

def CategoryTheory.Limits.Cone.ofTrident {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Trident fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) : CategoryTheory.Limits.Cone F

This is a helper construction that can be useful when verifying that a category has certain wide equalizers. Given F : WalkingParallelFamily ⥤ C, which is really the same as parallelFamily (λ 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 hasWideEqualizers_of_hasLimit_parallelFamily, which you may find to be an easier way of achieving your goal.

Equations

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

def CategoryTheory.Limits.Cocone.ofCotrident {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cotrident fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) : CategoryTheory.Limits.Cocone F

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

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.Cone.ofTrident_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Trident fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) (j : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Cone.ofTrident t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom (_ : (CategoryTheory.Limits.parallelFamily fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)).toPrefunctor.obj j = F.toPrefunctor.obj j))

@[simp]

theorem CategoryTheory.Limits.Cocone.ofCotrident_ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cotrident fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) (j : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Cocone.ofCotrident t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : F.toPrefunctor.obj j = (CategoryTheory.Limits.parallelFamily fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)).toPrefunctor.obj j)) (t.ι.app j)

def CategoryTheory.Limits.Trident.ofCone {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Trident fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)

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

Equations

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

def CategoryTheory.Limits.Cotrident.ofCocone {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cotrident fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.Trident.ofCone_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cone F) (j : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Trident.ofCone t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom (_ : F.toPrefunctor.obj j = (CategoryTheory.Limits.parallelFamily fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)).toPrefunctor.obj j))

@[simp]

theorem CategoryTheory.Limits.Cotrident.ofCocone_ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cocone F) (j : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Cotrident.ofCocone t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (CategoryTheory.Limits.parallelFamily fun (j : J) => F.toPrefunctor.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)).toPrefunctor.obj j = F.toPrefunctor.obj j)) (t.ι.app j)

@[simp]

theorem CategoryTheory.Limits.Trident.mkHom_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} {t : CategoryTheory.Limits.Trident f} (k : s.pt ⟶ t.pt) (w : autoParam (CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.Trident.ι t) = CategoryTheory.Limits.Trident.ι s) _auto✝) : (CategoryTheory.Limits.Trident.mkHom k).hom = k

def CategoryTheory.Limits.Trident.mkHom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} {t : CategoryTheory.Limits.Trident f} (k : s.pt ⟶ t.pt) (w : autoParam (CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.Trident.ι t) = CategoryTheory.Limits.Trident.ι s) _auto✝) : s ⟶ t

Helper function for constructing morphisms between wide equalizer tridents.

Equations

• CategoryTheory.Limits.Trident.mkHom k = CategoryTheory.Limits.ConeMorphism.mk k

@[simp]

theorem CategoryTheory.Limits.Trident.ext_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} {t : CategoryTheory.Limits.Trident f} (i : s.pt ≅ t.pt) (w : autoParam (CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.Trident.ι t) = CategoryTheory.Limits.Trident.ι s) _auto✝) : (CategoryTheory.Limits.Trident.ext i).hom = CategoryTheory.Limits.Trident.mkHom i.hom

@[simp]

theorem CategoryTheory.Limits.Trident.ext_inv {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} {t : CategoryTheory.Limits.Trident f} (i : s.pt ≅ t.pt) (w : autoParam (CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.Trident.ι t) = CategoryTheory.Limits.Trident.ι s) _auto✝) : (CategoryTheory.Limits.Trident.ext i).inv = CategoryTheory.Limits.Trident.mkHom i.inv

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

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

Equations

• CategoryTheory.Limits.Trident.ext i = CategoryTheory.Iso.mk (CategoryTheory.Limits.Trident.mkHom i.hom) (CategoryTheory.Limits.Trident.mkHom i.inv)

@[simp]

theorem CategoryTheory.Limits.Cotrident.mkHom_hom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Cotrident f} {t : CategoryTheory.Limits.Cotrident f} (k : s.pt ⟶ t.pt) (w : autoParam (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π s) k = CategoryTheory.Limits.Cotrident.π t) _auto✝) : (CategoryTheory.Limits.Cotrident.mkHom k).hom = k

def CategoryTheory.Limits.Cotrident.mkHom {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Cotrident f} {t : CategoryTheory.Limits.Cotrident f} (k : s.pt ⟶ t.pt) (w : autoParam (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cotrident.π s) k = CategoryTheory.Limits.Cotrident.π t) _auto✝) : s ⟶ t

Helper function for constructing morphisms between coequalizer cotridents.

Equations

• CategoryTheory.Limits.Cotrident.mkHom k = CategoryTheory.Limits.CoconeMorphism.mk k

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

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

Equations

• CategoryTheory.Limits.Cotrident.ext i = CategoryTheory.Iso.mk (CategoryTheory.Limits.Cotrident.mkHom i.hom) (CategoryTheory.Limits.Cotrident.mkHom i.inv)

@[inline, reducible]

abbrev CategoryTheory.Limits.HasWideEqualizer {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) : Prop

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

Equations

• CategoryTheory.Limits.HasWideEqualizer f = CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelFamily f)

@[inline, reducible]

abbrev CategoryTheory.Limits.wideEqualizer {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] : C

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

Equations

• CategoryTheory.Limits.wideEqualizer f = CategoryTheory.Limits.limit (CategoryTheory.Limits.parallelFamily f)

@[inline, reducible]

abbrev CategoryTheory.Limits.wideEqualizer.ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] : CategoryTheory.Limits.wideEqualizer f ⟶ X

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

Equations

• CategoryTheory.Limits.wideEqualizer.ι f = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.parallelFamily f) CategoryTheory.Limits.WalkingParallelFamily.zero

@[inline, reducible]

abbrev CategoryTheory.Limits.wideEqualizer.trident {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] : CategoryTheory.Limits.Trident f

A wide equalizer cone for a parallel family f.

Equations

• CategoryTheory.Limits.wideEqualizer.trident f = CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelFamily f)

@[simp]

theorem CategoryTheory.Limits.wideEqualizer.trident_ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] : CategoryTheory.Limits.Trident.ι (CategoryTheory.Limits.wideEqualizer.trident f) = CategoryTheory.Limits.wideEqualizer.ι f

@[simp]

theorem CategoryTheory.Limits.wideEqualizer.trident_π_app_zero {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] : (CategoryTheory.Limits.wideEqualizer.trident f).π.app CategoryTheory.Limits.WalkingParallelFamily.zero = CategoryTheory.Limits.wideEqualizer.ι f

theorem CategoryTheory.Limits.wideEqualizer.condition_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] (j₁ : J) (j₂ : J) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (CategoryTheory.CategoryStruct.comp (f j₁) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (CategoryTheory.CategoryStruct.comp (f j₂) h)

theorem CategoryTheory.Limits.wideEqualizer.condition {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] (j₁ : J) (j₂ : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (f j₁) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (f j₂)

def CategoryTheory.Limits.wideEqualizerIsWideEqualizer {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Trident.ofι (CategoryTheory.Limits.wideEqualizer.ι f) (_ : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (f j₁) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) (f j₂)))

The wideEqualizer built from wideEqualizer.ι f is limiting.

Equations

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

@[inline, reducible]

abbrev CategoryTheory.Limits.wideEqualizer.lift {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] {W : C} (k : W ⟶ X) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) : W ⟶ CategoryTheory.Limits.wideEqualizer f

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

Equations

• CategoryTheory.Limits.wideEqualizer.lift k h = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.parallelFamily f) (CategoryTheory.Limits.Trident.ofι k h)

@[simp]

theorem CategoryTheory.Limits.wideEqualizer.lift_ι_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] {W : C} (k : W ⟶ X) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.lift k h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.ι f) h) = CategoryTheory.CategoryStruct.comp k h

@[simp]

theorem CategoryTheory.Limits.wideEqualizer.lift_ι {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] {W : C} (k : W ⟶ X) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.lift k h) (CategoryTheory.Limits.wideEqualizer.ι f) = k

def CategoryTheory.Limits.wideEqualizer.lift' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] {W : C} (k : W ⟶ X) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) : { l : W ⟶ CategoryTheory.Limits.wideEqualizer f // CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.wideEqualizer.ι f) = k }

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

Equations

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

theorem CategoryTheory.Limits.wideEqualizer.hom_ext {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] {W : C} {k : W ⟶ CategoryTheory.Limits.wideEqualizer f} {l : W ⟶ CategoryTheory.Limits.wideEqualizer f} (h : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.wideEqualizer.ι f) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.wideEqualizer.ι f)) : k = l

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

instance CategoryTheory.Limits.wideEqualizer.ι_mono {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] : CategoryTheory.Mono (CategoryTheory.Limits.wideEqualizer.ι f)

A wide equalizer morphism is a monomorphism

Equations

• (_ : CategoryTheory.Mono (CategoryTheory.Limits.wideEqualizer.ι f)) = (_ : CategoryTheory.Mono (CategoryTheory.Limits.wideEqualizer.ι f))

theorem CategoryTheory.Limits.mono_of_isLimit_parallelFamily {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {c : CategoryTheory.Limits.Cone (CategoryTheory.Limits.parallelFamily f)} (i : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Mono (CategoryTheory.Limits.Trident.ι c)

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

@[inline, reducible]

abbrev CategoryTheory.Limits.HasWideCoequalizer {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) : Prop

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

Equations

• CategoryTheory.Limits.HasWideCoequalizer f = CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelFamily f)

@[inline, reducible]

abbrev CategoryTheory.Limits.wideCoequalizer {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] : C

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

Equations

• CategoryTheory.Limits.wideCoequalizer f = CategoryTheory.Limits.colimit (CategoryTheory.Limits.parallelFamily f)

@[inline, reducible]

abbrev CategoryTheory.Limits.wideCoequalizer.π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] : Y ⟶ CategoryTheory.Limits.wideCoequalizer f

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

Equations

• CategoryTheory.Limits.wideCoequalizer.π f = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.parallelFamily f) CategoryTheory.Limits.WalkingParallelFamily.one

@[inline, reducible]

abbrev CategoryTheory.Limits.wideCoequalizer.cotrident {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] : CategoryTheory.Limits.Cotrident f

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

Equations

• CategoryTheory.Limits.wideCoequalizer.cotrident f = CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelFamily f)

@[simp]

theorem CategoryTheory.Limits.wideCoequalizer.cotrident_π {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] : CategoryTheory.Limits.Cotrident.π (CategoryTheory.Limits.wideCoequalizer.cotrident f) = CategoryTheory.Limits.wideCoequalizer.π f

@[simp]

theorem CategoryTheory.Limits.wideCoequalizer.cotrident_ι_app_one {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] : (CategoryTheory.Limits.wideCoequalizer.cotrident f).ι.app CategoryTheory.Limits.WalkingParallelFamily.one = CategoryTheory.Limits.wideCoequalizer.π f

theorem CategoryTheory.Limits.wideCoequalizer.condition_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] (j₁ : J) (j₂ : J) {Z : C} (h : CategoryTheory.Limits.wideCoequalizer f ⟶ Z) : CategoryTheory.CategoryStruct.comp (f j₁) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) h) = CategoryTheory.CategoryStruct.comp (f j₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) h)

theorem CategoryTheory.Limits.wideCoequalizer.condition {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] (j₁ : J) (j₂ : J) : CategoryTheory.CategoryStruct.comp (f j₁) (CategoryTheory.Limits.wideCoequalizer.π f) = CategoryTheory.CategoryStruct.comp (f j₂) (CategoryTheory.Limits.wideCoequalizer.π f)

def CategoryTheory.Limits.wideCoequalizerIsWideCoequalizer {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cotrident.ofπ (CategoryTheory.Limits.wideCoequalizer.π f) (_ : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) (CategoryTheory.Limits.wideCoequalizer.π f) = CategoryTheory.CategoryStruct.comp (f j₂) (CategoryTheory.Limits.wideCoequalizer.π f)))

The cotrident built from wideCoequalizer.π f is colimiting.

Equations

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

@[inline, reducible]

abbrev CategoryTheory.Limits.wideCoequalizer.desc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] {W : C} (k : Y ⟶ W) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) : CategoryTheory.Limits.wideCoequalizer f ⟶ W

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

Equations

• CategoryTheory.Limits.wideCoequalizer.desc k h = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelFamily f) (CategoryTheory.Limits.Cotrident.ofπ k h)

@[simp]

theorem CategoryTheory.Limits.wideCoequalizer.π_desc_assoc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] {W : C} (k : Y ⟶ W) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) {Z : C} (h : W ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.desc k h✝) h) = CategoryTheory.CategoryStruct.comp k h

@[simp]

theorem CategoryTheory.Limits.wideCoequalizer.π_desc {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] {W : C} (k : Y ⟶ W) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) (CategoryTheory.Limits.wideCoequalizer.desc k h) = k

def CategoryTheory.Limits.wideCoequalizer.desc' {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] {W : C} (k : Y ⟶ W) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) : { l : CategoryTheory.Limits.wideCoequalizer f ⟶ W // CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) l = k }

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

Equations

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

theorem CategoryTheory.Limits.wideCoequalizer.hom_ext {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] {W : C} {k : CategoryTheory.Limits.wideCoequalizer f ⟶ W} {l : CategoryTheory.Limits.wideCoequalizer f ⟶ W} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) l) : k = l

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

instance CategoryTheory.Limits.wideCoequalizer.π_epi {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : J → (X ⟶ Y)} [CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] : CategoryTheory.Epi (CategoryTheory.Limits.wideCoequalizer.π f)

A wide coequalizer morphism is an epimorphism

Equations

• (_ : CategoryTheory.Epi (CategoryTheory.Limits.wideCoequalizer.π f)) = (_ : CategoryTheory.Epi (CategoryTheory.Limits.wideCoequalizer.π f))

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

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

@[inline, reducible]

abbrev CategoryTheory.Limits.HasWideEqualizers (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

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

Equations

• CategoryTheory.Limits.HasWideEqualizers C = ∀ (J : Type w), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingParallelFamily J) C

@[inline, reducible]

abbrev CategoryTheory.Limits.HasWideCoequalizers (C : Type u) [CategoryTheory.Category.{v, u} C] : Prop

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

Equations

• CategoryTheory.Limits.HasWideCoequalizers C = ∀ (J : Type w), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Limits.WalkingParallelFamily J) C

theorem CategoryTheory.Limits.hasWideEqualizers_of_hasLimit_parallelFamily (C : Type u) [CategoryTheory.Category.{v, u} C] [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelFamily f)] : CategoryTheory.Limits.HasWideEqualizers C

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

theorem CategoryTheory.Limits.hasWideCoequalizers_of_hasColimit_parallelFamily (C : Type u) [CategoryTheory.Category.{v, u} C] [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelFamily f)] : CategoryTheory.Limits.HasWideCoequalizers C

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

instance CategoryTheory.Limits.hasEqualizers_of_hasWideEqualizers (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWideEqualizers C] : CategoryTheory.Limits.HasEqualizers C

Equations

• (_ : CategoryTheory.Limits.HasEqualizers C) = (_ : CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C)

instance CategoryTheory.Limits.hasCoequalizers_of_hasWideCoequalizers (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWideCoequalizers C] : CategoryTheory.Limits.HasCoequalizers C

Equations

• (_ : CategoryTheory.Limits.HasCoequalizers C) = (_ : CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair C)