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