orientedCyclicFamilies_rawPrism_generate
plain-language theorem explainer
Packages the remaining geometric prism obligation for circle homology: every oriented cyclic family on S¹ is the boundary of some singular 2-chain plus an integer multiple of the fundamental cycle, written as a raw C₁ equality. Anyone closing the generation half of H₁(S¹;ℤ) ≅ ℤ cites this Prop. It is a pure definition of a proposition, not a proved theorem.
Claim. The following proposition holds: for every oriented cyclic family term $T$, there exist an integer $n$ and a singular $2$-chain $b$ in the integer singular chain complex of $S^1$ such that $\partial_2 b$ equals the image in $C_1$ of the cycle of $T$ minus $n$ times the fundamental cycle of $S^1$.
background
The module lifts path-level winding on the circle to singular simplices of TopCat.sphere 1 and proves that displacement kills boundaries of 2-simplices. Together with the fact that the once-around loop has winding 1, that gives 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: every 1-cycle is homologous to an integer multiple of the fundamental cycle) needs a simplicial prism or subdivision operator that Mathlib singular homology does not yet supply. The ambient chain complex is the imported Mathlib singular chain complex of $S^1$ with integer coefficients; its degree-1 homology is the stated comparison target. The fundamental cycle is the once-around singular 1-simplex, lifted into the cycle object via its zero-boundary proof.
An oriented cyclic family term is a concrete closed oriented edge walk on the circle. The raw-prism form asks for a singular 2-chain whose $C_1$ boundary equals that walk minus the matching multiple of the fundamental cycle, which is exactly what an explicit prism construction produces.
proof idea
No proof: this is a def of a Prop. The body is the universal quantification over oriented cyclic family terms $T$, asserting existence of an integer coefficient $n$ and a degree-2 chain $b$ in the singular complex such that the differential $d_{2,1}(b)$ equals the inclusion of $T$'s cycle into $C_1$ minus the inclusion of $n$ times the fundamental cycle. Downstream lemmas only transport this equality between cycle-object and raw-chain coordinates.
why it matters
This is the packaged remaining obligation for the generation half of the integer comparison $H_1(S^1;\mathbb{Z})\cong\mathbb{Z}$. Downstream, orientedCyclicFamilies_boundary_generate_of_rawPrism transports it to cycle-object generation by pure categorical inclusion; orientedCyclicFamilies_explicitRawPrism_generate_of_rawPrism and the free/raw equivalence show that coordinate packaging is settled. The terminal consumer is circleH1ZIsoInt_of_rawPrism: a raw prism filling for each concrete oriented cyclic family is enough for the final Mathlib circle $H_1$ computation.
Equivalence with zero-winding filling (orientedCyclicFamilies_rawPrism_generate_iff_zeroWindingCycles_bound) ties the Prop to the winding invariant already proved in the module. In the Recognition chain this closes the surjectivity half that the kills-boundaries identity alone cannot reach; the open geometric content is the actual singular prism 2-chain, not further algebraic packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.