of_iso_comp — Mathlib

English

The forgetful functor from BasedNatTrans to the underlying Functor category reflects isomorphisms on objects and morphisms.

Русский

Забывающий функтор из BasedNatTrans в базовую категорию отражает изоморфизмы на уровне объектов и морфизмов.

LaTeX

$$$(forgetful 𝒳 𝒴).ReflectsIsomorphisms$$$

Lean4

/-- Precomposing a Cartesian morphism with an isomorphism lifting the identity is Cartesian. -/
instance of_iso_comp {a' : 𝒳} (φ' : a' ≅ a) [IsHomLift p (𝟙 R) φ'.hom] : IsCartesian p f (φ'.hom ≫ φ) where
  universal_property := by
    intro c ψ hψ
    use IsCartesian.map p f φ ψ ≫ φ'.inv
    refine ⟨⟨inferInstance, by simp⟩, ?_⟩
    rintro τ ⟨hτ₁, hτ₂⟩
    rw [Iso.eq_comp_inv]
    apply map_uniq
    simp only [assoc, hτ₂]

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