codomainIsoOfBaseIso

Mathlib.CategoryTheory.FiberedCategory.Cocartesian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsStronglyCocartesian.codomainIsoOfBaseIso

Lean4

/-- The canonical isomorphism between the codomains of two strongly co-Cartesian arrows lying over
isomorphic objects. -/
noncomputable def codomainIsoOfBaseIso {R S S' : 𝒮} {a b b' : 𝒳} {f : R ⟶ S} {f' : R ⟶ S'} {g : S ≅ S'}
    (h : f' = f ≫ g.hom) (φ : a ⟶ b) (φ' : a ⟶ b') [IsStronglyCocartesian p f φ] [IsStronglyCocartesian p f' φ'] :
    b ≅ b' where
  hom := map p f φ h φ'
  inv :=
    @map _ _ _ _ p _ _ _ _ f' φ' _ _ _ _ _ (congrArg (· ≫ g.inv) h.symm) φ
      (by simp only [assoc, Iso.hom_inv_id, comp_id]; infer_instance)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru