shiftFunctor — Mathlib

English

The shift functor by any integer n on CochainComplex C ℤ is a well-defined endofunctor preserving the additive structure and commuting with the shift in each degree.

Русский

Сдвиг по целому n на концепте CochainComplex C ℤ образует законный концевой функтор, сохраняющий аддитивность и commuting в каждом градусе.

LaTeX

$$$\\text{shiftFunctor}(C, n) : \\mathrm{CochainComplex}(C, \\mathbb{Z}) \\to \\mathrm{CochainComplex}(C, \\mathbb{Z})$ is additive and preserves structure.$$

Lean4

/-- The shift functor by `n : ℤ` on `CochainComplex C ℤ` which sends a cochain
complex `K` to the complex which is `K.X (i + n)` in degree `i`, and which
multiplies the differentials by `(-1)^n`. -/
@[simps]
def shiftFunctor (n : ℤ) : CochainComplex C ℤ ⥤ CochainComplex C ℤ
    where
  obj
    K :=
    { X := fun i => K.X (i + n)
      d := fun _ _ => n.negOnePow • K.d _ _
      d_comp_d' := by
        intros
        simp only [Linear.comp_units_smul, Linear.units_smul_comp, d_comp_d, smul_zero]
      shape := fun i j hij => by
        rw [K.shape, smul_zero]
        intro hij'
        apply hij
        dsimp at hij' ⊢
        omega }
  map
    φ :=
    { f := fun _ => φ.f _
      comm' := by
        intros
        dsimp
        simp only [Linear.comp_units_smul, Hom.comm, Linear.units_smul_comp] }
  map_id := by intros; rfl
  map_comp := by intros; rfl

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