ext

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.BinaryCofan.ext

Lean4

/-- Constructs an isomorphism of `BinaryCofan`s out of an isomorphism of the tips that commutes with
the injections. -/
def ext {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : c.inl ≫ e.hom = c'.inl)
    (h₂ : c.inr ≫ e.hom = c'.inr) : c ≅ c' :=
  Cocones.ext e (fun j => by rcases j with ⟨⟨⟩⟩ <;> assumption)

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

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

Разделы

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

Аффилиация

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