The subgroup $S_n^{\mathcal{A}}(X) \subseteq S_n(X)$ of $\mathcal{A}$-small singular $n$-chains: the subgroup generated by singular simplices whose image is contained in some member of the family $\mathcal{A}$ (Definition 11.3).
Instances For
The $i$-th face of an $\mathcal{A}$-small simplex is again $\mathcal{A}$-small, since its image is a subset of the original simplex's image.
The singular boundary map sends $\mathcal{A}$-small chains to $\mathcal{A}$-small chains, so the subcomplex $S_*^{\mathcal{A}}(X)$ is closed under $\partial$.
The restriction of the singular boundary map to the subcomplex of $\mathcal{A}$-small chains, giving the differential of $S_*^{\mathcal{A}}(X)$.
Instances For
The standard cosimplicial identity for face inclusions of the standard simplex: composing face inclusions in two different orders yields the same map. This is the combinatorial fact underlying $\partial \circ \partial = 0$.
The singular boundary maps satisfy $\partial_n \circ \partial_{n+1} = 0$, making singular chains into a chain complex.
Two consecutive small boundary maps compose to zero, inherited from the analogous identity on full singular chains.
The chain complex $S_*^{\mathcal{A}}(X)$ of $\mathcal{A}$-small singular chains, with differentials inherited from the singular chain complex (Definition 11.3).
Instances For
The canonical isomorphism from SingularChains n X (defined as a free abelian
group on singular simplices) into the categorical singular chain complex
singularChainComplexZ X, sending each generator to the corresponding coproduct
inclusion of 1 : ℤ.
Instances For
The map from $\mathcal{A}$-small chains into the categorical singular chain
complex at degree n, defined by first including into all singular chains and then
applying singularChainsLift.
Instances For
The geometric face inclusion of the $n$-simplex into the $(n+1)$-simplex agrees
with the map induced by Fin.succAbove i via the standard simplex functor.
Evaluating a finite sum of morphisms ℤ ⟶ B at 1 : ℤ equals the sum of their
individual evaluations at 1. A small bookkeeping lemma used to unfold sums of
AddCommGrpCat-morphisms.
The lift singularChainsLift intertwines the elementary singular boundary map
with the differential of the categorical singular chain complex.
The chain map $\iota : S_*^{\mathcal{A}}(X) \hookrightarrow S_*(X)$ embedding the subcomplex of $\mathcal{A}$-small chains into the singular chain complex. The locality principle asserts this is a quasi-isomorphism.
Instances For
The map singularChainsLift from the free abelian group on singular simplices
to the categorical singular chain complex is surjective, obtained by exhibiting an
explicit section out of the coproduct.
The lift singularChainsLift intertwines the elementary subdivision operator
with the categorical subdivision operator on arbitrary chains, by extending the
generator case via the universal property of the free abelian group.
Right-recursive formula for iterated endomorphisms: f^(k+1) = f^k ≫ f.
The lift singularChainsLift intertwines the $k$-fold iterated subdivision
operator with the $k$-fold composite of the categorical subdivision operator.
Any singular chain whose support consists of $\mathcal{A}$-small simplices lies in the subgroup of $\mathcal{A}$-small chains, by decomposing the chain into its coefficient-weighted generators.
The map singularChainsLift is injective; in fact it is an isomorphism, with
left inverse given by the coproduct descent that sends each 1 : ℤ at index b
back to the generator FreeAbelianGroup.of (e.symm b).
At each degree, the inclusion $S_n^{\mathcal{A}}(X) \hookrightarrow S_n(X)$ is injective: it factors as the subgroup inclusion followed by the injective lift.
Chain-level factoring: if the $k$-fold subdivision of c is $\mathcal{A}$-small,
then the iterated subdivision of the image of c in singularChainComplexZ X
factors through the inclusion from the small subcomplex.
Cycle-level factoring: given a cycle z represented by a chain c whose
$k$-fold subdivision is $\mathcal{A}$-small, the iterated subdivision of z lifts
to a cycle z' in the small subcomplex compatible with the inclusion.
Homology-level factoring: given a homology class y of $X$ and a cover
$\mathcal{A}$, there is some iterated subdivision $\mathrm{Sd}^k$ such that
$\mathrm{Sd}^k(y)$ lies in the image of the inclusion-induced map from
$H_n^{\mathcal{A}}(X)$.
The map $H_n^{\mathcal{A}}(X) \to H_n(X)$ induced by the inclusion of small chains is surjective, using that iterated subdivision is chain-homotopic to the identity.
The $k$-fold iterate of the subdivision operator $\mathrm{Sd}^k$ packaged as an additive group homomorphism on singular chains.
Instances For
Iterated subdivision preserves the property of being an $\mathcal{A}$-small chain.
The iterated subdivision $\mathrm{Sd}^k$ sends $\mathcal{A}$-small chains to $\mathcal{A}$-small chains, so it restricts to the subcomplex $S_*^{\mathcal{A}}(X)$.
The restriction of $\mathrm{Sd}^k$ to the subgroup of $\mathcal{A}$-small chains, as an endomorphism of that subgroup.
Instances For
Naturality of the singular boundary map under continuous maps: pushing forward a
chain along f commutes with taking the boundary.
The subdivision operator commutes with the boundary on the standard simplex,
verified by transporting to the categorical singular chain complex via
singularChainsLift where the corresponding statement is naturality of the
subdivision operator.
The subdivision operator $\mathrm{Sd}$ is a chain map: it commutes with the singular boundary $\partial$ on any chain in any space, reducing to the standard simplex case via naturality.
The iterated subdivision $\mathrm{Sd}^k$ is a chain map: it commutes with the
boundary operator, by induction on k from the single-step case.
The restricted iterated subdivision $\mathrm{Sd}^k$ on $S_*^{\mathcal{A}}(X)$ commutes with the (restricted) boundary map, so it is a chain endomorphism of the small chain complex.
The degree-n component of the iterated subdivision endomorphism on the small
chain complex.
Instances For
The iterated subdivision operator $\mathrm{Sd}^k$ as an endomorphism of the small chain complex $S_*^{\mathcal{A}}(X)$.
Instances For
A placeholder for the canonical $(n+1)$-chain on the standard simplex used to
witness the chain homotopy between $\mathrm{Sd}^k$ and the identity (Lemma 13.4).
The current definition is a trivial choice; the homotopy iteratedSubdivisionHomotopy
is otherwise sourced from Section13.
Instances For
The chain homotopy operator $h_k : S_n(X) \to S_{n+1}(X)$ witnessing
$\mathrm{Sd}^k \simeq \mathrm{id}$. It is obtained on each generator $\sigma$ by
pushing forward the universal chain stdHomotopyKChain along $\sigma$.
Instances For
On a single $\mathcal{A}$-small simplex $\sigma$, the homotopy operator $h_k$ produces an $\mathcal{A}$-small chain, since each simplex in its support has image inside that of $\sigma$.
The homotopy operator $h_k$ sends $\mathcal{A}$-small chains to $\mathcal{A}$-small chains, so it restricts to the small subcomplex.
The restriction of the homotopy operator $h_k$ to the subgroup of $\mathcal{A}$-small chains.
Instances For
The chain homotopy hom data $h$ between $\mathrm{Sd}^k$ and the identity on
the small chain complex: on the relevant degree relations $j = i + 1$ it agrees
with smallHomotopyOpK, and is zero elsewhere.
Instances For
The homotopy relation $\mathrm{Sd}^k = \partial h + h \partial + \mathrm{id}$ on each degree, witnessing that $\mathrm{Sd}^k$ is chain-homotopic to the identity on the small chain complex.
The chain homotopy on the small chain complex $S_*^{\mathcal{A}}(X)$ exhibiting $\mathrm{Sd}^k \simeq \mathrm{id}$ (Lemma 13.4, restricted to small chains).
Instances For
Key technical step for injectivity: a small cycle z whose image in $H_n(X)$ is
zero is, after applying enough iterated subdivisions, a boundary in the small chain
complex. The result extracts the chain b of full chains together with the
subdivision count k and a small preimage w.
A small cycle that becomes null-homologous after inclusion into $H_n(X)$ is
killed at the cycles level by some iterated subdivision: there exists k such that
$\mathrm{Sd}^k(z) = 0$ in $H_n^{\mathcal{A}}(X)$.
Homology-level kernel killing: any small homology class x mapping to zero in
$H_n(X)$ is annihilated by some iterated subdivision $\mathrm{Sd}^k$ on the small
chain complex.
The map $H_n^{\mathcal{A}}(X) \to H_n(X)$ induced by the inclusion of small
chains is injective. Combined with surjective_on_homology, this gives the
isomorphism asserted by the locality principle.
The inclusion of small chains induces an isomorphism on homology in degree n,
i.e. it is a quasi-isomorphism at n. Packages the surjectivity and injectivity
results together.
The Locality Principle (Theorem 11.4 / 13.5). For any cover $\mathcal{A}$ of a space $X$, the inclusion of $\mathcal{A}$-small chains $S_*^{\mathcal{A}}(X) \subseteq S_*(X)$ is a quasi-isomorphism; equivalently, the induced map $H_*^{\mathcal{A}}(X) \to H_*(X)$ is an isomorphism in every degree.