rightShift — Mathlib

English

The equivalence between HomComplex.Cochain and Homotopy data is explicitly described by simps, linking a pair of morphisms to a cocycle condition involving δ and ofHom.

Русский

Эквивалентность между данными гомотопии и кокейн явно описана через simps, соединяя пару морфизмов с условием кокцикла, включающим δ и ofHom.

LaTeX

$$$\\text{equivHomotopy}(φ_1,φ_2) : \\mathrm{Homotopy}(φ_1,φ_2) \\to \\{ z : \\mathrm{Cochain}(F,G,-1)\\; |\\; \\mathrm{Cochain.ofHom}(φ_1) = δ(-1)0 z + \\mathrm{Cochain.ofHom}(φ_2) \\}$$$

Lean4

/-- The map `Cochain K L n → Cochain K (L⟦a⟧) n'` when `n' + a = n`. -/
def rightShift (a n' : ℤ) (hn' : n' + a = n) : Cochain K (L⟦a⟧) n' :=
  Cochain.mk (fun p q hpq => γ.v p (p + n) rfl ≫ (L.shiftFunctorObjXIso a q (p + n) (by cutsat)).inv)

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