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.
LHS collapse for a cohomologically trivial normal subgroup
Statement
In the LHS setup with its DC or fully supplied-comparison convention, if for every , then inflation gives natural isomorphisms for every .
Facts & Assumptions
Given: The LHS hypotheses and the stated positive-degree vanishing for this coefficient module.
LHS has page with finite normalized filtration (Lyndon-Hochschild-Serre spectral sequence).
Vanishing of the positive inner derived functors makes the lower composite edge an isomorphism (Derived composition isomorphisms under total acyclicity).
Proof
All with are zero, while . For , a differential out of this bottom row has negative second coordinate, and one into it starts in a zero row. Induction over pages therefore gives .
In degree , the only possible quotient is at filtration index . The zero quotients before it imply , and , so this quotient is the whole target; this is also the lower-edge isomorphism of F2. To identify its map, use the morphism of extensions given by , , and , together with the -linear inclusion from the inflation of into . By F1's contravariant map-of-extensions naturality, it induces a map from the trivial-kernel LHS sequence for to the given sequence. The source sequence has only its row and its lower edge is the identity on . The induced map on the target is the usual restriction/coefficient map along , namely inflation, while the map on the bottom row is the identity because taking -invariants of recovers . Commutativity of the edge square therefore identifies the lower edge above with inflation. At it is ; for or a zero surviving quotient the finite filtration gives zero. The trivial normal group satisfies the vanishing automatically. All comparisons retain F1's precise DC or supplied-data convention.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
17 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
- Weibel, 6.8.2 (standard reference, not scraped)