instInhabited

Mathlib.Algebra.Homology.ShortComplex.RightHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.RightHomologyMapData.instInhabited

Lean4

instance : Inhabited (RightHomologyMapData φ h₁ h₂) :=
  ⟨by
    let φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) (by rw [← φ.comm₁₂_assoc, h₂.wp, comp_zero])
    have commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃ := by
      rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc, RightHomologyData.p_g', φ.comm₂₃,
        RightHomologyData.p_g'_assoc]
    let φH : h₁.H ⟶ h₂.H := h₂.liftH (h₁.ι ≫ φQ) (by rw [assoc, commg', RightHomologyData.ι_g'_assoc, zero_comp])
    exact ⟨φQ, φH, by simp [φQ], commg', by simp [φH]⟩⟩

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

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

Разделы

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

Аффилиация

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