TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

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.

Inflation-restriction exact sequence in degree one

Statement

Let $N ⊴ G$ and let $A$ be an abelian $G$ -group. Then the sequence

$0 \to H^{1} (G / N, A^{N}) \overset{Inf}{\to} H^{1} (G, A) \overset{Res}{\to} H^{1} (N, A)$

is exact.

Facts & Assumptions

Given: A normal subgroup $N ⊴ G$ and an abelian $G$ -group $A$ .

[L1]

Restriction and inflation in degree one are given by the explicit cocycle formulas of Restriction, inflation, and the quotient conjugation action on first cohomology.

[L2]

The crossed-homomorphism model agrees with the inhomogeneous degree-one model (The inhomogeneous one-cocycle model agrees with crossed homomorphisms in degree one).

Proof

technique · direct

1.1

Inflation is injective. Suppose $\overset{ˉ}{z} : G / N \to A^{N}$ inflates to a principal crossed homomorphism $g \mapsto g \cdot a - a$ on $G$ . For $n \in N$ , inflation gives $0 = \overset{ˉ}{z} (N) = n \cdot a - a$ , so $a \in A^{N}$ . Therefore the same formula already defines a principal cocycle on $G / N$ , and the class of $\overset{ˉ}{z}$ is zero.

givenL1algebra

1.2

Conversely, let $z : G \to A$ be a crossed homomorphism whose restriction to $N$ is trivial in $H^{1} (N, A)$ . Then there exists $a \in A$ such that $z (n) = n \cdot a - a$ for all $n \in N$ . Replace $z$ by the cohomologous cocycle $z^{'} (g) = z (g) - (g \cdot a - a)$ . Now $z^{'} ∣_{N} = 0$ .

L1L2choosealgebra

2.1

If $\overset{ˉ}{z} : G / N \to A^{N}$ is a cocycle, then its inflation vanishes on $N$ because $n N = N$ . Hence $Res \circ Inf = 0$ .

L1step 1.1algebra

2.2

If $n \in N$ and $g \in G$ , then $z^{'} (n g) = z^{'} (n) + n \cdot z^{'} (g) = n \cdot z^{'} (g)$ , while also $z^{'} (n g) = z^{'} (g (g^{- 1} n g)) = z^{'} (g) + g \cdot z^{'} (g^{- 1} n g) = z^{'} (g)$ because $g^{- 1} n g \in N$ and $z^{'} ∣_{N} = 0$ . Therefore $n \cdot z^{'} (g) = z^{'} (g)$ for all $n \in N$ , so $z^{'} (g) \in A^{N}$ . Also $z^{'} (g n) = z^{'} (g) + g \cdot z^{'} (n) = z^{'} (g)$ , so $z^{'}$ is constant on cosets of $N$ .

step 1.2algebra

3.1

Define $\overset{ˉ}{z} : G / N \to A^{N}$ by $\overset{ˉ}{z} (g N) = z^{'} (g)$ . Step 2.2 shows this is well defined, and the crossed-homomorphism identity for $z^{'}$ implies that $\overset{ˉ}{z}$ is a cocycle on $G / N$ . By construction, inflating $\overset{ˉ}{z}$ gives $z^{'}$ , so the original class of $z$ lies in the image of inflation. Hence $\ker Res = im Inf$ .

L1step 2.2step 2.1

4.1

Steps 1.1, 2.1, and 3.1 prove exactness of the displayed sequence.

step 1.1step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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

Chaoli Li, Class field theory: proofs (standard reference, not scraped)