of_comp_iso — Mathlib

English

Precomposing a Cartesian morphism with an isomorphism lifting the identity is Cartesian.

Русский

Предположим, что после предсуммирования кардинального зрителя по изоморфизму, подъем сохраняется.

LaTeX

$$$[\\text{IsCartesian } p f (\\phi')]\\; \\Rightarrow\\; IsCartesian p f (\\phi'\\text{Hom} \\circ \\phi)$$$

Lean4

instance of_comp_iso {b' : 𝒳} (φ' : b ≅ b') [IsHomLift p (𝟙 S) φ'.hom] : IsCartesian p f (φ ≫ φ'.hom) where
  universal_property := by
    intro c ψ hψ
    use IsCartesian.map p f φ (ψ ≫ φ'.inv)
    refine ⟨⟨inferInstance, by simp only [fac_assoc, assoc, Iso.inv_hom_id, comp_id]⟩, ?_⟩
    rintro τ ⟨hτ₁, hτ₂⟩
    apply map_uniq
    rw [Iso.eq_comp_inv]
    simp only [assoc, hτ₂]

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