orientedCyclicFamilies_boundary_generate
plain-language theorem explainer
Names the local geometric generation target: every concrete oriented closed walk on S¹ is homologous to an integer multiple of the fundamental cycle. Anyone chasing the surjective half of H₁(S¹;ℤ) ≅ ℤ cites this Prop. It is a bare Prop definition packaging the cycle-object equation, not a proved theorem.
Claim. The following assertion holds as a named proposition: for every oriented cyclic family term $T$, there exist an integer $n$ and a singular $2$-chain $b$ on $S^1$ such that the free $1$-cycle of $T$ equals $\partial b + n\,[γ]$, where $[γ]$ is the fundamental singular $1$-cycle of $S^1$.
background
The module lifts path-level winding on $S^1$ to singular simplices and proves that displacement kills boundaries of $2$-simplices. Together with the fact that the once-around loop has winding $1$, this yields a left inverse to the fundamental class, i.e. the split-injective half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$.
The converse, generation, says every integer $1$-cycle is homologous to an integer multiple of the fundamental cycle. Mathlib's singular homology does not yet supply a simplicial prism or subdivision operator, so the project isolates that remaining geometric work as named Props.
Here the ambient chain complex is the Mathlib singular chain complex of $\mathrm{TopCat.sphere},1$ with $\mathbb{Z}$ coefficients. The fundamental cycle is that once-around generator lifted into the cycle object via its zero-boundary proof. An oriented cyclic family term packages a concrete closed walk together with its free $1$-cycle.
proof idea
Definitional: the body is the Prop itself. Universally quantify over oriented cyclic family terms $T$; assert existence of an integer coefficient $n$ (as a morphism out of $\mathbb{Z}$ in $\mathrm{ModuleCat}$) and a degree-$2$ singular chain $b$ such that the cycle of $T$ equals the image of $b$ under the chain-complex boundary-to-cycles map plus $n$ times the fundamental cycle. No tactics or lemmas are applied; downstream theorems discharge or transport this Prop.
why it matters
This is the retained-walk form of the remaining generation target for the circle $H_1$ computation. Feeding it into fundamentalCycle_boundary_generates_of_orientedCyclicFamilies yields the global chain-level generation theorem, which in turn yields circleH1ZIsoInt_of_orientedCyclicFamilies: the concrete oriented-family filling target is enough for the final Mathlib circle $H_1$ computation.
Equivalence theorems pin it to zero-winding filling and to raw-prism generation, so the geometric work can be attacked as an explicit singular prism $2$-chain whose $C_1$ boundary is the oriented closed walk minus the matching multiple of the fundamental cycle. In the Recognition forcing chain this closes the strict integer comparison half of $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$, the topological input behind T8 ($D=3$) landmarks that rely on the circle's homology being $\mathbb{Z}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.