homotopyInvHomId — Mathlib

English

Let f: X1 → X2 and g: X2 → X3 be composable morphisms of cochain complexes. Then there exists a specified homotopy between the composite inv(f,g) ∘ hom(f,g) and the identity on the target mapping cone, exhibiting a homotopy equivalence.

Русский

Пусть f: X1 → X2 и g: X2 → X3 — вместе образующие морфизмы цепочечных комплексoв. Существует явно заданный гомотопийный переход между композицией inv(f,g) ∘ hom(f,g) и тождественным отображением на соответствующем образующем коне.

LaTeX

$$$\text{Homotopy}(\operatorname{inv}(f,g) \circ \operatorname{hom}(f,g), \mathrm{Id})$$$

Lean4

/-- Given two composable morphisms `f` and `g` in the category of cochain complexes,
this is the `homotopyInvHomId` field of the homotopy equivalence
`mappingConeCompHomotopyEquiv f g` between `mappingCone g` and the mapping cone of
the morphism `mappingCone f ⟶ mappingCone (f ≫ g)`. -/
noncomputable def homotopyInvHomId : Homotopy (inv f g ≫ hom f g) (𝟙 _) :=
  (Cochain.equivHomotopy _ _).symm
    ⟨-((snd _).comp ((fst (f ≫ g)).1.comp ((inl f).comp (inl _) (by decide)) (show 1 + (-2) = -1 by decide))
          (zero_add (-1))),
      by
      rw [δ_neg, δ_zero_cochain_comp _ _ _ (neg_add_cancel 1), Int.negOnePow_neg, Int.negOnePow_one, Units.neg_smul,
        one_smul, δ_comp _ _ (show 1 + (-2) = -1 by decide) 2 (-1) 0 (by decide) (by decide) (by decide),
        δ_comp _ _ (show (-1) + (-1) = -2 by decide) 0 0 (-1) (by decide) (by decide) (by decide), Int.negOnePow_neg,
        Int.negOnePow_neg, Int.negOnePow_even 2 ⟨1, by decide⟩, Int.negOnePow_one, Units.neg_smul, one_smul, one_smul,
        δ_inl, δ_inl, δ_snd, Cocycle.δ_eq_zero, Cochain.zero_comp, add_zero, Cochain.neg_comp, neg_neg]
      ext n
      rw [ext_from_iff _ (n + 1) n rfl, ext_from_iff _ (n + 1) n rfl, ext_from_iff _ (n + 2) (n + 1) (by cutsat)]
      dsimp [hom, inv]
      simp [ext_to_iff _ n (n + 1) rfl, map, Cochain.comp_v _ _ (add_neg_cancel 1) n (n + 1) n (by cutsat) (by cutsat),
        Cochain.comp_v _ _ (show 1 + -2 = -1 by decide) (n + 1) (n + 2) n (by cutsat) (by cutsat),
        Cochain.comp_v _ _ (show (-1) + -1 = -2 by decide) (n + 2) (n + 1) n (by cutsat) (by cutsat)]⟩

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