instInhabited

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

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

Lean4

instance : Inhabited (LeftHomologyMapData φ h₁ h₂) :=
  ⟨by
    let φK : h₁.K ⟶ h₂.K := h₂.liftK (h₁.i ≫ φ.τ₂) (by rw [assoc, φ.comm₂₃, h₁.wi_assoc, zero_comp])
    have commf' : h₁.f' ≫ φK = φ.τ₁ ≫ h₂.f' := by
      rw [← cancel_mono h₂.i, assoc, assoc, LeftHomologyData.liftK_i, LeftHomologyData.f'_i_assoc,
        LeftHomologyData.f'_i, φ.comm₁₂]
    let φH : h₁.H ⟶ h₂.H := h₁.descH (φK ≫ h₂.π) (by rw [reassoc_of% commf', h₂.f'_π, comp_zero])
    exact ⟨φK, φH, by simp [φK], commf', by simp [φH]⟩⟩

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

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

Разделы

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

Аффилиация

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