English
Let f,g,f',g' and i1,i2,i3 with e1,e2 and [Mono i3] be as in the statement. The cartesian lifts of the common map given by pullback.map form a pullback square: the two lifted arrows from the domain to the respective pullbacks form a pullback with the common first projections.
Русский
Пусть даны карты и условия, образующие общую схему. Тогда канонические канонические подстановки образуют квадрат типа pullback.
LaTeX
$$$\\mathrm{IsPullback}\\left( \\mathrm{pullback.lift}\\left( \\mathrm{pullback.map} f g f' g' i_1 i_2 i_3 e_1 e_2 \\right) (\\mathrm{fst}\\ '_'\\ _) (\\mathrm{lift\\_fst}\\ _\\ _ ) ,\\; \\mathrm{pullback.lift}\\left( \\mathrm{pullback.map} f g f' g' i_1 i_2 i_3 e_1 e_2 \\right) (\\mathrm{snd}\\ '_'\\ _) (\\mathrm{lift\\_snd}\\ _\\ _ ) ,\\; \\mathrm{pullback.fst}\\ _\\ _ ,\\; \\mathrm{pullback.fst}\\ _\\ _ \\right)$$
Lean4
theorem pullback_lift_map_isPullback {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S')
(i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : f ≫ i₃ = i₁ ≫ f') (e₂ : g ≫ i₃ = i₂ ≫ g') [Mono i₃] :
IsPullback (pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst _ _) (lift_fst _ _ _))
(pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd _ _) (lift_snd _ _ _)) (pullback.fst _ _)
(pullback.fst _ _) :=
IsPullback.of_iso_pullback ⟨by rw [lift_fst, lift_fst]⟩ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm (by simp)
(by simp)
