English
If i1, i2 are morphisms and i1, i2 preserve P, then the pullback map preserves P under the given equalities e1, e2.
Русский
Если i1, i2 сохраняют P, то отображение pullback сохраняет P при данных равенствах e1, e2.
LaTeX
$$P i1 → P i2 → ∀ e1 e2, P (pullback.map f g f' g' i1 i2 _ _)$$
Lean4
theorem pullback_map [HasPullbacks C] [IsStableUnderBaseChange P] [P.IsStableUnderComposition] {S X X' Y Y' : C}
{f : X ⟶ S} {g : Y ⟶ S} {f' : X' ⟶ S} {g' : Y' ⟶ S} {i₁ : X ⟶ X'} {i₂ : Y ⟶ Y'} (h₁ : P i₁) (h₂ : P i₂)
(e₁ : f = i₁ ≫ f') (e₂ : g = i₂ ≫ g') :
P (pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁) ((Category.comp_id _).trans e₂)) :=
by
have :
pullback.map f g f' g' i₁ i₂ (𝟙 _) ((Category.comp_id _).trans e₁) ((Category.comp_id _).trans e₂) =
((pullbackSymmetry _ _).hom ≫ ((Over.pullback _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫
(pullbackSymmetry _ _).hom ≫ ((Over.pullback g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left :=
by ext <;> simp
rw [this]
apply P.comp_mem <;> rw [P.cancel_left_of_respectsIso]
exacts [baseChange_map _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂,
baseChange_map _ (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f') h₁]
