coequalizerComparison_map_desc — Mathlib

English

The universal morphism for desc commutes with the functor: coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) = coequalizer.desc (G.map h) (by simp).

Русский

Универсальная стрелка desc коммутирует с функтором: coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) = coequalizer.desc (G.map h) (по доказательству).

LaTeX

$$$ coequalizerComparison f g G \\; \\circ \\; G.map (coequalizer.desc h w) = coequalizer.desc (G.map h) (by simp) $$$

Lean4

@[reassoc (attr := simp)]
theorem coequalizerComparison_map_desc [HasCoequalizer f g] [HasCoequalizer (G.map f) (G.map g)] {Z : C} {h : Y ⟶ Z}
    (w : f ≫ h = g ≫ h) :
    coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
      coequalizer.desc (G.map h) (by simp only [← G.map_comp, w]) :=
  by
  apply coequalizer.hom_ext
  simp [← G.map_comp]

Похожие утверждения