rotateHomotopyEquivComm₂Homotopy

English

The rotated homotopy equivalence commutes with the inr map in the quotient homotopy category, ensuring a natural compatibility.

Русский

Повернутая гомотопическая эквивалентность коммутирует с отображением inr в факторной гомотопической категории.

LaTeX

$$$ (HomotopyCategory.quotient).map( (triangle φ).mor_3 ) \\circ (HomotopyCategory.quotient).map( rotateHomotopyEquiv φ ).hom = (HomotopyCategory.quotient).map( inr (inr φ) )$$$

Lean4

/-- Auxiliary definition for `rotateTrianglehIso`. -/
noncomputable def rotateHomotopyEquivComm₂Homotopy :
    Homotopy ((triangle φ).mor₃ ≫ (rotateHomotopyEquiv φ).hom) (inr (CochainComplex.mappingCone.inr φ)) :=
  (Cochain.equivHomotopy _ _).symm
    ⟨-(snd φ).comp (inl (inr φ)) (zero_add (-1)), by
      ext p
      dsimp [rotateHomotopyEquiv]
        -- the following list of lemmas has been obtained by doing
                -- simp? [ext_from_iff _ _ _ rfl, ext_to_iff _ _ _ rfl,
                --  (inl φ).leftShift_v 1 0 (neg_add_cancel 1) p p (add_zero p) (p + 1) (by omega),
                --  δ_zero_cochain_comp _ _ _ (neg_add_cancel 1),
                --  Cochain.comp_v _ _ (add_neg_cancel 1) p (p + 1) p rfl (by omega),
                --  (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by omega)]⟩

      simp only [Int.reduceNeg, Cochain.ofHom_comp, ofHom_lift, Cocycle.coe_neg, Cocycle.leftShift_coe,
        Cocycle.ofHom_coe, Cochain.comp_zero_cochain_v, shiftFunctor_obj_X', Cochain.ofHom_v, δ_neg,
        δ_zero_cochain_comp _ _ _ (neg_add_cancel 1), δ_inl, Int.negOnePow_neg, Int.negOnePow_one, δ_snd,
        Cochain.neg_comp, Cochain.comp_assoc_of_second_is_zero_cochain, smul_neg, Units.neg_smul, one_smul, neg_neg,
        neg_add_rev, Cochain.add_v, Cochain.neg_v, Cochain.comp_v _ _ (add_neg_cancel 1) p (p + 1) p rfl (by cutsat),
        Cochain.zero_cochain_comp_v, ext_from_iff _ _ _ rfl, inl_v_triangle_mor₃_f_assoc, triangle_obj₁,
        shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, Preadditive.neg_comp,
        id_comp, Preadditive.comp_add, Preadditive.comp_neg, inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, neg_zero,
        add_zero, ext_to_iff _ _ _ rfl, liftCochain_v_fst_v,
        (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by cutsat), mul_one, sub_self, mul_zero,
        Int.zero_ediv, Iso.refl_hom, Preadditive.add_comp, assoc, inl_v_fst_v, comp_id, inr_f_fst_v, comp_zero,
        liftCochain_v_snd_v, (inl φ).leftShift_v 1 0 (neg_add_cancel 1) p p (add_zero p) (p + 1) (by cutsat),
        Int.negOnePow_zero, inl_v_snd_v, inr_f_snd_v, zero_add, and_self, inr_f_triangle_mor₃_f_assoc,
        inr_f_fst_v_assoc, inr_f_snd_v_assoc, neg_add_cancel]⟩

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