LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09

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.

The kernel of degree-two inflation is the transgression image

Statement

Assume AC. The map $\inf : H^{2} (Q, A^{N}) \to H^{2} (G, A)$ is pullback along $π : G \to Q$ followed by coefficient inclusion $A^{N} ↪ A$ . Then $\ker \inf = im Tra$ . H2 denotes normalized bar cohomology, with its inherited derived interpretation.

Facts & Assumptions

Given: AC, the group extension, module A and B=A^N.

[F1]

For a Q-invariant class, $L = N_{A ⋊ G} (D)$ projects onto G with kernel B, and Tra is L/D (Low-degree transgression for a group extension).

[F2]

Pullback then abelian coefficient pushout realizes inflation on bar H2 (Pullback and coefficient pushout realize bar cohomology maps).

Proof

1.1

For a transgression class let E0=L/D. Its pullback to G is isomorphic to L by $l \mapsto (l D, p (l))$ . Injectivity follows from $D \cap \ker p = 1$ . For a pair (lD,g) in the pullback, $p (l)^{- 1} g \in N$ and multiplication by its unique lift in D corrects p(l) to g, proving surjectivity. This isomorphism fixes the kernel B. Pushing L out to A gives the group $(A ⋊ L) / {(- b, (b, 1)) : b \in B}$ . The homomorphism $(a, l) \mapsto (a, 1) l$ onto $A ⋊ G$ has exactly that kernel: its value is the identity only if $l = (- a, 1) \in B$ . It is onto since L maps onto G. Thus the inflated extension is split, and its class is zero.

F1F2givenalgebra

1.2

Conversely let $0 \to B \overset{i_{0}}{\to} E_{0} \to Q \to 1$ have zero inflated class. Form $P = E_{0} \times_{Q} G$ and $E = (A ⋊ P) / S$ , $S = {(- b, (i_{0} (b), 1)) : b \in B}$ . By F2 this is the inflated extension. The map $j : P \to E$ , $p \mapsto [(0, p)]$ , is injective, since membership of (0,p) in S forces b=0 and p=1. Its intersection with A is precisely B. In P the subgroup $U = {(1, n) : n \in N}$ is normal, has trivial intersection with B and projects isomorphically onto N. Put $D = j (U)$ .

F2givenalgebra

2.1

The normalizer of D in E is exactly j(P). One inclusion follows because U is normal in P. Every e in E is a product a j(p); if e normalizes D then a does. Conjugation by a sends the unique D-element over n to itself exactly when $n a = a$ for every n, because its commutator is the kernel element $a - n a$ . Hence such a belongs to B, already in j(P), proving the other inclusion. Therefore $N_{E} (D) / D = j (P) / j (U) ≅ E_{0}$ via the first projection of P. This isomorphism fixes the identified B and Q.

step 1.2algebra

3.1

Since the inflated class is zero, E is equivalent to the split extension $A ⋊ G$ by the classification implicit in F2. Carry D through this equivalence. It is the graph of a crossed map d on N, and its normalizer projects onto G, so the normalizer equation of F1 shows [d] is Q-invariant. Step 2.1 identifies its normalizer quotient, with both kernel and quotient fixed, with the original E0. Hence $Tra [d] = [E_{0}]$ . Together with step 1.1 this proves both inclusions. In particular no injectivity of $H^{2} (G, B) \to H^{2} (G, A)$ was used.

F1F2step 1.1step 2.1algebra∎

Depends on

Used by

The inflation–restriction–transgression five-term sequence Theorem

Dependency tree · two levels

6 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

Dekimpe–Hartl–Wauters, A seven-term exact sequence for the cohomology of a group extension, Sections 2–5 pp.2–11 and Section 10.2 p.21 (standard reference, not scraped)