domainIsoOfBaseIso

Mathlib.CategoryTheory.FiberedCategory.Cartesian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso

Lean4

/-- The canonical isomorphism between the domains of two strongly Cartesian morphisms lying over
isomorphic objects. -/
@[simps]
noncomputable def domainIsoOfBaseIso (h : f' = g.hom ≫ f) (φ : a ⟶ b) (φ' : a' ⟶ b) [IsStronglyCartesian p f φ]
    [IsStronglyCartesian p f' φ'] : a' ≅ a where
  hom := map p f φ h φ'
  inv :=
    haveI : p.IsHomLift ((fun x ↦ g.inv ≫ x) (g.hom ≫ f)) φ := by simpa using IsCartesian.toIsHomLift
    map p f' φ' (congrArg (g.inv ≫ ·) h.symm) φ

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

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

Разделы

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

Аффилиация

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