Equalizers as pullbacks of products

Also see CategoryTheory.Limits.Constructions.Equalizers for very similar results.

theorem CategoryTheory.Limits.isPullback_equalizer_prod {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasEqualizer f g] [HasBinaryProduct Y Y] : IsPullback (equalizer.ι f g) (CategoryStruct.comp (equalizer.ι f g) f) (prod.lift f g) (prod.lift (CategoryStruct.id Y) (CategoryStruct.id Y))

The equalizer of f g : X ⟶ Y is the pullback of the diagonal map Y ⟶ Y × Y along the map (f, g) : X ⟶ Y × Y.

theorem CategoryTheory.Limits.isPushout_coequalizer_coprod {C : Type u} [Category.{v, u} C] {X Y : C} (f g : X ⟶ Y) [HasCoequalizer f g] [HasBinaryCoproduct X X] : IsPushout (coprod.desc f g) (coprod.desc (CategoryStruct.id X) (CategoryStruct.id X)) (coequalizer.π f g) (CategoryStruct.comp f (coequalizer.π f g))

The coequalizer of f g : X ⟶ Y is the pushout of the diagonal map X ⨿ X ⟶ X along the map (f, g) : X ⨿ X ⟶ Y.

noncomputable def CategoryTheory.Limits.equalizerPullbackMapIso {C : Type u} [Category.{v, u} C] [HasEqualizers C] [HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) : equalizer (pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) ≅ pullback (equalizer.ι f g) (pullback.fst s v)

The natural isomorphism eq(f ×[S] T, g ×[S] T) ≅ eq(f, g) ×[S] T.

Equations

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

@[simp]

theorem CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst {C : Type u} [Category.{v, u} C] [HasEqualizers C] [HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) : CategoryStruct.comp (equalizerPullbackMapIso hf hg v).hom (CategoryStruct.comp (pullback.fst (equalizer.ι f g) (pullback.fst s v)) (equalizer.ι f g)) = CategoryStruct.comp (equalizer.ι (pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯)) (pullback.fst s v)

@[simp]

theorem CategoryTheory.Limits.equalizerPullbackMapIso_hom_fst_assoc {C : Type u} [Category.{v, u} C] [HasEqualizers C] [HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (equalizerPullbackMapIso hf hg v).hom (CategoryStruct.comp (pullback.fst (equalizer.ι f g) (pullback.fst s v)) (CategoryStruct.comp (equalizer.ι f g) h)) = CategoryStruct.comp (equalizer.ι (pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯)) (CategoryStruct.comp (pullback.fst s v) h)

@[simp]

theorem CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd {C : Type u} [Category.{v, u} C] [HasEqualizers C] [HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) : CategoryStruct.comp (equalizerPullbackMapIso hf hg v).hom (pullback.snd (equalizer.ι f g) (pullback.fst s v)) = equalizer.ι (pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯)

@[simp]

theorem CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd_assoc {C : Type u} [Category.{v, u} C] [HasEqualizers C] [HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) {Z : C} (h : pullback s v ⟶ Z) : CategoryStruct.comp (equalizerPullbackMapIso hf hg v).hom (CategoryStruct.comp (pullback.snd (equalizer.ι f g) (pullback.fst s v)) h) = CategoryStruct.comp (equalizer.ι (pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯)) h

@[simp]

theorem CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst {C : Type u} [Category.{v, u} C] [HasEqualizers C] [HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) : CategoryStruct.comp (equalizerPullbackMapIso hf hg v).inv (CategoryStruct.comp (equalizer.ι (pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯)) (pullback.fst s v)) = CategoryStruct.comp (pullback.fst (equalizer.ι f g) (pullback.fst s v)) (equalizer.ι f g)

@[simp]

theorem CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_fst_assoc {C : Type u} [Category.{v, u} C] [HasEqualizers C] [HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (equalizerPullbackMapIso hf hg v).inv (CategoryStruct.comp (equalizer.ι (pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯)) (CategoryStruct.comp (pullback.fst s v) h)) = CategoryStruct.comp (pullback.fst (equalizer.ι f g) (pullback.fst s v)) (CategoryStruct.comp (equalizer.ι f g) h)

@[simp]

theorem CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd {C : Type u} [Category.{v, u} C] [HasEqualizers C] [HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) : CategoryStruct.comp (equalizerPullbackMapIso hf hg v).inv (CategoryStruct.comp (equalizer.ι (pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯)) (pullback.snd s v)) = CategoryStruct.comp (pullback.snd (equalizer.ι f g) (pullback.fst s v)) (pullback.snd s v)

@[simp]

theorem CategoryTheory.Limits.equalizerPullbackMapIso_inv_ι_snd_assoc {C : Type u} [Category.{v, u} C] [HasEqualizers C] [HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) (v : T ⟶ S) {Z : C} (h : T ⟶ Z) : CategoryStruct.comp (equalizerPullbackMapIso hf hg v).inv (CategoryStruct.comp (equalizer.ι (pullback.map s v t v f (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (pullback.map s v t v g (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯)) (CategoryStruct.comp (pullback.snd s v) h)) = CategoryStruct.comp (pullback.snd (equalizer.ι f g) (pullback.fst s v)) (CategoryStruct.comp (pullback.snd s v) h)