English
In a category with pullbacks, for morphisms g: Y → X and f: X → S, a certain constructed square involving diagonal of f and pullback maps is a pullback square; i.e., it satisfies the defining universal property of a pullback.
Русский
В категории с точками вытягиваний (pullbacks) для морфизмов g: Y → X и f: X → S образуется квадрат, состоящий из диагонали f и связанных отображений pullback, который является квадратом-подтягиванием (pullback).
LaTeX
$$$\IsPullback\left(g,\mathrm{pullback.lift}(\mathrm{id}_Y, g, \cdots),\ \mathrm{diagonal}(f),\ \mathrm{pullback.map}(g\!\gg f, f, f, f, g, \mathrm{id}_X, \mathrm{id}_S, \cdots)\right).$$$
Lean4
/-- Informally, this is a special case of `pullback_map_diagonal_isPullback` for `T = X`. -/
theorem pullback_lift_diagonal_isPullback (g : Y ⟶ X) (f : X ⟶ S) :
IsPullback g (pullback.lift (𝟙 Y) g (by simp)) (diagonal f)
(pullback.map (g ≫ f) f f f g (𝟙 X) (𝟙 S) (by simp) (by simp)) :=
by
let i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom rfl (by simp)
let e :
pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) (by simp) (by simp)) ≅
pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) (by simp) (by simp)) :=
(asIso (map _ _ _ _ (𝟙 _) i.inv (𝟙 _) (by simp) (by ext <;> simp [i]))).symm
apply
IsPullback.of_iso_pullback _
(e ≪≫ pullbackDiagonalMapIdIso (T := X) (S := S) g (𝟙 X) f ≪≫ asIso (pullback.fst _ _)).symm
· simp [e]
· ext <;> simp [e, i]
· constructor
ext <;> simp
