inr_desc

Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc

← MathLib Explorer

English

Similarly, for t a PushoutCocone with ht an IsColimit, the morphism inr t composed with desc ht h k w equals k.

Русский

Аналогично, для inr t ∘ desc ht h k w = k.

LaTeX

$$inr t ≫ IsColimit.desc ht h k w = k$$

Lean4

@[reassoc (attr := simp)]
theorem inr_desc {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) :
    inr t ≫ IsColimit.desc ht h k w = k :=
  ht.fac _ _

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

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

Разделы

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

Аффилиация

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