inrX

Mathlib.Algebra.Homology.HomotopyCofiber

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.homotopyCofiber.inrX

Lean4

/-- The right inclusion `G.X i ⟶ (homotopyCofiber φ).X i`. -/
noncomputable def inrX (i : ι) : G.X i ⟶ X φ i :=
  if hi : c.Rel i (c.next i) then
    haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hi
    biprod.inr ≫ (XIsoBiprod φ _ _ hi).inv
  else (XIso φ i hi).inv

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

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

Разделы

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

Аффилиация

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