fst — Mathlib

English

The first projection from the mapping cone is a cocycle of degree 1, giving a canonical representation for the cone’s left component.

Русский

Первая проекция из mappingCone является кокцикелем степени 1, задавая каноническое представление левого компонента конуса.

LaTeX

$$$\mathrm{fst}: \text{Cocycle}(\text{mappingCone}(φ),F,1).$$$

Lean4

/-- The first projection from the mapping cone, as a cocyle of degree `1`. -/
noncomputable def fst : Cocycle (mappingCone φ) F 1 :=
  Cocycle.mk (Cochain.mk (fun p q hpq => homotopyCofiber.fstX φ p q hpq)) 2 (by cutsat)
    (by
      ext p _ rfl
      simp [δ_v 1 2 (by cutsat) _ p (p + 2) (by cutsat) (p + 1) (p + 1) (by cutsat) rfl,
        homotopyCofiber.d_fstX φ p (p + 1) (p + 2) rfl, mappingCone, show Int.negOnePow 2 = 1 by rfl])

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