Galois cohomology

Continuous Galois cohomology and its finite-group models. Includes Kummer and Artin–Schreier theory, low-degree exact sequences, cup products, transfer and pro-p cohomology.

Collects root characters, finite restriction kernels, prime-degree actions, valuation characters, and the associated vanishing and detection results.

A moved additive class gives a moved continuous absolute Galois character. The construction uses the separable closure and therefore does not require that the field be perfect.

Additive Hilbert 90 realizes every character by a root. Changing the field element by an Artin–Schreier coboundary leaves its character unchanged.

Trace averaging and the Artin–Schreier exact sequence give explicit locally constant primitives for two-cocycles with values in the prime field.

Root differences commute with the actual absolute Galois restriction maps. Simultaneous approximation of additive classes therefore prescribes characters.

The Frobenius-fixed elements are exactly the prime field. Thus the difference between a root and its Galois translate gives a continuous cyclic character.

Canonical aggregate generated by the reviewed rehome.

For a finite cyclic group generated by g, mathlib computes odd group cohomology using Rep.FiniteCyclicGroup.subCompNormHom A g. The canonical boundary comparison identifies that short-complex homology with tateCohomology…

Focused aggregate for Herbrand finiteness and low-degree calculations.

This file supplies the finiteness clause in Herbrand-quotient multiplicativity: for a short exact sequence of modules over a finite cyclic group, if the Herbrand quotients of any two terms are defined, then the quotient…

Public aggregate for the low-degree Tate quotients, their cardinality and exact-sequence calculations, and the resulting Herbrand quotient theory.

This reusable implementation supplies the low-degree cyclic cohomology used by the class-formation and local class field theory layers.

This specializes the dependent-product calculation to two possibly different coefficient groups. It is used to join the unrestricted and integral parts of a supported idele group.

For a short exact sequence of finite cyclic modules, this module applies mathlib's homology long exact sequence to the standard two-periodic cyclic complex. The resulting cardinality identity is transported to the arithm…

The foundational constructions and their comparison with mathlib Tate cohomology are split into focused modules. This public module retains the Herbrand quotient and its multiplicativity result.

An equivariant multiplicative equivalence identifies fixed elements, norm kernels, norm images, and augmentation images. Consequently it induces equivalences on the concrete low-degree Tate cohomology groups and preserve…

This file isolates the elementary cardinal arithmetic at the end of the low-degree Herbrand quotient calculation. If a finite low-degree Tate quotient has Herbrand quotient equal to a natural number n, then its degree-ze…

This file proves that multiplicative Tate H⁰ and H⁻¹ commute with dependent products, giving the product step for low-degree Herbrand quotients.

Comparisons between arithmetic Herbrand quotient presentations and mathlib Tate cohomology.

This file supplies the multiplicative induced-module model used in the Herbrand quotient calculation. If H ≤ G acts on a commutative group B, then IndH^G B is represented by the equivariant functions f : G → B, f (h x) =…

Provides the public declarations in the CyclicCohomology.Herbrand.LowDegree Lean module.

Provides the public normal-basis lattice declarations used in Herbrand computations.

This file proves the permutation-stable sublattice lemma. The proof also handles a permutation basis with more than one orbit: approximate every large coordinate vector by a lattice point and average all these approximat…

This file connects the complete permutation sublattice with its orbit-stabilizer Herbrand quotient calculation.

This file supplies the abstract cohomology calculation for permutation lattices. It proves the value of the Herbrand quotient on the trivial integer lattice, transports that calculation through Shapiro's lemma to transit…

This file defines the integer-unit quotient by a principal-unit subgroup and compares it with the concrete quotient used in the normal-basis calculations.

Provides the public declarations in the CyclicCohomology.Herbrand.PrincipalUnits.QuotientTower Lean module.

This file extracts the cardinality consequence of the product decompositions of low-degree Tate cohomology, giving the corresponding product formula for Herbrand quotients.

Let S be a stable subgroup of a commutative G-group A, and let P be another stable subgroup. If S ⊔ P = ⊤, every class modulo P has a representative in S. This file upgrades the resulting second isomorphism S / (S ∩ P) ≃…

Mathlib's Rep ℤ G currently requires the coefficient ring and acting group to inhabit the same universe. Since ℤ : Type 0, every representation-bearing part of local class field theory uses this single named boundary. Ke…

This file formalizes the cyclic norm-kernel vanishing condition as a property, not as a new Lean axiom, and the finite-cyclic cohomology calculation using the actual finite-cyclic group-cohomology computation. The constr…

This file identifies mathlib's Tate cohomology in degrees 0 and -1 with the standard finite-cyclic short complexes. It adds no alternative cohomology model: both targets are the homology objects already defined by mathli…

Focused aggregate for the standard Tate object and its arithmetic comparisons.

The actual invariant submodule of the unit representation, together with its arithmetic identification with the units of the base field.

This module identifies degree-zero Tate cohomology of the multiplicative group of a finite Galois extension with the corresponding field norm quotient.

The representation norm on the units of a field extension lands in the invariant units. Its image defines the norm submodule, and the quotient of the invariant units by this submodule realizes degree-zero Tate cohomology…

Collects finite algebraic constants, finitely generated field models, roots, integral-closure torsion, and additive cohomology results.

In a finite Galois extension, an element of trace one gives an explicit coboundary. A locally constant cocycle on an infinite Galois group descends to a finite Galois field, so the same construction applies.

A finite relative algebraic closure contains all roots of unity. It also supplies an element outside the image of every map x ↦ x ^ n - x, for n > 1.

If every nonzero element of a field is carried to a scalar multiple of itself by scalars in a fixed proper subfield, a unital ring endomorphism is the identity. The proof compares an element outside the subfield with its…

Canonical aggregate generated by the reviewed rehome.

This file develops the actual augmentation quotient IG / IG² used in the transfer/augmentation comparison. It is kept separate from the transfer calculation so that the group-ring identities can be reused in the proof of…

This file isolates the finite-group inputs for prime-power and normal-closure splitting arguments. For the prime-power subgroup reduction, a proper subgroup of a finite group of order p ^ v is contained in a subgroup of…

The product of all translates is fixed by the acting finite group. If a commuting automorphism changes the original element by a fixed factor, it changes the orbit product by that factor raised to the group's cardinality…

The coefficient trace is the existing finite-index coinduction-induction isomorphism followed by the induction counit. Its composite with the coinduction unit is the index. Shapiro then supplies the vanishing intermediat…

A nontrivial finite p-group has a central subgroup of order p. Its fixed field gives a smaller Galois p-extension of the base, with a cyclic prime-degree extension on top. This constructs the intermediate field needed fo…

If two subgroups generate a commutative group, every class modulo the second subgroup has a representative in the first. This is the precise group-theoretic comparison used when a sufficiently large group of supported id…

This file supplies the type-level equivalences between the quotient of a subgroup and the corresponding quotient after viewing that subgroup inside a larger group. They complement Mathlib's natural-number relative-index…

This file isolates a group-theoretic criterion for identifying the image of a subgroup with the kernel of a homomorphism after a surjective quotient.

This file constructs the transfer on abelianizations and the concrete relative augmentation quotient (IH + IG IH) / IG IH. The two vertical augmentation maps in the transfer square are developed from the integral group r…

For a finitely generated group G with finite abelianization, the transfer from G / G' to G' / G'' is trivial. The proof follows Witt's group-ring argument. This file first constructs the required right Fox coefficients d…

For an arbitrary characteristic-zero field, the p-th roots of unity in its algebraic closure form a discrete ZMod p-module with the natural (generally nontrivial) absolute-Galois action. This file constructs that coeffic…

When the base field contains a primitive p-th root of unity, the natural absolute-Galois action on mup is trivial. A chosen primitive root gives a continuous ZMod p-linear equivalence with the standard trivial coefficien…

Canonical aggregate generated by the reviewed rehome.

This file connects elements produced in the invariant subtype AM to the ambient representation A. A cyclic radical with trivial stabilizer in GK / GM is fixed in the ambient module by exactly GM. Consequently, a family o…

abelian extension The proof of the finite abelian Kummer decomposition reduces a finite abelian extension to cyclic subextensions. This file supplies the group-theoretic source for that step. A finite commutative group i…

abstract-operator step This file isolates the finite cyclic step in the proof of the finite abelian Kummer decomposition. It does not claim the full Kummer correspondence. In additive notation, we use a fixed kernel elem…

For an equivariant additive operator wp, the construction defines Delta = wp(AL) ∩ AK. Here fixed modules are represented as ambient additive subgroups. The finite abelian assembly supplies finitely many elements in wp⁻¹…

in this construction, for a subset S of the coefficient module, K(S) is the abstract field whose subgroup consists of the elements of GK fixing every member of S. This file constructs that subgroup and proves that it is…

operator This file constructs, rather than assumes, the endomorphism of AL induced by a global equivariant endomorphism wp : A ⟶ A. It also embeds a GK-fixed global kernel element into the invariant subtype defining AL a…

Canonical aggregate generated by the reviewed rehome.

Semilinear conjugation descends through the closed commutator subgroup. The result is independent of the chosen lift to the algebraic closure and gives a covariant action of base-field automorphisms. A changed continuous…

Precomposition with inverse conjugation gives a left action. Its group law uses independence from the chosen extensions to the algebraic closure.

Average cyclic absolute characters over a finite relative Galois group. The average is invariant under the relative action and preserves a common orbit value when the group order is coprime to the character modulus.

A chosen extension of a field automorphism to its algebraic closure conjugates base-linear automorphisms to base-linear automorphisms. Root quotients transform by the same extension; this is the concrete identity underly…

Inverse semilinear conjugation preserves continuity. Restricting the algebraic character action therefore gives the action on continuous abelian characters.

The character action with trivial coefficients gives the additive action on H¹. Restriction along relative Galois automorphisms gives the action for an extension.

Triviality of the relative action on H¹ gives invariance under forward conjugation by applying the inverse automorphism's action. The constructed closure comparison then gives invariance under any actual semilinear lift.

When a field automorphism fixes the roots of unity, inverse-conjugation pullback sends a Kummer character to the character of the transformed unit. The fixed coordinate identification with cyclic coefficients preserves t…

The absolute Kummer character of a power class evaluates as the Galois quotient of any root with the prescribed power.

For a field containing a primitive n-th root of unity, this file identifies K× / K×ⁿ with continuous characters of the absolute Galois group. The target is first the discrete group of n-th roots of unity and is then iden…

The Kummer character of a transformed unit, evaluated at the conjugated Galois automorphism, is the transformed original character value. When the base automorphism fixes the roots of unity, the coefficient value is unch…

Base automorphisms act on the actual residual quotient of the absolute Galois group. After topological abelianization the action is independent of the selected semilinear lift, and composition agrees with composition on…

Restriction along the inverse field automorphism and conjugation by a chosen extension of the field automorphism agree on all commutative characters.

When a base automorphism acts by a specified power on the roots of unity, its chosen lift acts by that power on the same roots in the algebraic closure. The roots are descended using an actual primitive root in the base…

Collects concrete Kummer extensions, character correspondences, root actions, restriction kernels, finite approximations, and S-unit preparations.

When the prime is different from the field characteristic, extension of completion characters separates every class in the local abelian quotient.

A continuous character from an infinite Galois group to a discrete group factors through the Galois group of a finite Galois intermediate field.

A locally constant multiplicative cocycle descends to a finite Galois stage. An open normal subgroup in its identity fiber fixes every cocycle value, so the finite-stage cocycle takes values in that actual intermediate f…

Over a separably closed Galois extension, Hilbert 90 writes a continuous multiplicative cocycle as a coboundary. Taking a root of that actual coboundary parameter lifts the cocycle, preserving local constancy and the roo…

For a fixed separable closure Omega/K, a positive integer n, and enough n-th roots of unity in K, admissible subgroups of Kˣ correspond to abelian Galois intermediate extensions whose Galois groups have exponent dividing…

A cyclic Galois extension whose Galois group has exponent dividing n is generated by a single element whose n-th power lies in the base field, provided the base field contains a primitive n-th root of unity.

Aggregate for the concrete cyclotomic fields, characters, and profinite unit decompositions used by Kummer theory.

The compiled child modules combine the local decompositions of all ℤ[p]ˣ into a splitting of ℤ̂ˣ with one torsion-free profinite-integer factor and a product of finite groups.

This module contains the reusable, inexpensive product equivalences used by the compiled stages of the profinite-unit decomposition.

This file assembles mathlib's p-adic cyclotomic characters of the actual extension rationalCyclotomicField / ℚ. Their product takes values in the canonical product of the local unit groups, and the topological Chinese-re…

Finite cyclotomic levels are detected by their prime-power reductions, using mathlib's Chinese-remainder equivalence for ZMod. Surjectivity is obtained from the finite-intersection property for the closed fibers of the r…

This file constructs the actual field ℚ(μ∞) inside SeparableClosure ℚ. It uses mathlib's general IsCyclotomicExtension API, so the infinite field and its finite cyclotomic levels are not replaced by abstract copies of th…

The rational cyclotomic construction takes the fixed field of the closure of the torsion subgroup in Gal(ℚ(μ∞)/ℚ). This file defines that actual closed subgroup and fixed field. No copy of the Galois group is replaced de…

Hilbert 90 and compatible primitive-root coordinates lift actual locally constant cocycles from modulo p to modulo every positive power of p.

Weak approximation for cyclic characters descends from a prime cyclotomic extension using an invariant character lift and restriction at each completion. The resulting simultaneous approximation applies whenever the prim…

This file records two structural facts about the concrete cyclotomic-field model: it admits a primitive generator of the defining order, and divisibility of orders induces an algebra homomorphism between the correspondin…

A finite cyclotomic image would yield a finite fixed field containing all primary roots of unity. The actual primitive roots contradict finiteness.

When an automorphism acts by the same power on a unit's power class and on the roots of unity, Kummer naturality cancels these two actions. Coprimality of the exponent makes the power map injective on the character value…

The orbit product of an eigenunit's Kummer character is invariant under the upper cyclotomic group. The commuting automorphism changes it by the root's Kummer character to the cyclotomic degree. Coprimality prevents this…

The fixed field of an open subgroup is finite over the base. Its actual relative Galois group supplies the cocycle lift without extra hypotheses.

An invariant character of a finite normal intermediate field descends across a coprime degree. If the lower automorphism acts trivially on H¹, every lift to that intermediate field fixes this character. The proof constru…

For an abelian Galois intermediate extension E/K of exponent dividing n, adjoining in the ambient algebraic closure all n-th roots belonging to the actual radical subgroup of E recovers E itself.

The chosen map of algebraic closures restricts to the separable closures and carries root quotients to root quotients. This gives the naturality of Kummer characters under actual absolute Galois restriction, in every cha…

For an actual finite Galois extension L/K, this file constructs Delta = {a : Kˣ | there is beta : Lˣ with beta ^ n = a} as a subgroup, chooses one root for each element only after the subgroup has been constructed, and p…

This file supplies the first missing finite-duality source for the full subgroup/extension correspondence in the Kummer correspondence. Characters of a finite abelian group killed by n can be chosen with values in μₙ, an…

For a finite abelian Galois extension of exponent dividing n, the Kummer pairing identifies the Galois group with the character group of the actual radical quotient.

Let L/K be a finite abelian Galois extension whose Galois group is killed by n, and suppose that K contains a primitive n-th root of unity. This file proves that L is generated over K by all nonzero beta : L such that be…

For a nontrivial chosen simple Kummer extension, this file chooses a cyclic generator whose Kummer root character is the inverse of the selected primitive root. It also records the coefficient morphism for a tower of int…

Membership in K(√[n]{Δ}) uses only finitely many of the adjoined roots. For such a finite root set this file chooses the corresponding coefficients in Δ, records them in a finite subset of Kˣ, and forms the subgroup they…

For a finite normal intermediate field, the actual quotient conjugation action on its fixing subgroup agrees with the canonical absolute Galois action after a constructed continuous comparison of the abelianizations.

Transport an absolute character of a finite normal intermediate field to its actual fixing subgroup. The established comparison of conjugation actions preserves invariance. Transfer divided by the extension degree then e…

Restriction supplies the base map of an ambient automorphism. The fixing subgroup equivalence intertwines its actual subgroup conjugation with that semilinear conjugation, and therefore intertwines their abelianized acti…

For a finite normal intermediate field in a separable closure, the actual quotient conjugation action on its fixing subgroup agrees with the canonical absolute Galois action after a constructed continuous comparison of t…

The usual algebraic identification of the fixing subgroup with the relative Galois group is a homeomorphism for the Krull topologies. Finiteness of the intermediate field suffices; no normality or algebraicity of the amb…

The comparison on topological abelianization identifies the values of a continuous abelian character after actual and chosen semilinear conjugation.

Changing the algebraic closure intertwines concrete semilinear conjugation with the canonical action on topological abelianization. Both the closure equivalence and the comparison are constructed from the given field dat…

A base-linear field equivalence conjugates the relative Galois groups and preserves their Krull topologies. A finite intermediate field pulls back to a finite intermediate field under the inverse equivalence, so no algeb…

Hilbert 90 and multiplicative cocycle statements used by the concrete Kummer correspondence.

Continuous characters of an infinite Galois group factor through finite Galois stages. Finite Kummer surjectivity at such a stage then supplies a radical representative in the ambient extension.

For an infinite Galois extension Ω/K, a Kummer character attached to a chosen root β is already determined on the finite Galois normal closure of K(β). Equivalently, its kernel contains the fixing subgroup of that finite…

For an arbitrary Galois extension Ω/K, each element of Ω lies in a finite Galois intermediate field. If the full Galois group is abelian and killed by n, restriction gives the same two properties at that finite stage. Th…

Any radical appearing in K(√[n]{Δ}) uses only finitely many of the adjoined roots. The corresponding admissible finite-support subgroup Δ₀ ≤ Δ gives a finite Galois Kummer stage. Applying the finite inverse theorem at th…

A finite Galois extension containing the required roots of unity admits a simultaneous lift of prescribed completion characters. Averaging the lift over the Galois group gives invariance while retaining every local chara…

Kummer naturality and invariance identify the transformed unit class with the power prescribed by the action on roots. Injectivity of the Kummer equivalence gives a witness in the original field unit group. This directio…

For E = K(√[n]{Delta}), this file packages the canonical transposed Kummer pairing Gal(E/K) → Hom(Delta / Kˣⁿ, mun(E)). Its Galois-side injectivity is obtained from the fact that the internal Kummer roots generate E; thi…

Finiteness of the prime-power roots gives a maximal primitive-root exponent. At this exponent a primitive root of prime order has nonidentity power class.

For a positive integer n that is nonzero in a nonarchimedean local field, the Kummer extension obtained by adjoining all n-th roots is finite.

This file packages the complete-DVF derivative criterion for a field extension generated by an n-th root of a unit, with n itself a unit in the base field. The statement is independent of the global Kummer construction s…

The largest admissible Kummer subgroup is the full unit group. Its restricted radical quotient is canonically the ordinary power-class group.

Finiteness of primary roots in every finite extension forces the cyclotomic character to have infinite image. Its image therefore has a cyclic quotient of order equal to the residue characteristic.

If not all roots of a given order lie in the base field of a finite Galois extension, a primitive root is moved by an actual Galois automorphism.

Compute character restriction through compatible algebraic closures. For a finite Galois extension, characters of modulus coprime to the degree are detected by restriction, and invariant characters admit extensions.

The kernel of restriction from Gal(Ω/K) to Gal(M/K) is Gal(Ω/M), with the same underlying field automorphisms. For finite M/K and Galois Ω/K this is a continuous equivalence. Actual subgroup conjugation becomes semilinea…

The kernel of restriction to a finite normal extension is the fixing subgroup of its actual image in the upper field. If the upper extension is normal and the finite extension is Galois, restriction is surjective and thi…

The actual kernel of normal restriction identifies with the upper field's absolute Galois group. Transport through both actual quotient maps preserves conjugation by the same lift of the relative automorphism.

When the base field contains the relevant roots of unity, simultaneous prescription of multiplicative power classes gives simultaneous prescription of continuous cyclic characters along arbitrary field embeddings. The pr…

An infinite primary subgroup in the units of a field contains primitive roots of every prime-power order. Its power maps are surjective. Consequently, if the only unit divisible by every positive integer is one, every pr…

Primary roots embed through the actual map on units. A finite extension embedded in a chosen overfield is identified with its actual intermediate field range.

A nonidentity automorphism of a prime-degree Galois extension has an eigenunit with primitive eigenvalue when the base field contains the corresponding roots of unity. The unit is produced by the cyclic Kummer radical ge…

A primitive r-th root cannot be an r^s-th power if the field has no primitive r^(s+1)-th root. The quotient here is the ordinary power-class group used by absoluteKummerContinuousNthRootsCharacterEquiv.

Start with a prime-degree Galois extension M/F, and adjoin the p-th roots of unity to M. When the two primes differ, the resulting extension over F is finite Galois with order coprime to p. This uses the tower law and no…

Primitive roots identify additive residue classes with roots of unity. These coordinates respect reduction and the actual cyclotomic Galois action.

Prescribed local characters over inequivalent base valuations lift to a global character over a finite family of prolongations. Equivalent prolongations are grouped together before weak approximation of power classes, an…

The nontrivial automorphism has exactly the base field as its fixed field. An anti-invariant generator gives the two base-field square classes which become squares in the extension.

Let Delta be a subgroup of Kˣ. Inside a fixed separable closure Omega/K, we adjoin all roots beta of the equations beta ^ n = a, for a ∈ Delta. Using all roots makes the construction independent of choices and visibly st…

Source lemmas for the quotient on the radical side of the Kummer pairing in Concrete Kummer radical quotients. Unlike MultiplicativeRadicalDatum, this construction starts with an arbitrary choice of roots. The hypothesis…

Let Delta ≤ Kˣ contain Kˣ^n, and suppose every element of Delta has an n-th root in a finite Galois extension L/K. This file restricts the actual finite Kummer character to Delta / Kˣ^n → Hom(Gal(L/K), μₙ(L)). The exact…

Support API for root-quotient constructions in concrete Kummer extensions.

An automorphism has the same actual power action on a root and on the Kummer coefficient roots. Their cyclotomic actions cancel. The resulting constant-coefficient Kummer character is fixed by the true left action.

The image of a primitive root is primitive. Its bounded exponent is therefore coprime to the order and describes the action on every root at that order.

Collects radical support, local power kernels, restricted characters, and S-unit power quotients used in concrete Kummer extensions.

Linear-algebraic coordinates for kernels of surjections between finite free modules over ZMod (p ^ v).

An actual base-linear equivalence transports a semilinear automorphism and intertwines its conjugation on the two relative Galois groups.

An automorphism of an extension field lying over a base automorphism conjugates the relative Galois group. Two lifts of the same base automorphism differ by an actual relative Galois automorphism, so their conjugations a…

The inverse images of a basis of a finite intermediate field generate a finite intermediate field. Its fixing subgroup maps into the original fixing subgroup under semilinear conjugation. This proves continuity for the K…

Conjugation by the same ambient field automorphism commutes with restriction of scalars. For two field towers, restriction to a normal field supplies the lower automorphism and its actual compatibility with the upper aut…

The actual Krull restriction equivalence transfers separable Kummer characters to the existing absolute Galois group. The exponent need only be nonzero in the base field; no characteristic-zero or perfectness assumption…

The chosen lift restricts to the separable closure and carries each radical root to a root of the transformed unit. If the base automorphism fixes the roots of unity, the actual absolute Kummer character has constant coe…

The chosen automorphism of the algebraic closure restricts to the separable closure. Both directions use that same automorphism and its actual inverse.

The comparison factors through the canonical separable closure and restriction from the algebraic closure. Independence of the chosen semilinear lift proves compatibility with the actual absolute action, including imperf…

For an exponent nonzero in the base field, every unit has a root in the separable closure. The existing Galois Kummer equivalence therefore applies without a perfectness or characteristic-zero hypothesis.

This file exposes the chosen singleton-radical construction used in Kummer theory. For b : Kˣ, it chooses an embedded field K(ⁿ√b) inside the separable closure and proves that, when K contains the n-th roots of unity, th…

This file constructs a field-generic norm witness for the pair formed by a unit and its nonzero complement. The construction uses the finite quotient of the roots of unity by the image of the simple Kummer character, so…

The inclusion of base-field units is equivariant for the trivial action. In a finite cyclic Galois extension, every H² class has a carry representative with invariant coefficient; Galois fixed-value descent makes that co…

This uses the existing periodic H² calculation and base-unit representatives. The norm hypothesis is the actual algebra norm, rather than a separate cohomology model.

The two routes through a finite Galois tower are compared using their actual group restriction and coefficient maps. This comparison is used to turn relative norm primitives into vanishing of restricted inflated H² class…

Relates the cohomology maps on field-unit representations to the corresponding base-unit maps in a finite Galois tower.

The actual restriction homomorphisms and inclusion of units define the inflation and restriction maps without representing the lower field as a subtype of the upper field.

Identifies the invariant and quotient representations associated to an intermediate field and transports the degree-two inflation and restriction maps.

The map is induced by actual restriction to a normal intermediate field and inclusion of its units. For a finite Galois upper field, Hilbert 90 corrects an upper primitive by an actual principal one-coboundary. The corre…

A finite field-unit primitive is first corrected, by the proved Hilbert-90 construction, to a continuous natural mup primitive. The existing primitive-root trivialization then turns it into a lifted ZMod p primitive. Its…

A primitive p-th root in the base field gives an equivariant additive map from the trivial ZMod p coefficient group to the unit representation of a finite extension. This file constructs the resulting morphism of Int-rep…

For a finite Galois extension, changing the coefficients of the ordinary degree-two character cup class by a chosen primitive root is represented by applying the chosen-root homomorphism pointwise to its two-cocycle. Com…

Constructs carry cocycles from the negative Kummer character and compares them with cup-product classes and factor sets inflated from cyclic quotients.

The finite chosen-root homomorphism and the existing absolute mup trivialization use the same supplied primitive root. Their values therefore agree in the algebraic closure. The finite coefficient homomorphism is also na…

The inclusions Kˣ → Lˣ → Nˣ give an actual equivariant coefficient map for Gal(N/L), starting with the trivial action on Kˣ.

Suppose a finite Galois two-cochain with values in mup is the boundary of a unit-valued one-cochain b. Then b^p is a crossed homomorphism. Noether's Hilbert 90 produces its primitive u; a p-th root of u in the algebraic…

A vanishing first cohomology group supplies primitives for the conjugation cocycles of a relative representative. A coset section then turns these primitives into one global cochain.

The descended cocycle takes values in the actual subgroup invariants. Together with relative normalization, this proves exactness in degree two when subgroup H¹ vanishes.

Restriction-zero classes have representatives which vanish pointwise on the subgroup. Their conjugation defect is an actual degree-one cocycle, the input for Hilbert 90 in finite Galois descent.

Conjugation identifies the automorphism groups, while the same field isomorphism identifies their actual unit representations.

When F → E is surjective, restricting an E-automorphism of N to F is a group isomorphism. Its action on Nˣ is unchanged.

Canonical aggregate generated by the reviewed rehome.

A surjection with kernel of prime order can split only if its kernel is not contained in the Frattini subgroup. Applied to the cocycle extension of a nonzero degree-two class, this identifies the coefficient kernel as a…

For a closed normal subgroup contained in the power--commutator subgroup of a pro-p group, relative Nakayama constructs a new detecting invariant character whenever the chosen relators do not normally generate. Their tri…

A finite independent family of ambient-invariant characters of a closed normal subgroup contained in the power--commutator subgroup gives independent classes in the quotient's H². No presentation or finite normal generat…

This file identifies continuous additive ZMod p-characters with Mathlib's degree-one continuous cohomology for the trivial coefficient representation. It supplies both the small-universe coefficient API and the universe-…

For continuous additive ZMod p-characters, the canonical homogeneous representatives give the degree-two cochain (g, h, k) ↦ χ(g⁻¹h) ψ(h⁻¹k). This file constructs that cochain directly and proves its cocycle equation. No…

Two continuous mod-p characters of a pro-p group factor through one common finite p-group quotient. Restriction naturality then identifies their canonical cup with inflation of the cup of the descended characters.

This file packages the explicit canonical character cup cocycle as a degree-two continuous cohomology class and as a bilinear map.

The canonical character representatives commute with pullback along a continuous group homomorphism. Consequently their degree-two cup cocycle and cohomology class commute with continuous-cohomology restriction.

For an open normal subgroup U, continuous mod-p characters of G / U inflate to continuous characters of G. Their range is exactly the kernel of restriction to U.

The three kernel--range identities for inflation, restriction, and transgression assemble into the continuous low-degree five-term sequence with trivial ZMod p coefficients.

The algebraic factor-set construction in FiniteTransgression uses a bottom topology on its finite quotient. Here the same construction is made directly for the canonical quotient topology of an open normal subgroup, so t…

For an open normal subgroup, restriction of an ambient continuous mod-p character lands in the conjugation-invariant continuous characters. Its range is exactly the kernel of the continuous factor-set transgression.

This file extracts the normalized degree-one primitive of an inflated degree-two cocycle and uses its restriction to the open normal subgroup to reconstruct the invariant continuous character occurring in transgression.

For a discrete group in the base universe, continuous homogeneous cochains with lifted trivial mod-p coefficients are additively equivalent to the usual inhomogeneous function cochains. This file records the equivalences…

For a discrete group in the base universe, the explicit homogeneous and inhomogeneous comparison induces an additive equivalence in degree two. The ordinary coefficient object is exactly the trivial Int-representation on…

The existing comparison is evaluated on every lifted homogeneous two-cocycle. The representative is its actual dehomogenization, with no cup-product or normalization restriction and no extra comparison assumption.

The explicit homogeneous/inhomogeneous cochain equivalences commute with the two differentials surrounding degree two. We package them as an isomorphism of short complexes after forgetting topology and restricting scalar…

Bézout inversion of the index power normalizes transfer. This works for every finite abelian coefficient group, including universe-lifted coefficient groups, and preserves continuity. No choice of cyclic coordinates is n…

For a specified generator g, let S(x) be the prefix 1 + g + ... + g^(r(x)-1), where r(x) is the standard representative of the generator coordinate of x. The degree-two bar differential applied to these prefixes is the c…

The generator prefixes and carry identity define the first four components of a map from the bar resolution to the cyclic periodic resolution. This file verifies the chain squares through degree three and extends those c…

This module identifies the normalized finite-cyclic carry cocycle in bar cohomology with the canonical even-degree class from the periodic resolution.

A specified generator of a finite cyclic group identifies the group with ZMod (Nat.card G). Taking the standard natural-number representative of that coordinate records multiplication by addition with a possible carry. T…

A coefficient morphism sends the carry cocycle of a fixed element to the carry cocycle of its image. If that image is the norm of an actual element in the target representation, the resulting degree-two cohomology class…

Every even cyclic cohomology class has a generator-fixed representative. If the coefficient image of every such representative has an actual norm preimage, the entire induced degree-two map vanishes.

For a chosen generator of a finite cyclic group, Mathlib computes positive even group cohomology and degree-zero Tate cohomology by the same periodic short complex. This file records the resulting comparison in degree tw…

For a finite nontrivial pro-p group, finite cochains supply finite-dimensional H² and the constructed finite minimal presentation identifies its relation rank with that dimension. Thus no presentation or finite-presentat…

The algebraic transfer is continuous: its transversal formula is a finite product, and representatives are continuous functions of the discrete coset space. Normality of the subgroup and discreteness of the target are no…

A finitely generated pro-p group with finite-dimensional H² has an actual finite minimal presentation. The free source is constructed by completion, its epimorphism is minimal by equality of generator ranks, and the clos…

For a closed normal subgroup R and an ambient finite quotient F/U, this file constructs the canonical map from F/R to (F/U)/(image R) and uses it to inflate the finite factor-set class.

At an open finite quotient stage, every abstract mod-p character is continuous. This file therefore upgrades finite transgression exactness to the continuous degree-one characters of the ambient finite quotient: their re…

A primitive for a vanishing inflated class is corrected by finite-stage quotient-section residues. The resulting coboundary datum gives a continuous ambient character extending the original invariant kernel character.

Defines finite-stage inflation as a linear map, composes it with the explicit finite transgression map, and transports the no-extendable-combination independence criterion across injective degree-two inflation.

If an inflated finite-stage transgression class vanishes, its explicit homogeneous cocycle is a boundary. This file extracts a degree-one primitive and records its normalized coboundary identity. The residue correction a…

At a finite quotient stage, invariant characters modulo restrictions of continuous degree-one characters identify with the range of finite transgression.

An ambient-conjugation-invariant ZMod p character on a normal subgroup determines the usual factor-set homogeneous two-cocycle on the discrete quotient, and hence a continuous degree-two cohomology class with universe-li…

Restriction of an ambient mod-p character to a normal subgroup is conjugation invariant. This file proves the missing converse to the finite transgression kernel theorem: an invariant character has zero factor-set class…

If the explicit factor-set class of an invariant character vanishes, an elementwise boundary calculation constructs an extension of that character to the ambient group. This is the kernel half of the low-degree transgres…

Packages ambient-conjugation-invariant finite characters as a ZMod p-module and proves that the explicit finite transgression construction is linear. The kernel extension theorem then gives a criterion for linear indepen…

The exact kernel calculation for finite transgression identifies invariant characters modulo ambient restrictions with the range of finite transgression.

This file proves that continuous degree-two cohomology with universe-lifted trivial ZMod p coefficients vanishes for the finite-basis free pro-p source used by a presentation. The proof is explicit: a homogeneous cocycle…

This helper leaf converts homogeneous degree-two cocycles with lifted trivial ZMod p coefficients into normalized inhomogeneous cocycles and constructs the homogeneous degree-one primitive associated to a continuous cobo…

A one-cocycle that vanishes on a normal subgroup takes values in the subgroup invariants and descends to the quotient. Subtracting a boundary on the normal subgroup gives the degree-one vanishing induction step for arbit…

This file chooses a homogeneous cocycle representative of a lifted continuous degree-two class and attaches its explicit central extension. A continuous group-theoretic section of the extension forces the represented coh…

A normalized continuous ZMod p-valued two-cocycle on a topological group Q defines a twisted central extension of Q. This file packages that construction, including its product topology, quotient projection, coefficient…

A continuous character which is the identity on the explicit coefficient kernel constructs a continuous section by correcting the zero-coordinate lift. The prime-to-index restriction leaf supplies this character from the…

Two continuous lifts of the same group map differ by a continuous coefficient character. The cocycle terms cancel because their base coordinates agree. The construction takes values in ZMod p itself, so it can be restric…

These formulas use the actual coefficient coordinates of the existing lifts. In particular, agreement of a correction character with the lift difference on a subgroup is exactly the condition for the corrected lift to ki…

The chosen degree-two representatives are linear. Their normalized cocycles therefore respect addition and scalar multiplication. These identities construct actual sums and scalar multiples of lifts, while subtracting a…

Restriction of a homogeneous degree-two cocycle is evaluated explicitly on the standard continuous resolution. The resulting pullback cocycle extension maps to the original extension, so vanishing of the restricted class…

A homogeneous degree-one boundary is converted to a normalized continuous inhomogeneous primitive. That primitive gives an explicit continuous group section of the associated degree-two cocycle extension. In particular,…

A nonzero lifted continuous degree-two class of a pro-p group descends to a nonzero class on one finite p-group quotient. Its explicit cocycle extension is therefore a finite central p-extension with no continuous group-…

Every lifted degree-two class of a pro-p group is inflated from a finite p-group quotient.

Finite families of lifted degree-two classes of a pro-p group inflate from one common finite p-group quotient. In particular, the ranges of finite-stage inflation cover the ambient degree-two cohomology.

If every finite-stage inflation range embeds in one fixed finite-dimensional target, then finite families of ambient classes descending to a common stage force the whole ambient degree-two cohomology to have the same dim…

A uniform bound p^d on finite-stage inflation images gives finite continuous H² of dimension at most d. Finiteness of the finite-stage cohomology and its image is constructed, rather than assumed.

Vanishing on an open finite-index subgroup supplies a continuous lift to the cocycle extension. The difference between this lift and the inclusion gives a coefficient character on the preimage subgroup. Its continuous tr…

For an open normal subgroup, continuous transgression has range exactly the kernel of degree-two inflation. The reverse inclusion is proved at cochain level by restricting a continuous primitive of the inflated cocycle.

The inflation--transgression kernel calculation identifies finite-stage degree-two cohomology modulo continuous transgression with the corresponding range in ambient degree-two cohomology.

For an open normal subgroup, every continuous transgression class lies in the kernel of degree-two inflation. The proof uses an explicit continuous homogeneous primitive after inflation.

This file packages the conjugation-invariant continuous ZMod p characters of the kernel of a finite pro-p presentation as a ZMod p-submodule. Evaluation on the displayed relators is injective, so this invariant character…

Constructs the two coordinate maps for a product of multiplicative representations and proves their combined degree-two evaluation is injective.

The concrete equivariant-function module used by the local idele block decomposition has exactly Mathlib's coinduced action after applying Additive. This file supplies the representation isomorphism and hence Shapiro in…

Primitives are selected coordinatewise and assembled into an actual one-cochain. The local vanishing input is supplied by the proved local integer-unit and archimedean block theorems at the idele application.

An actual one-cochain primitive in each coordinate combines into a product primitive. Consequently evaluation detects degree-two classes, including for an infinite product of multiplicative coefficient groups.

The normalized free-source primitive restricts to a continuous conjugation-invariant character of the presentation kernel. The construction is linear in the degree-two cohomology class.

For a minimal pro-p presentation realizing the least relation count, normalized invariant kernel characters descend to a common finite stage. Their inflated transgression classes are linearly independent: a vanishing com…

This file linearly selects homogeneous cocycle representatives and, after restriction to the finite-basis free pro-p source, linearly selects degree-one primitives. It also records the pointwise boundary and normalizatio…

If the extracted kernel character vanishes, the normalized free-source primitive descends along the presentation quotient. Its homogeneous lift is a target primitive, proving injectivity into the invariant kernel charact…

Continuous group equivalences induce linear equivalences on continuous cohomology. A finite pro-p presentation supplies the required topological first-isomorphism equivalence between the quotient of its free source by th…

Transfer followed by multiplication by the inverse index extends a conjugation-invariant character on an open normal subgroup. The modulus need not be prime.

Defines the continuous quotient projection and subgroup inclusion and identifies their composite cochain and cohomology maps with the constant-one map.

For a finite minimal pro-p presentation realizing the least relation count, relative Nakayama characters separate each displayed relator from the closed normal closure of the others. After normalization, their invariant…

The upper and lower presentation bounds identify the least relation count of a finitely minimally presented pro-p group with the dimension of its continuous degree-two cohomology with trivial ZMod p coefficients.

A changed continuous cyclic p-power character factors through the actual maximal pro-p residual quotient. Its change therefore detects conjugation on the topological abelianization of that quotient.

For a group in the base universe, the universe-lifted trivial ZMod p coefficient and the benchmark's small coefficient are isomorphic. Functoriality of homogeneous cochains transports this coefficient isomorphism to ever…

A normal subgroup acts trivially on its coset space. Each factor of the transfer of an element of the subgroup is therefore a conjugate of that element. Conjugation invariance of the character makes the product its value…

Pullback along the constant-one homomorphism vanishes on cocycles and continuous cohomology with trivial ZMod p coefficients. Consequently, inflation followed by restriction to the kernel vanishes in degree one. The same…

This is the coefficient object used by the relation-rank benchmark, together with its canonical restriction maps on homogeneous cochains, cocycles, and continuous cohomology.

Canonical aggregate generated by the reviewed rehome.

The cyclotomic torsion calculation uses the decomposition Gal(ℚcyc/ℚ) ≃ ℤ̂ × f, where the torsion subgroup is dense in the second factor. This file proves the topological-group calculation which turns that decomposition…

Euler's theorem gives compatible finite powers of (p + 1) ^ (p - 1). Their inverse limit is a continuous character of the additive p-adic integers, with infinite image and trivial reduction modulo p.

If every finite reduction had order prime to p, each reduction would have exponent dividing p - 1. Separation by reductions would then place the entire image in the finite group of (p - 1)-st roots of unity.

This file supplies the source-producing facts about ℤ̂ used to normalize the surjection in the opening datum of abstract valuation theory. In particular, multiplication by a positive integer identifies ℤ̂ with the closed…

We construct ℤ̂ as the topological closure of the diagonal image of ℤ inside the product of all positive cyclic quotients ZMod n. This realizes the canonical reduction maps and the dense integer embedding directly in Mat…

This file constructs the canonical map ℤ̂ → ∏ p : Nat.Primes, ℤp from the compatible finite reductions.

This file upgrades the prime-product Chinese-remainder equivalence for ℤ̂ to topological additive, multiplicative, and unit-group equivalences.

This file contains the small amount of topological-generation theory used in the construction of Frobenius fixed fields, next to its sole application.

The inner discrepancy in the choice of algebraic-closure embeddings disappears in every commutative quotient, including the quotient modulo q-th powers.

A closure embedding intertwining two Galois automorphisms identifies their values under every continuous character with commutative target. Its difference from mathlib's chosen lift is removed by an inner automorphism.

The chosen algebraic-closure embeddings behind absoluteGaloisGroup.map need not compose. Their discrepancy is an inner automorphism, so restriction of a continuous homomorphism with commutative target does compose exactl…

A single algebraic element is fixed by an open subgroup. Its orbit map, and the induced orbit map on units, are locally constant in the Krull topology.

Canonical aggregate generated by the reviewed rehome.

The cocycle projection is surjective as a function, and its kernel consists of boundaries. These are statements about the actual topological homology objects, with no exactness assumptions on a coefficient sequence.

An arbitrary finite-valued lift has a defect in the prime-order kernel. Trivial action on that kernel makes the defect an ordinary two-cocycle; a primitive supplied by H² vanishing corrects the lift.

Scalar restriction is continuous and identifies the upper Galois group with the open subgroup fixing the embedded finite extension field.

Finite discrete-valued continuous functions on a pair of Galois groups factor through one actual finite Galois intermediate field.

The algebraic-closure embedding used for absolute Galois restriction preserves the separable closure. Its restriction intertwines the actual Galois maps.

This file proves that a closed normal quotient of a compact Hausdorff totally disconnected topological group is totally disconnected.