Automorphisms of an abelian extension
Abstract
Endpoint-fixing automorphisms of an arbitrary abelian group extension, modulo actual kernel conjugations, form its first cohomology group.
Theorem 1.1 (Defects, twists and actual inner automorphisms).
Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/AbelianExtensionH1.classification (✓ std3). ∎
Source. Repository-derived.
Acknowledgement. Brian Conrad (2012). Math 210B. Group cohomology and group extensions. URL: https://virtualmath1.stanford.edu/~conrad/210BPage/handouts/gpext.pdf.
Commentary.
In the formula, A = automorphisms E, Z = cocycles1 (coefficients E), D = defectEquiv E, I = innerKernel E, and H = H1 (coefficients E). The maps i and p are E.inl and E.rightHom. The symbol u is Additive.toMul on N, ofMul is Additive.ofMul on A, U(a,y) is a.toMul.val y, and T(d,y) is ((defectEquiv E).symm d).toMul.val y. AddEquiv denotes an additive group isomorphism. These abbreviations retain all four conjuncts and the complete small-type telescope.
Let N be any commutative group, Q and S groups, and E an actual short exact sequence 1 to N to Q to S to 1. Write i for its injection and p for its projection. The quotient action on N is descended from conjugation in Q: i(rho(p(y))(n)) = y i(n) y inverse for every y and n. No group section is assumed. The integral representation coefficients E has underlying additive group Additive N and precisely this action.
The subgroup automorphisms E consists of automorphisms of Q that fix i(N) pointwise and induce the identity on S. Its multiplication is ordinary composition. The additive equivalence defectEquiv sends such an automorphism a to the unique cocycle d satisfying i(d(p(y))) = a(y) y inverse for every lift y. The formula holds for every y, so the cocycle is independent of any chosen set-theoretic lift. Conversely its inverse sends d to the automorphism y maps to i(d(p(y))) y. The cocycle relation is d(st) = rho(s)(d(t)) + d(s), which equals the source order because N is commutative. Composition corresponds to cocycle addition, and the inverse twist corresponds to negation.
The homomorphism classMap takes this defect to Mathlib H1. Its kernel innerKernel is characterized exactly by the existence of b in N such that a(y) = i(b) y i(b) inverse for every y. The inner defect is b minus rho(s)(b). Mathlib writes coboundaries as rho(s)(c) minus c; the proof uses c = minus b. Thus the displayed additive quotient is the actual automorphism group modulo actual inner-kernel automorphisms, and is isomorphic as a group to general-action H1.
For the section 27 source carriers, retain the original hypotheses that pi is finitely generated, N is finite-index and characteristic, S = pi/N is finite with trivial center, and ell is prime. Define N_ell inside pi as the subgroup generated by [N,N] together with every ell-th power from N (the notation N^ell therefore means generated subgroup), then set V_ell = N/N_ell and Q_ell = pi/N_ell. Characteristicity of N makes both factors of N_ell characteristic in pi, so N_ell is normal and N_ell is contained in N; the commutator factor makes V_ell abelian. The quotient maps induced by N inclusion and pi/N_ell -> pi/N give the actual exact extension 1 -> V_ell -> Q_ell -> S -> 1. The compiled application instantiates the theorem above with that extension, so every classification formula is on the original quotient carriers rather than on an unrelated arbitrary E.
Under this substitution, the induced action is the source lambda: for s represented by x in pi and v represented by n in N, the extension action satisfies i(rho(s)(v)) = x i(v) x inverse, hence rho(s)[n] = [x n x inverse] in V_ell. The quotient construction proves independence of the lift because N_ell contains [N,N]. This attaches the defect, cocycle and inverse formulas to the actual section 27 extension. The following application constructs the adjusted Lambda action, its normalized representatives and its K_ell/C_ell map on these same carriers.
For the complete outer-action application, put R = N_ell, V = N/R and Q = pi/R, with the injection i induced by N inclusion and projection p to S = pi/N. Here N/R denotes N modulo the inverse image of R under its inclusion in pi. Let A be the inverse image of Lambda under Aut(pi) -> Out(pi), where Out means the quotient by the range of actual conjugations. Characteristicity gives homomorphisms q: A -> Aut(Q), t: A -> Aut(V), and u: A -> Aut(S). The hypothesis on Lambda says precisely that every u(eta) is inner; it does not say u(eta) is the identity. Since S has trivial center, conjugation S -> Aut(S) is injective. Its unique inverse on u(A) gives a homomorphism s: A -> S with u(eta) = Ad(s(eta)).
The coefficient action is exactly the deck action lambda. Naturality of conjugation gives t(eta) lambda(z) t(eta) inverse = lambda(s(eta) z s(eta) inverse). Thus lambda(s(eta)) inverse t(eta) commutes with every lambda(z). Each element of V has ell-th power one because R contains every ell-th power from N, so Additive V carries its canonical ZMod ell module structure, including when V is zero. Every additive homomorphism of this group is ZMod ell linear (ZMod.map_smul). Extending lambda linearly to the group algebra therefore identifies the corrected map with an automorphism of the original F_ell[S] module, rather than merely naming a centralizer as its codomain.
For eta and zeta in A, uniqueness gives s(eta zeta) = s(eta)s(zeta). The covariance identity above implies that the corrected maps multiply. If eta is replaced by Ad(x) eta, its t is left multiplied by lambda(x bar) and its s is left multiplied by x bar, so the corrected map is unchanged. In particular it kills every inner automorphism of pi. Descending along A -> Lambda defines the homomorphism Psi on the given subgroup Lambda of Out(pi); its formula holds for every automorphism representative of every element of Lambda.
Independently, q followed by Aut(Q) -> Out(Q) kills the inner automorphisms of pi, since q(Ad(x)) = Ad(x mod R). Its descent is the actual induced outer action a: Lambda -> Out(Q). Define C = ker(a) and K = ker(Psi) in this same Lambda. If q(eta) = Ad(w), its base action is Ad(p(w)); uniqueness forces s(eta) = p(w), and its V action is lambda(p(w)). Hence Psi is one and C is contained in K. This uses triviality of the center of S only; the center of Q and the kernel of lambda may be nontrivial.
For gamma in K, choose any eta in A representing gamma and any r in Q with p(r) = s(eta). Define beta = Ad(r inverse) q(eta). The quotient action of beta is the identity, and its V action is lambda(s(eta)) inverse t(eta) = one. Thus beta belongs to automorphisms E for the original extension. Define h(gamma) = classMap E (Additive.ofMul beta), regarded in Multiplicative(H1 (coefficients E)) when writing group homomorphisms multiplicatively. The first conjunct of classification identifies its defect for every y in Q by i(d(p(y))) = beta(y)y inverse; no arbitrary equivalence selected from the last Nonempty conjunct defines h.
If r is replaced by r prime with the same projection, beta prime = Ad(r prime inverse r) beta and r prime inverse r lies in i(V). The third conjunct of classification sends this inner factor to zero under classMap. If eta is replaced by Ad(x) eta, the compatible normalization lift is (x mod R) r, for which beta is exactly unchanged; the preceding lift calculation covers every other normalization lift. Two representatives of the same element of Out(pi) differ by such an actual inner automorphism. Consequently h is independent of both choices.
To check multiplication without assuming a section is a homomorphism, choose representatives eta, zeta and normalization lifts r, t, and write beta, delta for their normalized automorphisms. Then q(eta zeta) = Ad(r beta(t)) beta delta. For any normalization lift v of s(eta zeta), the normalized product is Ad(v inverse r beta(t)) beta delta. Its conjugating element has projection s(eta zeta) inverse s(eta)s(zeta) = one, so it lies in i(V). The actual classMap kills this inner factor and is additive on beta delta by defectEquiv. Thus h is a group homomorphism on the actual K, including for nonsplit extensions.
Finally h(gamma) is one exactly when beta = Ad(i(b)) for some b in V, by the third conjunct of classification. In that case q(eta) = Ad(r i(b)), so gamma belongs to C. Conversely, if gamma belongs to C and q(eta) = Ad(w), the equality of base actions and the trivial center of S give p(w) = s(eta) = p(r). Therefore r inverse w lies in i(V), beta is its inner automorphism, and h(gamma) is one. The kernel of h is exactly C restricted to K. The standard quotient-by-kernel injection then gives K/C -> H1 for the original coefficients.
Mathlib uses d(st) = s.d(t) + d(s), equal to the source order since V is abelian, and boundaries s.c minus c. The source writes b minus s.b; substitution c = minus b gives precisely the same boundary subgroup. The integral representation used by coefficients records the original additive V and deck S action, so this change of notation changes neither cocycles nor their quotient. No coprimality, splitting, faithful deck action, nonzero coefficient, or trivial representative action on S enters this derivation. Finite generation and finite index are needed for the separate finiteness and dimension claims, not for this outer-action argument.
The outer-action application assembles the actual quotient homomorphisms, the original module action and classMap. The classification does not establish the additional finite elementary-abelian and coprime consequences, the surface intersection form and dimension statements, or finite-target factorization.
The classifier permits nonsplit extensions, nontrivial actions, infinite groups, arbitrary characteristic and the trivial coefficient group. In its outer-action application, characteristicity supplies the quotient homomorphisms and the trivial center of S supplies the unique base conjugator. Neither condition imposes a splitting, a faithful deck action or a restriction on the prime.
Conrad section 2.1 states the simply transitive H1 action on the quotient set for arbitrary extensions. The composition-compatible equivalence is established here using the pinned Mathlib extension and cohomology APIs. This is a formal construction of a classical extension-theoretic correspondence, with no claim of literature novelty.