of_iso_comp — Mathlib

English

If p is strongly cocartesian for f and φ, then it is cocartesian for f and φ.

Русский

Из сильно кокартезианского следует кокартезианское свойство.

LaTeX

$$[IsStronglyCocartesian p f φ] ⇒ [IsCocartesian p f φ]$$

Lean4

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

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