shiftTriangleIso — Mathlib

English

Canonical isomorphism between the shifted triangle and the triangle of the shifted morphism: (triangle φ)⟦n⟧ ≅ triangle (φ⟦n⟧').

Русский

Каноническое изоморфие между сдвинутым треугольником и треугольником от сдвинутого морфизма: (triangle φ)⟦n⟧ ≅ triangle (φ⟦n⟧').

LaTeX

$$$ (triangle\\, φ)^{\\langle n \\rangle} \\cong triangle(φ^{\\langle n \\rangle'}) $$$

Lean4

/-- The canonical isomorphism `(triangle φ)⟦n⟧ ≅ triangle (φ⟦n⟧')`. -/
noncomputable def shiftTriangleIso (n : ℤ) : (Triangle.shiftFunctor _ n).obj (triangle φ) ≅ triangle (φ⟦n⟧') :=
  by
  refine Triangle.isoMk _ _ (Iso.refl _) (n.negOnePow • Iso.refl _) (shiftIso φ n) ?_ ?_ ?_
  · dsimp
    simp only [Linear.comp_units_smul, comp_id, id_comp, smul_smul, Int.units_mul_self, one_smul]
  · ext p
    dsimp
    simp only [Units.smul_def, shiftIso, Int.reduceNeg, Linear.smul_comp, id_comp, ext_to_iff _ _ (p + 1) rfl,
      shiftFunctor_obj_X', assoc, lift_f_fst_v, Cocycle.coe_smul, Cocycle.shift_coe, Cochain.smul_v, Cochain.shift_v',
      Linear.comp_smul, inr_f_fst_v, smul_zero, lift_f_snd_v, inr_f_snd_v, and_true]
  · ext p
    dsimp
    simp only [triangle, Triangle.mk_mor₃, Cocycle.homOf_f, Cocycle.rightShift_coe, Cocycle.coe_neg,
      Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
      (fst φ).1.rightShift_v 1 0 (zero_add 1) (p + n) (p + n) (add_zero (p + n)) (p + 1 + n) (by cutsat),
      shiftFunctor_obj_X, shiftFunctorObjXIso, shiftFunctorComm_hom_app_f, Preadditive.neg_comp, assoc, Iso.inv_hom_id,
      comp_id, smul_neg, Units.smul_def, shiftIso, Int.reduceNeg,
      (fst (φ⟦n⟧')).1.rightShift_v 1 0 (zero_add 1) p p (add_zero p) (p + 1) rfl, HomologicalComplex.XIsoOfEq_rfl,
      Iso.refl_inv, Preadditive.comp_neg, lift_f_fst_v, Cocycle.coe_smul, Cocycle.shift_coe, Cochain.smul_v,
      Cochain.shift_v']

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