of_comp_iso — Mathlib

English

The inverse part of domain iso yields a HomLift for the inverse base morphism.

Русский

Обратная часть доменного изоморфизма образует подъём для обратного базового гомоморфизма.

LaTeX

$$$IsHomLift(p,\\; g.inv,\\; (domainIsoOfBaseIso(p,h,φ,φ')).inv)$$$

Lean4

/-- Postcomposing a co-Cartesian morphism with an isomorphism lifting the identity is
co-Cartesian. -/
instance of_comp_iso {b' : 𝒳} (φ' : b ≅ b') [IsHomLift p (𝟙 S) φ'.hom] : IsCocartesian p f (φ ≫ φ'.hom) where
  universal_property := by
    intro c ψ hψ
    use φ'.inv ≫ IsCocartesian.map p f φ ψ
    refine ⟨⟨inferInstance, by simp⟩, ?_⟩
    rintro τ ⟨hτ₁, hτ₂⟩
    rw [Iso.eq_inv_comp]
    apply map_uniq
    exact ((assoc φ _ _) ▸ hτ₂)

Похожие утверждения