mathlib documentation

category_theory.limits.shapes.wide_equalizers

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 #

Each of these has a dual.

Main statements #

Implementation notes #

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

References #

inductive category_theory.limits.walking_parallel_family (J : Type w) :
Type w

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

Instances for category_theory.limits.walking_parallel_family

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

Instances for category_theory.limits.walking_parallel_family.hom

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

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

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

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

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

@[reducible]

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

@[reducible]

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

noncomputable def category_theory.limits.trident.of_ι {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {P : C} (ι : P X) (w : ∀ (j₁ j₂ : J), ι f j₁ = ι f j₂) :

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

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

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

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

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

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

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

theorem category_theory.limits.trident.is_limit.hom_ext {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s : category_theory.limits.trident f} (hs : category_theory.limits.is_limit s) {W : C} {k l : W s.X} (h : k s.ι = l s.ι) :
k = l
theorem category_theory.limits.cotrident.is_colimit.hom_ext {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s : category_theory.limits.cotrident f} (hs : category_theory.limits.is_colimit s) {W : C} {k l : s.X W} (h : s.π k = s.π l) :
k = l
noncomputable def category_theory.limits.trident.is_limit.lift' {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s : category_theory.limits.trident f} (hs : category_theory.limits.is_limit s) {W : C} (k : W X) (h : ∀ (j₁ j₂ : J), k f j₁ = k f j₂) :
{l // l s.ι = k}

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

Equations
noncomputable def category_theory.limits.cotrident.is_colimit.desc' {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s : category_theory.limits.cotrident f} (hs : category_theory.limits.is_colimit s) {W : C} (k : Y W) (h : ∀ (j₁ j₂ : J), f j₁ k = f j₂ k) :
{l // s.π l = k}

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

Equations
def category_theory.limits.trident.is_limit.mk {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] (t : category_theory.limits.trident f) (lift : Π (s : category_theory.limits.trident f), s.X t.X) (fac : ∀ (s : category_theory.limits.trident f), lift s t.ι = s.ι) (uniq : ∀ (s : category_theory.limits.trident f) (m : s.X t.X), (∀ (j : category_theory.limits.walking_parallel_family J), m t.π.app j = s.π.app j)m = lift s) :

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

Equations

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
def category_theory.limits.cotrident.is_colimit.mk {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] (t : category_theory.limits.cotrident f) (desc : Π (s : category_theory.limits.cotrident f), t.X s.X) (fac : ∀ (s : category_theory.limits.cotrident f), t.π desc s = s.π) (uniq : ∀ (s : category_theory.limits.cotrident f) (m : t.X s.X), (∀ (j : category_theory.limits.walking_parallel_family J), t.ι.app j m = s.ι.app j)m = desc s) :

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

Equations

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
noncomputable def category_theory.limits.trident.is_limit.hom_iso {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {t : category_theory.limits.trident f} (ht : category_theory.limits.is_limit t) (Z : C) :
(Z t.X) {h // ∀ (j₁ j₂ : J), h f j₁ = h f j₂}

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

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

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

noncomputable def category_theory.limits.cotrident.is_colimit.hom_iso {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {t : category_theory.limits.cotrident f} (ht : category_theory.limits.is_colimit t) (Z : C) :
(t.X Z) {h // ∀ (j₁ j₂ : J), f j₁ h = f j₂ h}

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

Equations
@[simp]

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

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

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

Equations

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

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

Equations

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

Equations

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

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

Helper function for constructing morphisms between wide equalizer tridents.

Equations
@[simp]
theorem category_theory.limits.trident.mk_hom_hom {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s t : category_theory.limits.trident f} (k : s.X t.X) (w : k t.ι = s.ι) :
@[simp]
theorem category_theory.limits.trident.ext_hom {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s t : category_theory.limits.trident f} (i : s.X t.X) (w : i.hom t.ι = s.ι) :
@[simp]
theorem category_theory.limits.trident.ext_inv {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s t : category_theory.limits.trident f} (i : s.X t.X) (w : i.hom t.ι = s.ι) :
def category_theory.limits.trident.ext {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s t : category_theory.limits.trident f} (i : s.X t.X) (w : i.hom t.ι = s.ι) :
s t

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

Equations
def category_theory.limits.cotrident.mk_hom {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s t : category_theory.limits.cotrident f} (k : s.X t.X) (w : s.π k = t.π) :
s t

Helper function for constructing morphisms between coequalizer cotridents.

Equations
@[simp]
theorem category_theory.limits.cotrident.mk_hom_hom {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s t : category_theory.limits.cotrident f} (k : s.X t.X) (w : s.π k = t.π) :
def category_theory.limits.cotrident.ext {J : Type w} {C : Type u} [category_theory.category C] {X Y : C} {f : J → (X Y)} [nonempty J] {s t : category_theory.limits.cotrident f} (i : s.X t.X) (w : s.π i.hom = t.π) :
s t

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

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

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

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

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

@[reducible]

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

@[reducible]

A wide equalizer cone for a parallel family f.

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

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

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

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

Equations
@[ext]

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

@[protected, instance]

A wide equalizer morphism is a monomorphism

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

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

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

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

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

@[reducible]

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

@[reducible]

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

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

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

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

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

Equations
@[ext]

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

@[protected, instance]

A wide coequalizer morphism is an epimorphism

@[reducible]

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

@[reducible]

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

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

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