English
If h is already a pullback and all pieces are replaced by isomorphic ones with compatible maps, then the resulting square is again a pullback.
Русский
Если уже есть предел, и все компоненты замещены изоморфизмами с согласованными стрелками, то получившийся квадрат снова является пределом.
LaTeX
$$$ \text{IsPullback fst snd f g} \Rightarrow \text{IsPullback fst' snd' f' g'} $$$
Lean4
theorem of_iso (h : IsPullback fst snd f g) {P' X' Y' Z' : C} {fst' : P' ⟶ X'} {snd' : P' ⟶ Y'} {f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'} (e₁ : P ≅ P') (e₂ : X ≅ X') (e₃ : Y ≅ Y') (e₄ : Z ≅ Z') (commfst : fst ≫ e₂.hom = e₁.hom ≫ fst')
(commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd') (commf : f ≫ e₄.hom = e₂.hom ≫ f') (commg : g ≫ e₄.hom = e₃.hom ≫ g') :
IsPullback fst' snd' f' g'
where
w := by rw [← cancel_epi e₁.hom, ← reassoc_of% commfst, ← commf, ← reassoc_of% commsnd, ← commg, h.w_assoc]
isLimit' :=
⟨(IsLimit.postcomposeInvEquiv (cospanExt e₂ e₃ e₄ commf.symm commg.symm) _).1
(IsLimit.ofIsoLimit h.isLimit
(by
refine PullbackCone.ext e₁ ?_ ?_
· change fst = e₁.hom ≫ fst' ≫ e₂.inv
rw [← reassoc_of% commfst, e₂.hom_inv_id, Category.comp_id]
· change snd = e₁.hom ≫ snd' ≫ e₃.inv
rw [← reassoc_of% commsnd, e₃.hom_inv_id, Category.comp_id]))⟩
