map_lift_equalizerComparison — Mathlib

English

For HasEqualizer f g and HasEqualizer (G.map f) (G.map g), the map G.map (equalizer.lift h w) composed with equalizerComparison equals equalizer.lift (G.map h) (by simp).

Русский

Пусть существуют эквалайзер f g и эквалайзер (G.map f) (G.map g). Тогда G.map (equalizer.lift h w) составленный с equalizerComparison равен равнозначителю равному G.map h.

LaTeX

$$$ G.map (equalizer.lift h w) \\; \\circ\\; equalizerComparison f g G = equalizer.lift (G.map h) (by simp) $$$

Lean4

@[reassoc (attr := simp)]
theorem map_lift_equalizerComparison [HasEqualizer f g] [HasEqualizer (G.map f) (G.map g)] {Z : C} {h : Z ⟶ X}
    (w : h ≫ f = h ≫ g) :
    G.map (equalizer.lift h w) ≫ equalizerComparison f g G =
      equalizer.lift (G.map h) (by simp only [← G.map_comp, w]) :=
  by
  apply equalizer.hom_ext
  simp [← G.map_comp]

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