Coequalizers in Type

The coequalizer of a pair of maps (f, g) from X to Y is the quotient of Y by ∀ x : Y, f x ~ g x

def CategoryTheory.Limits.Types.coequalizerColimit {X Y : Type u} (f g : X ⟶ Y) : ColimitCocone (parallelPair f g)

Show that the quotient by the relation generated by f(x) ~ g(x) is a coequalizer for the pair (f, g).

Equations

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

theorem CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq {X Y Z : Type u} (f g : X ⟶ Y) (π : Y ⟶ Z) (e : CategoryStruct.comp f π = CategoryStruct.comp g π) (h : IsColimit (Cofork.ofπ π e)) (U : Set Y) (H : ⇑(ConcreteCategory.hom f) ⁻¹' U = ⇑(ConcreteCategory.hom g) ⁻¹' U) : ⇑(ConcreteCategory.hom π) ⁻¹' ⇑(ConcreteCategory.hom π) '' U = U

If π : Y ⟶ Z is a coequalizer for (f, g), and U ⊆ Y such that f ⁻¹' U = g ⁻¹' U, then π ⁻¹' π '' U = U.

noncomputable def CategoryTheory.Limits.Types.coequalizerIso {X Y : Type u} (f g : X ⟶ Y) : coequalizer f g ≅ Function.Coequalizer ⇑(ConcreteCategory.hom f) ⇑(ConcreteCategory.hom g)

The categorical coequalizer in Type u is the quotient by f g ~ g x.

Equations

• CategoryTheory.Limits.Types.coequalizerIso f g = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coequalizerColimit f g)

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom {X Y : Type u} (f g : X ⟶ Y) : CategoryStruct.comp (coequalizer.π f g) (coequalizerIso f g).hom = TypeCat.ofHom (Function.Coequalizer.mk ⇑(ConcreteCategory.hom f) ⇑(ConcreteCategory.hom g))

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom_apply {X Y : Type u} (f g : X ⟶ Y) (x : Y) : (ConcreteCategory.hom (coequalizerIso f g).hom) ((ConcreteCategory.hom (coequalizer.π f g)) x) = Function.Coequalizer.mk (⇑(ConcreteCategory.hom f)) (⇑(ConcreteCategory.hom g)) x

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv {X Y : Type u} (f g : X ⟶ Y) : CategoryStruct.comp (TypeCat.ofHom (Function.Coequalizer.mk ⇑(ConcreteCategory.hom f) ⇑(ConcreteCategory.hom g))) (coequalizerIso f g).inv = coequalizer.π f g

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv_apply {X Y : Type u} (f g : X ⟶ Y) (x : Y) : (ConcreteCategory.hom (coequalizerIso f g).inv) (Function.Coequalizer.mk (⇑(ConcreteCategory.hom f)) (⇑(ConcreteCategory.hom g)) x) = (ConcreteCategory.hom (coequalizer.π f g)) x