map_lift_pullbackComparison — Mathlib

English

In a pullback diagram, pullbackComparison composed with snd equals the functorial image of snd.

Русский

В диаграмме пуллбэка, композиция pullbackComparison с snd равна образу snd под действиемfunctor.

LaTeX

$$$\mathrm{pullbackComparison}\, G\, f\, g \;\; \circ\; \mathrm{pullback.snd} (G.map f) (G.map g) = G\, \mathrm{map}(\mathrm{pullback.snd} f g)$$$

Lean4

@[reassoc (attr := simp)]
theorem map_lift_pullbackComparison (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPullback (G.map f) (G.map g)] {W : C}
    {h : W ⟶ X} {k : W ⟶ Y} (w : h ≫ f = k ≫ g) :
    G.map (pullback.lift _ _ w) ≫ pullbackComparison G f g =
      pullback.lift (G.map h) (G.map k) (by simp only [← G.map_comp, w]) :=
  by ext <;> simp [← G.map_comp]

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