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

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} : WalkingParallelFamily J
• one {J : Type w} : WalkingParallelFamily J

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

Equations

• CategoryTheory.Limits.instDecidableEqWalkingParallelFamily CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.zero = isTrue ⋯
• CategoryTheory.Limits.instDecidableEqWalkingParallelFamily CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.one = isFalse ⋯
• CategoryTheory.Limits.instDecidableEqWalkingParallelFamily CategoryTheory.Limits.WalkingParallelFamily.one CategoryTheory.Limits.WalkingParallelFamily.zero = isFalse ⋯
• CategoryTheory.Limits.instDecidableEqWalkingParallelFamily CategoryTheory.Limits.WalkingParallelFamily.one CategoryTheory.Limits.WalkingParallelFamily.one = isTrue ⋯

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

Equations

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

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

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

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

instance CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom {J✝ : Type u_1} {a✝ a✝¹ : WalkingParallelFamily J✝} [DecidableEq J✝] : DecidableEq (Hom J✝ a✝ a✝¹)

Equations

• CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom = CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom.decEq

def CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom.decEq {J✝ : Type u_1} {a✝ a✝¹ : WalkingParallelFamily J✝} [DecidableEq J✝] (x✝ x✝¹ : Hom J✝ a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom.decEq (CategoryTheory.Limits.WalkingParallelFamily.Hom.id a✝) (CategoryTheory.Limits.WalkingParallelFamily.Hom.id a✝) = isTrue ⋯

instance CategoryTheory.Limits.instInhabitedHomZero (J : Type v) : Inhabited (WalkingParallelFamily.Hom J WalkingParallelFamily.zero 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 Y Z : WalkingParallelFamily J} : Hom J X Y → Hom J Y Z → 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.
• (CategoryTheory.Limits.WalkingParallelFamily.Hom.id x✝²).comp x✝ = x✝

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

Equations

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

@[simp]

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

def CategoryTheory.Limits.WalkingParallelFamily.arrowEquiv (J : Type w) : Arrow (WalkingParallelFamily J) ≃ Option (Option J)

Arrow (WalkingParallelFamily J) identifies to the type obtained by adding two elements to T.

Equations

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

def CategoryTheory.Limits.parallelFamily {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) : Functor (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} [Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) : (parallelFamily f).obj WalkingParallelFamily.zero = X

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.Limits.diagramIsoParallelFamily F = CategoryTheory.NatIso.ofComponents (fun (j : CategoryTheory.Limits.WalkingParallelFamily J) => CategoryTheory.eqToIso ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.diagramIsoParallelFamily_hom_app {J : Type w} {C : Type u} [Category.{v, u} C] (F : Functor (WalkingParallelFamily J) C) (X : WalkingParallelFamily J) : (diagramIsoParallelFamily F).hom.app X = eqToHom ⋯

@[simp]

theorem CategoryTheory.Limits.diagramIsoParallelFamily_inv_app {J : Type w} {C : Type u} [Category.{v, u} C] (F : Functor (WalkingParallelFamily J) C) (X : WalkingParallelFamily J) : (diagramIsoParallelFamily F).inv.app X = eqToHom ⋯

def CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair : WalkingParallelFamily (ULift.{w, 0} Bool) ≌ 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.

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app (X : WalkingParallelFamily (ULift.{w, 0} Bool)) : walkingParallelFamilyEquivWalkingParallelPair.unitIso.inv.app X = eqToHom ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app (X : WalkingParallelFamily (ULift.{w, 0} Bool)) : walkingParallelFamilyEquivWalkingParallelPair.unitIso.hom.app X = eqToHom ⋯

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app (X : WalkingParallelPair) : walkingParallelFamilyEquivWalkingParallelPair.counitIso.hom.app X = eqToHom ⋯

@[simp]

theorem CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app (X : WalkingParallelPair) : walkingParallelFamilyEquivWalkingParallelPair.counitIso.inv.app X = eqToHom ⋯

@[simp]

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

@[reducible, inline]

abbrev CategoryTheory.Limits.Trident {J : Type w} {C : Type u} [Category.{v, u} C] {X 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)

@[reducible, inline]

abbrev CategoryTheory.Limits.Cotrident {J : Type w} {C : Type u} [Category.{v, u} C] {X 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)

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Trident.ofι {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (ι : P ⟶ X) (w : ∀ (j₁ j₂ : J), CategoryStruct.comp ι (f j₁) = CategoryStruct.comp ι (f j₂)) : 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.Trident.ofι_pt {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (ι : P ⟶ X) (w : ∀ (j₁ j₂ : J), CategoryStruct.comp ι (f j₁) = CategoryStruct.comp ι (f j₂)) : (ofι ι w).pt = P

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

Equations

• CategoryTheory.Limits.Trident.IsLimit.lift' hs k h = ⟨hs.lift (CategoryTheory.Limits.Trident.ofι k h), ⋯⟩

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

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

Equations

• CategoryTheory.Limits.Cotrident.IsColimit.desc' hs k h = ⟨hs.desc (CategoryTheory.Limits.Cotrident.ofπ k h), ⋯⟩

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

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

• CategoryTheory.Limits.Trident.IsLimit.mk' t create = CategoryTheory.Limits.Trident.IsLimit.mk t (fun (s : CategoryTheory.Limits.Trident f) => ↑(create s)) ⋯ ⋯

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

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

• CategoryTheory.Limits.Cotrident.IsColimit.mk' t create = CategoryTheory.Limits.Cotrident.IsColimit.mk t (fun (s : CategoryTheory.Limits.Cotrident f) => ↑(create s)) ⋯ ⋯

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : Cotrident f} {Z Z' : C} (q : Z ⟶ Z') (ht : IsColimit t) (k : t.pt ⟶ Z) : ↑((homIso ht Z') (CategoryStruct.comp k q)) = CategoryStruct.comp (↑((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} [Category.{v, u} C] {F : Functor (WalkingParallelFamily J) C} (t : Trident fun (j : J) => F.map (WalkingParallelFamily.Hom.line j)) : 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 (fun j ↦ F.map (line j)), and a trident on fun j ↦ F.map (line j), we get a cone on F.

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

Equations

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

def CategoryTheory.Limits.Cocone.ofCotrident {J : Type w} {C : Type u} [Category.{v, u} C] {F : Functor (WalkingParallelFamily J) C} (t : Cotrident fun (j : J) => F.map (WalkingParallelFamily.Hom.line j)) : 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} [Category.{v, u} C] {F : Functor (WalkingParallelFamily J) C} (t : Trident fun (j : J) => F.map (WalkingParallelFamily.Hom.line j)) (j : WalkingParallelFamily J) : (ofTrident t).π.app j = CategoryStruct.comp (t.π.app j) (eqToHom ⋯)

@[simp]

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

def CategoryTheory.Limits.Trident.ofCone {J : Type w} {C : Type u} [Category.{v, u} C] {F : Functor (WalkingParallelFamily J) C} (t : Cone F) : Trident fun (j : J) => F.map (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} [Category.{v, u} C] {F : Functor (WalkingParallelFamily J) C} (t : Cocone F) : Cotrident fun (j : J) => F.map (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} [Category.{v, u} C] {F : Functor (WalkingParallelFamily J) C} (t : Cone F) (j : WalkingParallelFamily J) : (ofCone t).π.app j = CategoryStruct.comp (t.π.app j) (eqToHom ⋯)

@[simp]

theorem CategoryTheory.Limits.Cotrident.ofCocone_ι {J : Type w} {C : Type u} [Category.{v, u} C] {F : Functor (WalkingParallelFamily J) C} (t : Cocone F) (j : WalkingParallelFamily J) : (ofCocone t).ι.app j = CategoryStruct.comp (eqToHom ⋯) (t.ι.app j)

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

Helper function for constructing morphisms between wide equalizer tridents.

Equations

• CategoryTheory.Limits.Trident.mkHom k w = { hom := k, w := ⋯ }

@[simp]

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

def CategoryTheory.Limits.Trident.ext {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : Trident f} (i : s.pt ≅ t.pt) (w : CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : 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 w = { hom := CategoryTheory.Limits.Trident.mkHom i.hom w, inv := CategoryTheory.Limits.Trident.mkHom i.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

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

Helper function for constructing morphisms between coequalizer cotridents.

Equations

• CategoryTheory.Limits.Cotrident.mkHom k w = { hom := k, w := ⋯ }

@[simp]

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

def CategoryTheory.Limits.Cotrident.ext {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : Cotrident f} (i : s.pt ≅ t.pt) (w : CategoryStruct.comp s.π i.hom = t.π := by cat_disch) : 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 w = { hom := CategoryTheory.Limits.Cotrident.mkHom i.hom w, inv := CategoryTheory.Limits.Cotrident.mkHom i.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[reducible, inline]

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

A family f of parallel morphisms has a wide equalizer if the diagram parallelFamily f has a limit.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.wideEqualizer {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [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)

@[reducible, inline]

abbrev CategoryTheory.Limits.wideEqualizer.ι {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [HasWideEqualizer f] : 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

@[reducible, inline]

abbrev CategoryTheory.Limits.wideEqualizer.trident {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [HasWideEqualizer f] : 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)

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

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

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

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

def CategoryTheory.Limits.wideEqualizerIsWideEqualizer {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [HasWideEqualizer f] [Nonempty J] : IsLimit (Trident.ofι (wideEqualizer.ι f) ⋯)

The wideEqualizer built from wideEqualizer.ι f is limiting.

Equations

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

@[reducible, inline]

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

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

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

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

• CategoryTheory.Limits.wideEqualizer.lift' k h = ⟨CategoryTheory.Limits.wideEqualizer.lift k h, ⋯⟩

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

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

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

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

A wide equalizer morphism is a monomorphism

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

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

@[reducible, inline]

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

A family f of parallel morphisms has a wide coequalizer if the diagram parallelFamily f has a colimit.

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Limits.wideCoequalizer.π {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [HasWideCoequalizer f] : Y ⟶ 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

@[reducible, inline]

abbrev CategoryTheory.Limits.wideCoequalizer.cotrident {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [HasWideCoequalizer f] : 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)

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

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

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

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

def CategoryTheory.Limits.wideCoequalizerIsWideCoequalizer {J : Type w} {C : Type u} [Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [HasWideCoequalizer f] [Nonempty J] : IsColimit (Cotrident.ofπ (wideCoequalizer.π f) ⋯)

The cotrident built from wideCoequalizer.π f is colimiting.

Equations

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

@[reducible, inline]

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

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

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

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

• CategoryTheory.Limits.wideCoequalizer.desc' k h = ⟨CategoryTheory.Limits.wideCoequalizer.desc k h, ⋯⟩

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

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

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

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

A wide coequalizer morphism is an epimorphism

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

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

@[reducible, inline]

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

A category HasWideEqualizers if it has all limits of shape WalkingParallelFamily J, i.e. if it has a wide equalizer for every family of parallel morphisms.

Equations

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

@[reducible, inline]

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

A category HasWideCoequalizers if it has all colimits of shape WalkingParallelFamily J, i.e. if it has a wide coequalizer for every family of parallel morphisms.

Equations

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

theorem CategoryTheory.Limits.hasWideEqualizers_of_hasLimit_parallelFamily (C : Type u) [Category.{v, u} C] [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, HasLimit (parallelFamily f)] : 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) [Category.{v, u} C] [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, HasColimit (parallelFamily f)] : HasWideCoequalizers C

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

@[instance 10]

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

@[instance 10]

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