CategoryTheory.Limits.PreservesCoequalizer.iso_hom

theorem CategoryTheory.Limits.PreservesCoequalizer.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g] [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)] [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G], (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).hom = CategoryTheory.Limits.coequalizerComparison f g G

This theorem, `CategoryTheory.Limits.PreservesCoequalizer.iso_hom`, states that for any category `C`, category `D`, and functor `G` mapping `C` to `D`, given the conditions that `C` has a coequalizer for a pair of morphisms `f` and `g` from `X` to `Y`, and `D` has a coequalizer for the pair of morphisms `G.map f` and `G.map g`, and `G` preserves the colimit of the parallel pair of `f` and `g`, then the homomorphism component of the isomorphism `CategoryTheory.Limits.PreservesCoequalizer.iso G f g` equals to the coequalizer comparison of `f`, `g` and `G`. In simpler terms, under the given conditions, the functor `G` preserves the structure of the coequalizer in the transition from `C` to `D`.

More concisely: If `C` is a category with a coequalizer for a pair of morphisms `f` and `g`, `D` is a category with a coequalizer for `G.map f` and `G.map g`, and `G` preserves the colimit of `f` and `g`, then the isomorphism `CategoryTheory.Limits.PreservesCoequalizer.iso G f g` equals the coequalizer comparison of `f`, `g`, and `G`.