homologySequenceδ_triangleh — Mathlib

English

Let n0, n1 ∈ Z with n0 + 1 = n1. The connecting morphism in the homology sequence of triangle h is equal to the composite of the usual functorial maps, the δ-map from DescShortComplex, and the boundary inv/coefficients tied to the up-shift structure.

Русский

Пусть n0, n1 ∈ ℤ с n0 + 1 = n1. Связующая морфизма в гомологических последовательностях треугольника равна композиции обычных отображений-факторов, δ-маршрута DescShortComplex и граничного отображения, учитывающего сдвиг вверх.

LaTeX

$$$\big(\text{homologyFunctor}(C,\uparrow\mathbb{Z}, 0)\big).\text{homologySequenceδ}(\triangleh S.f) n_0 n_1 h = (\text{homologyFunctorFactors}(C,\uparrow\mathbb{Z}) n_0).hom.app _ \;\circ\; \mathrm{HomologicalComplex.homologyMap}(\descShortComplex S) n_0 \;\circ\; h_S.δ n_0 n_1 h \;\circ\; (\text{homologyFunctorFactors}(C,\uparrow\mathbb{Z}) n_1).inv.app _$$$

Lean4

theorem homologySequenceδ_triangleh (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) :
    (homologyFunctor C (up ℤ) 0).homologySequenceδ (triangleh S.f) n₀ n₁ h =
      (homologyFunctorFactors C (up ℤ) n₀).hom.app _ ≫
        HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
          hS.δ n₀ n₁ h ≫ (homologyFunctorFactors C (up ℤ) n₁).inv.app _ :=
  by
  /- We proceed by diagram chase. We test the identity on
       cocycles `x' : A' ⟶ (mappingCone S.f).X n₀` -/

  dsimp
  rw [← cancel_mono ((homologyFunctorFactors C (up ℤ) n₁).hom.app _), assoc, assoc, assoc, Iso.inv_hom_id_app, ←
    cancel_epi ((homologyFunctorFactors C (up ℤ) n₀).inv.app _), Iso.inv_hom_id_app_assoc]
  apply yoneda.map_injective
  ext ⟨A⟩ (x : A ⟶ _)
  obtain ⟨A', π, _, x', w, hx'⟩ := (mappingCone S.f).eq_liftCycles_homologyπ_up_to_refinements x n₁ (by simpa using h)
  erw [homologySequenceδ_quotient_mapTriangle_obj_assoc _ _ _ h]
  dsimp
  rw [comp_id, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
  erw [comp_id]
  rw [← cancel_epi π, reassoc_of% hx', reassoc_of% hx', HomologicalComplex.homologyπ_naturality_assoc,
    HomologicalComplex.liftCycles_comp_cyclesMap_assoc]
    /- We decompose the cocycle `x'` into two morphisms `a : A' ⟶ S.X₁.X n₁`
         and `b : A' ⟶ S.X₂.X n₀` satisfying certain relations. -/

  obtain ⟨a, b, hab⟩ := decomp_to _ x' n₁ h
  rw [hab, ext_to_iff _ n₁ (n₁ + 1) rfl, add_comp, assoc, assoc, inr_f_d, add_comp, assoc, assoc, assoc, assoc,
    inr_f_fst_v, comp_zero, comp_zero, add_zero, zero_comp, d_fst_v _ _ _ _ h, comp_neg, inl_v_fst_v_assoc, comp_neg,
    neg_eq_zero, add_comp, assoc, assoc, assoc, assoc, inr_f_snd_v, comp_id, zero_comp, d_snd_v _ _ _ h, comp_add,
    inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, add_zero] at w
  conv_rhs => simp only [hab, add_comp, assoc, inr_f_descShortComplex_f, inl_v_descShortComplex_f, comp_zero, zero_add]
  rw [hS.δ_eq n₀ n₁ (by simpa using h) (b ≫ S.g.f n₀) _ b rfl (-a)
      (by simp only [neg_comp, neg_eq_iff_add_eq_zero, w.2]) (n₁ + 1) (by simp)]
    /- We simplify the LHS. -/

  dsimp [Functor.shiftMap, homologyFunctor_shift]
  rw [HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.liftCycles_comp_cyclesMap_assoc,
    S.X₁.liftCycles_shift_homologyπ_assoc _ _ _ _ n₁ (by cutsat) (n₁ + 1) (by simp), Iso.inv_hom_id_app]
  dsimp [homologyFunctor_shift]
  simp only [hab, add_comp, assoc, inl_v_triangle_mor₃_f_assoc, shiftFunctorObjXIso, neg_comp, Iso.inv_hom_id, comp_neg,
    comp_id, inr_f_triangle_mor₃_f_assoc, zero_comp, comp_zero, add_zero]

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