How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Homological Lyndon–Hochschild–Serre spectral sequence for group extensions
Statement
Assume the Axiom of Choice. For every short exact sequence of discrete groups the homological Serre spectral sequence of the induced map of classifying spaces has Here denotes homology of with the local coefficient system determined by the left -module , and group homology uses the bar classifying spaces. The coefficient group has the -action induced by conjugation by lifts in , and convergence is strong with the finite Serre filtration in each total degree.
Statement references
Facts & Assumptions
Given: Full AC and a short exact sequence of discrete groups.
Full AC, written AC, is The Axiom of Choice.
Full AC implies DC: apply AC to the family of nonempty successor sets of a serial relation, choose one initial element, and recursively follow the resulting choice function. The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain
Under AC, Milnor's classifying space is a connected CW model with and for . The classifying space of a discrete group is a K(G,1)
The homotopy long exact sequence of a Serre fibration computes the homotopy groups of its fiber. Long exact sequence of homotopy groups of a fibration
For a Serre fibration over a path-connected CW complex, the homological Serre spectral sequence has and strongly converges to the homology of the total space. Homological Serre spectral sequence
The homology of a classifying space with the local system determined by a module is the usual bar-model group homology; the derived-functor identification in the library assumes DC. Diagonal bar coinvariants compute group homology, The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain
Connected CW models with the same identified fundamental group and vanishing higher homotopy groups are homotopy equivalent under AC. Existence and homotopy uniqueness of Eilenberg--Mac Lane spaces
External input: For a map between CW complexes, its mapping-path homotopy fiber has CW homotopy type. This is the homotopy-fiber consequence of Milnor's compact-domain mapping n-ad theorem, stated explicitly in Hatcher's §4.3; the hypotheses here are satisfied by the classifying CW models in step 1.1. [Hatcher §4.3, p. 408], [Milnor, Theorem 3, pp. 276–280]
Classifying maps commute up to based homotopy with a based map and its induced fundamental-group homomorphism. Classifying maps are natural up to based homotopy
Proof
Given: The group extension and [A1].
Choose connected CW models from [L1]. Build a based map inducing by mapping the one-skeleton to loops representing the quotient images, filling each two-cell because its attaching word maps to the identity in , and extending over each higher cell because for . The finite cell extensions are simultaneous over a set of cells; [A1] supplies those choices. Replace this map by its mapping-path fibration ; the total space is homotopy equivalent to , and the fiber is its homotopy fiber.
The map on fundamental groups is the quotient . Exactness of [F1] gives , , and for every , because both and have zero higher homotopy groups by [L1]. By the external input [F5], has CW homotopy type. Choose a connected CW model and identify with . The uniqueness theorem [F4] gives , so for every .
A lift of a loop class transports the fiber fundamental group by . Choose a based homotopy equivalence as in step 2.1 and a based homotopy inverse , using the basepoint path supplied by the transport. The map is a based self-map of inducing on . By [F6], the classifying map satisfies , so the monodromy on agrees under with the bar-classifying-space map induced by . If a different lift is chosen, it differs by an element of and changes this map by an inner automorphism of . Inner conjugation is homotopic to the identity on the bar classifying space: the conjugation functor on the one-object category of is naturally isomorphic to the identity by the conjugating element. Hence the induced action on depends only on , and is exactly the stated -module action.
Apply [F2] to . By step 2.1 the fiber homology is , and step 3.1 identifies its monodromy local system with the conjugation action. Therefore the page is and the spectral sequence strongly converges to .
The total-space equivalence from step 1.1 identifies with . By [F4], this classifying CW model is homotopy equivalent to the bar model used in [F3], so its homology is . The base and fiber are connected CW models, so the Serre filtration is first quadrant and finite on each total-degree diagonal. AC supplies the DC hypothesis of [F3] by [L2]. The fiber action and Serre filtration introduce no further choice.
Depends on
- The Axiom of Choice
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
- The classifying space of a discrete group is a K(G,1)
- Existence and homotopy uniqueness of Eilenberg--Mac Lane spaces
- Long exact sequence of homotopy groups of a fibration
- Homological Serre spectral sequence
- Diagonal bar coinvariants compute group homology
- Classifying maps are natural up to based homotopy
Used by
Dependency tree · two levels
54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- John McCleary, Nontrivial fundamental groups, §8bis.2 (standard reference, not scraped)
- Allen Hatcher, Algebraic Topology (standard reference, not scraped)
- John Milnor, On Spaces Having the Homotopy Type of a CW-Complex (standard reference, not scraped)