toCycles — Mathlib

English

This is the map from i-chains to j-cycles induced by the differential in the complex of inhomogeneous chains.

Русский

Это отображение из i-цепей в j-циклы, индуцированное дифференциалом в комплексе инхомогенных цепей.

LaTeX

$$toCycles(i,j) : (inhomogeneousChains A)_i ⟶ Z_j(G,A) = cycles A j$$

Lean4

/-- This is the map from `i`-chains to `j`-cycles induced by the differential in the complex of
inhomogeneous chains. -/
abbrev toCycles (i j : ℕ) : (inhomogeneousChains A).X i ⟶ cycles A j :=
  (inhomogeneousChains A).toCycles i j

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