mkHomFromDouble — Mathlib

Lean4
/-- Constructor for morphisms from a homological complex `double f hi₀₁`. -/
noncomputable def mkHomFromDouble : double f hi₀₁ ⟶ K
    where
  f
    k :=
    if hk₀ : k = i₀ then eqToHom (by rw [hk₀]) ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom (by rw [hk₀])
    else if hk₁ : k = i₁ then eqToHom (by rw [hk₁]) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom (by rw [hk₁]) else 0
  comm' k₀ k₁
    hk := by
    by_cases h₀ : k₀ = i₀
    · subst h₀
      rw [dif_pos rfl]
      obtain rfl := c.next_eq hk hi₀₁
      simp [dif_neg h.symm, double_d f hi₀₁ h, comm]
    · rw [dif_neg h₀]
      by_cases h₁ : k₀ = i₁
      · subst h₁
        dsimp
        rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero, double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]
      · apply (isZero_double_X f hi₀₁ k₀ h₀ h₁).eq_of_src
Похожие утверждения