augment — Mathlib

English

A chain map to the single-object complex induces an augmented chain complex via the inverse equivalence.

Русский

Цепное отображение к единичному объекту порождает аугментированный цепной комплекс через эквивалентность обратную.

LaTeX

$$$\\text{toSingle}_0^{AsComplex}(C,X,f) \\Rightarrow \\text{augment}(C,f,w) \\;\\text{with } w:\\; C.d_{1 0} \\circ f = 0$$$

Lean4

/-- We can "augment" a cochain complex by inserting an arbitrary object in degree zero
(shifting everything else up), along with a suitable differential.
-/
def augment (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : f ≫ C.d 0 1 = 0) : CochainComplex V ℕ
    where
  X
    | 0 => X
    | i + 1 => C.X i
  d
    | 0, 1 => f
    | i + 1, j + 1 => C.d i j
    | _, _ => 0
  shape i j
    s := by
    rcases j with (_ | _ | j) <;> cases i <;> try simp
    · contradiction
    · rw [C.shape]
      simp only [ComplexShape.up_Rel] at ⊢ s
      contrapose! s
      rw [← s]
  d_comp_d' i j k hij
    hjk := by
    rcases k with (_ | _ | k) <;> rcases j with (_ | _ | j) <;> cases i <;> try simp
    cases k
    · exact w
    · rw [C.shape, comp_zero]
      simp only [ComplexShape.up_Rel, zero_add]
      exact (Nat.one_lt_succ_succ _).ne

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