English
If φ is a morphism over an isomorphism g, and f φ is strongly Cartesian, then φ is strongly Cartesian.
Русский
Если φ лежит над изоморфизмом g и φ над f является сильно-картезианским, то φ сам является сильно-картезианским.
LaTeX
$$$(p.IsStronglyCartesian p f φ) \\Rightarrow (p.IsStronglyCartesian p f φ)$$$
Lean4
/-- A strongly Cartesian morphism lying over an isomorphism is an isomorphism. -/
theorem isIso_of_base_isIso (φ : a ⟶ b) [IsStronglyCartesian p f φ] [IsIso f] : IsIso φ :=
by
subst_hom_lift p f φ; clear a b R S
let φ' := map p (p.map φ) φ (IsIso.inv_hom_id (p.map φ)).symm (𝟙 b)
use φ'
have inv_hom : φ' ≫ φ = 𝟙 b := fac p (p.map φ) φ _ (𝟙 b)
refine
⟨?_, inv_hom⟩
-- We will now show that `φ ≫ φ' = 𝟙 a` by showing that `(φ ≫ φ') ≫ φ = 𝟙 a ≫ φ`.
have h₁ : IsHomLift p (𝟙 (p.obj a)) (φ ≫ φ') :=
by
rw [← IsIso.hom_inv_id (p.map φ)]
apply IsHomLift.comp
apply IsStronglyCartesian.ext p (p.map φ) φ (𝟙 (p.obj a))
simp only [assoc, inv_hom, comp_id, id_comp]
