cyclesMk — Mathlib

English

From an element f in the appropriate X_m-component that lies in the kernel of the differential, one obtains a term in Z_m via cyclesMk; i.e., cyclesMk(m,n,h,f,hf) is a cycle.

Русский

Из элемента f, лежащего в ядре дифференциала, с помощью cyclesMk строится элемент цикла в Z_m.

LaTeX

$$cyclesMk(m,n,h,f,hf) ∈ Z_m(G,A)$$

Lean4

/-- When `m = 0` this makes a term of `cycles A 0` from any element of `A` (or more precisely
any element in the kernel of `d₀,₀ = 0`). When `m` is positive, this makes a term of `cycles A m`
from any element of the kernel of `dₘ,ₘ₋₁`. -/
abbrev cyclesMk (m n : ℕ) (h : (ComplexShape.down ℕ).next m = n) (f : (Fin m → G) →₀ A)
    (hf : (inhomogeneousChains A).d m n f = 0) : cycles A m :=
  (inhomogeneousChains A).cyclesMk f n h hf

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