instCoeCochain — Mathlib

English

Given a 0-cocycle z, there is an associated morphism homOf z: F ⟶ G, defined by taking the diagonal components z.v_i_i at i.

Русский

Для 0‑кокцикла z имеется связанный морфизм homOf z: F ⟶ G, определяемый диагональными компонентами z.v_i_i.

LaTeX

$$def homOf (z : Cocycle F G 0) : F ⟶ G defined by f_i = z.v_{i,i} (add_zero i)$$

Lean4

instance : Coe (Cocycle F G n) (Cochain F G n) where coe x := x.1

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