diagonal_comp — Mathlib

English

A specialized IsPullback result for a lifting along diagonal in a diagram where f,g,i are pulled back, showing the diagonal lift yields a pullback square.

Русский

Специализированный результат IsPullback для подъёма вдоль диагонали в диаграмме, где f,g,i являются предельно подобранными, показывающий, что диагональный подъём образует квадрат предела.

LaTeX

$$$$ IsPullback g (pullback.lift (id_Y) g (by simp)) (diagonal f) (pullback.map (g ≫ f) f f f g (id_X) (id_S) (by simp) (by simp)) $$$$

Lean4

theorem diagonal_comp (f : X ⟶ Y) (g : Y ⟶ Z) :
    diagonal (f ≫ g) = diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ pullback.snd _ _ := by ext <;> simp

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