Totally real number-field towers and their unramified pro-p Galois groups. Includes Frobenius constraints, finite-support comparisons and relation-rank bounds.
Multiplication by the actual character of negative three switches the real value and leaves inertia at every finite place other than three unchanged. This constructs a character with any specified real value, starting wi…
The real local Artin value of negative one is complex conjugation whenever an infinite place ramifies. If a discrete absolute representation kills these actual elements over a totally real base, its finite Galois kernel…
A discrete p-group representation killing finite inertia outside the chosen support and the real Artin value of negative one has an actual finite Galois kernel field satisfying the defining local conditions. Its inclusio…
The actual ambient inclusion supplies a continuous surjective restriction homomorphism. Its kernel is exactly the subgroup fixing the constructed compositum. The quotient by this kernel is continuously isomorphic to the…
Absolute inertia outside the allowed support fixes every admissible finite layer, hence their compositum. Real Artin conjugation fixes that compositum because every complex embedding of it is real.
Totally real number-field towers and their unramified pro-p Galois groups. Includes Frobenius constraints, finite-support comparisons and relation-rank bounds.
A vanishing finite field-unit class gives an actual field-unit primitive. The existing Hilbert-90 correction then gives a continuous lift of the normalized central extension over the absolute Galois group. Thus its infla…
The finite coefficient map is composed with the established discrete continuous-to-ordinary H² comparison. Normalization changes a representative by the boundary of a constant one-cochain. The representative-level Hilber…
Restrict the chosen absolute valuation to the actual finite Galois layer. An absolute decomposition automorphism preserves this restricted valuation class. Complete splitting makes its decomposition group trivial, indepe…
The existing local residue comparison identifies the quotient by inertia with the profinite integers. The class of arithmetic Frobenius is the inverse image of additive one, and a representative is chosen in the actual a…
We select actual finite Galois intermediate fields of the fixed algebraic closure of ℚ. The base field is a member and binary composita remain in the family. These constructors provide the directed family used to form th…
Compact intermediate fields contained in the supremum of admissible finite layers lie in one layer, since the family is nonempty and directed. This applies both to finite-dimensional intermediate fields and to the field…
The concrete finite Galois compositum equals the field generated by its five square roots. Independence of their rational square classes gives its degree by the general finite-adjoin induction.
The radicands 5, 13, 17, 21, 33 have no nonempty square subproduct. There are exactly thirty-one nonempty subsets. The natural-number check uses the square-root decision procedure inside the Lean kernel; the rational sta…
The fixed field of an intersection of closed subgroups is the compositum of their fixed fields. The comparison uses the infinite Galois correspondence.
Depths n + 5 leave a strict negative Golod--Shafarevich margin at t = 5/12. This numerical file does not assert that the required Frobenius elements or their deep lifts have already been constructed.
Restriction embeds the automorphism group of a compositum of normal subextensions into the product of their automorphism groups. Consequently, p-group automorphism groups are preserved by composita. This applies in parti…
Complex conjugation in the algebraic closure restricts to the chosen negative-one Artin value in every finite abelian subextension. These finite projections identify its maximal-abelian restriction with the actual idele…
Forgetting the splitting conditions in Sawin's theorem gives totally real number fields of unbounded degree with uniformly bounded root discriminant.
Every finite normal subextension of the constructed compositum is contained in an admissible finite layer. Restriction therefore makes its Galois group a quotient of a p-group. Applying this to fixed fields of open norma…
The field is formed from the concrete directed family of finite layers. Galoisness and total reality follow from the corresponding properties of those layers. The pro-p property and arithmetic rank estimates are separate…
A finite family of independent square classes gives an actual extension of degree two to the power of the family size. Degree and square-class classification are proved simultaneously: classification in the previous laye…
Restriction to the actual field generated by a square root of negative three gives a continuous character of the absolute Galois group of the rationals. Its discriminant proves that it kills finite inertia away from thre…
Global reciprocity applied to the principal idele of negative one identifies its local value at three with its nontrivial real sign. All other finite components disappear by the proved unramifiedness of the actual quadra…
The finite-quotient definition of the profinite Frattini subgroup is equivalent to intersection over open normal subgroups of index two. For the reverse inclusion, each maximal subgroup of a finite two-group quotient pul…
A positive squarefree integer congruent to one modulo four determines an actual quadratic field in the fixed algebraic closure. Its Galois group has order two, its embeddings are real, and its discriminant is the given i…
A generator of a quadratic extension of ℚ supplies the actual basis 1, α. Reindexing its power basis by Fin 2 gives named basis vectors and the rational coordinates of every element. No square relation is needed for this…
The actual rational basis 1, α, where α² = d, has diagonal trace matrix with entries 2 and 2d. Its discriminant is therefore 4d. No integrality or squarefreeness assumption is needed.
A chosen square root of a nonsquare rational number generates an actual finite Galois intermediate field of degree two. Its internal generator, square relation, and generation theorem let later arithmetic constructions s…
A root of the same quadratic equation generates the same subfield of the fixed algebraic closure. This identifies arbitrary quadratic layers with the concrete constructors and makes squarefree radicands unique.
An intermediate field containing square roots of finitely many radicands also contains a square root of their product, up to a square in the base field. The proof constructs that root as an actual product and compares th…
The constructed bases of the full ring of integers determine the number field discriminant. Integer traces agree with rational traces after scalar extension, so the two-by-two trace determinants give 4d or d according to…
The nontrivial square root of unity in ℚ makes every quadratic extension a Kummer extension. The resulting generator has irreducible polynomial X ^ 2 - C d, which forces its rational square d to be nonzero and nonsquare.…
The square-root generator is integral. When its square is one modulo four, its half-integer translate is integral as well. Integer-coordinate classification gives spanning, and the concrete rational quadratic basis gives…
The trace and norm conditions and their parity criterion give integer coordinates for every algebraic integer. Away from d = 1 modulo four the generators are 1, α. Every algebraic integer also has integer coordinates in…
The trace and norm of an algebraic integer are integral. For a square-root generator of signed squarefree square d, these identities force both coordinates to be half-integers and give the congruence modulo four. Convers…
A square root of an integer is integral. More generally, the element (m + n α) / 2, where α ^ 2 = d, is integral whenever 4 ∣ m ^ 2 - d n ^ 2. The divisibility witness supplies the integer constant coefficient of the mon…
For a signed squarefree integer d, the norm numerator a² - d b² is divisible by four precisely for even coordinates, or for odd coordinates when d is one modulo four.
A square root of a nonnegative rational number has real image under every complex embedding. If it generates the extension, conjugation fixes the whole image. Conversely, a rational number that is a square in a totally r…
Two signed squarefree integers in the same rational square class agree. Taking traces in a quadratic field shows that any two square-root generators have squares in the same rational square class. Thus the normalized rad…
In a quadratic extension generated by a square root of a, an element of the base field becomes a square precisely when its square class is trivial or that of a. The basis 1, α makes the cross coefficient of a square expl…
Rescaling a rational Kummer generator by a nonzero rational number preserves the generated field and replaces its square by a signed squarefree integer.
A totally real quadratic number field has a positive squarefree integer radicand. If its allowed finite ramification support excludes two, the discriminant formula forces the radicand to be one modulo four. The discrimin…
A square-root generator of a quadratic extension has minimal polynomial X² - d. Its trace and norm, and those of every rational linear combination of 1 and the generator, follow from the power basis and a two-dimensional…
The initial arithmetic group in the Sawin construction permits ramification at specified finite places. This predicate retains the existing local unramifiedness condition outside that set. Its tower lemmas work also for…
Inertia at a prime outside the permitted support is trivial on each factor. The restrictions to the factors jointly detect automorphisms of their compositum. This argument does not require an odd extension degree.
An algebra equivalence preserves the permitted finite places on the base.
Class number one makes the actual unit-to-radical map surjective. The integral units of the rationals are ±1, so these two representatives exhaust the ideal-square radical. This identifies its unique possible obstruction…
The canonical identification of the integers of ℚ with ℤ identifies their local unramifiedness conditions. Under the equivalence between finite places of ℚ and positive rational primes, the allowed ramification support t…
Apply the natural-number squarefree decomposition to the product of the absolute numerator and denominator. The numerator's sign then gives an integer representative without introducing a square root in an extension.
Local unramified degree-two vanishing constructs the reference lifts. The actual absolute lift has finite ramification support; its differences from these reference lifts are genuine local characters. Prime three absorbs…
The finite-support radical kernel constructs an absolute quadratic character with the prescribed inertia values. Multiplication by the character of negative three then gives any specified real value while preserving iner…
The rational ideal-square radical is generated by the actual class of −1. The local restriction of the character of ℚ(√−3) has nonzero reciprocity pairing with that class. Subtracting its uniquely determined scalar multi…
The initial Sawin tower has base field ℚ. Over this base, being unramified at infinite places is exactly total reality. Total reality is preserved by composita inside an algebraic extension, so this supplies the real-pla…
An actual quotient of a finitely generated profinite group admits finite arithmetic stages such that every element trivial on that stage has a lift of any prescribed augmentation depth in the source.
Outside the allowed support inertia acts trivially. Consequently the actual decomposition map factors through its residue-degree quotient; killing arithmetic Frobenius kills its entire decomposition image.
The closed normal subgroup generated by the chosen arithmetic Frobenii has a Hausdorff group quotient. At primes outside the allowed ramification support, its projection kills the whole absolute decomposition group.
Take the fixed field of the constructed closed normal subgroup inside the maximal real extension, then lift it into the same algebraic closure of ℚ. Its Galois group is the actual quotient from S3.
The actual quotient kills the absolute decomposition groups at selected unramified primes. Thus those groups fix the cut field elementwise. The proved restriction-image theorem for decomposition groups then gives complet…
The actual arithmetic Frobenius is represented by an absolute decomposition element. Complete splitting makes its finite-stage restriction trivial, so the constructed depth-detecting stage supplies a deep source lift.
An open normal subgroup determines an actual finite Galois fixed field. Lifting it to the chosen algebraic closure gives an admissible finite layer. The quotient is identified with that layer's Galois group. No rank esti…
The global ramification certificates on an admissible finite layer imply the actual chosen-completion conditions used by finite H² localization.
The actual finite quotient is continuously identified with the Galois group of its lifted fixed field. Its restriction map agrees with restriction from the fixed algebraic closure, by the actions of both maps on every fi…
The actual finite stage detecting source depth has completely split rational primes congruent to one modulo four outside any finite set. Excluding also the six allowed ramified primes gives an actual new unramified Frobe…
The group-theoretic intersection over quadratic quotients and the arithmetic classification of all quadratic layers identify the actual Frattini fixed field. No finite-generation hypothesis is used.
The proved Frattini fixed-field comparison identifies the canonical power--commutator quotient with the Galois group of the five quadratic layers. Its cardinality is therefore thirty-two. No finite-generation, quotient-f…
The finite-rank free source is an actual completion of an abstract free group. Its epimorphism to the arithmetic group has kernel in the Frattini subgroup.
Choose genuine primes and source lifts at depths n + 5 in the actual minimal presentation from S1. The prescribed finite-prefix budget allows all these Frobenius relations to be imposed while the quotient stays infinite.
The computed power--commutator quotient has order 32. Its vector-space basis lifts to a finite generating set of the actual Galois group by the pro-p Burnside criterion. The quotient dimension also proves minimality.
An actual absolute cocycle lift is corrected at its finite ramification support and at real conjugation. Its kernel field is an admissible finite real two-extension, so the corrected lift factors through the constructed…
At every actual finite arithmetic stage the field-unit Kummer image has at most 64 elements. Its kernel is killed by inflation to the constructed maximal group. Discrete comparison and the finite-stage Galois equivalence…
The arithmetic H² bound and the constructed five-generator quotient supply a finite minimal presentation. Its relation rank is at most six, so the Golod--Shafarevich criterion proves that the actual Galois group is infin…
Choose a presentation attaining the least relation count constructed in S1. Minimality identifies its displayed generator count with the actual rank five. The same presentation, including its free source and relators, is…
Finite Galois layers inside the maximal real extension correspond to open normal subgroups. Restricting and then lifting recovers the original ambient field. The index-degree equality identifies its quadratic layers, who…
The degree of every finite admissible layer is a power of two. Its ramified rational primes belong to {3,5,7,11,13,17}, whose product is 255255. The prime-to-degree different bound gives the same root scale 255255 for ev…
A single infinite set of rational primes congruent to one modulo four splits completely in totally real number fields of unbounded degree and uniformly bounded root discriminant. The statement matches the arithmetic inpu…
The finite set of allowed places is the actual six-prime support, with cardinality six. It provides the coordinate set used by H² localization.
The ramification and discriminant classification supplies a positive squarefree radicand for every quadratic layer. Its explicit square-class factorization then places that layer inside the compositum of the five chosen…
The radicands 5, 13, 17, 21, 33 give actual finite Galois fields inside the chosen algebraic closure of ℚ. Each satisfies the prescribed finite ramification and real-place conditions. Their finite supremum is therefore a…
Restriction to the two factors of a compositum is jointly injective. An exponent bound on both Galois groups therefore holds on their compositum. Each of the five chosen quadratic fields has Galois group of order two, so…
A squarefree integer supported on 3, 5, 7, 11, 13, 17 divides their product. The primes 5, 13, 17 are one modulo four, while an even subset of 3, 7, 11 contributes 1, 21, 33, or 77. The last contribution is 21 33 / 3². T…
The finite place support is the inverse image of the six primes under the canonical equivalence between finite places of ℚ and rational primes.
Over any base field, a square root of a nonsquare has minimal polynomial X² - a and generates an extension of degree two. No assumption on the characteristic or on the ambient extension is required.
If a signed squarefree integer times the square of a rational number is integral, the denominator squared divides the squarefree integer. Coprimality of the rational numerator and denominator then forces the denominator…
This aggregate exposes the global, local, Kummer, radical, and relation-rank modules for unramified pro-p extensions.
This aggregate collects global reciprocity characters, idele cohomology, class groups, unramified composita, and maximal everywhere-unramified pro-p extensions.
This file proves that the compositum of two finite Galois number-field extensions unramified at finite places is again unramified at finite places. An odd-degree hypothesis on the compositum then supplies the infinite-pl…
The cyclic class-field axiom already supplies H¹ = 0 through cyclic Tate periodicity. This file propagates that source result to every finite p-extension by induction on its quotient order. The induction works with cocyc…
This file combines the finite-prime bridges for rings of integers with the infinite-place API. It also transports everywhere-unramifiedness across an equivalence of top fields and supplies odd-degree Galois constructors.
This file bundles the finite Galois everywhere-unramified p-extensions inside the chosen algebraic closure. For odd p, the bundle is closed under binary composita.
For an odd prime p, every finite family of bundled finite Galois everywhere-unramified p-extensions has a bundled compositum. Its underlying field is the finite supremum of the fields in the family.
The actual field-unit embedding factors through the principal-idele representation isomorphism. Its degree-two map is therefore injective in a finite Galois p-extension. An explicit idele primitive of a field-unit cocycl…
The actual principal ideles, relative ideles, and relative idele classes form a short exact sequence of Galois representations. Its long exact sequence is the source of the global degree-two diagonal injection.
This file identifies the power--commutator quotient of the maximal everywhere- unramified pro-p Galois group with the elementary Hilbert class-field layer. For odd p, it then identifies the topological generator rank wit…
An absolute character factors through the actual maximal abelian subextension. Pulling that character back by global Artin gives a principal-trivial idele character. This direction is used to compare choices of global ce…
This file cuts out the exponent-p layer of the small Hilbert class field and identifies its Galois group with the ordinary class group modulo pth powers. It also realizes that layer in the canonical algebraic closure and…
This file places the realized elementary Hilbert class-field layer inside the maximal everywhere-unramified pro-p extension. It identifies the resulting intermediate field with the abstract Hilbert layer and transports i…
A continuous finite-valued idele character trivial on principal ideles descends first to the idele class group and then to its component quotient. Actual global reciprocity identifies that quotient with the maximal abeli…
The rational idele-class formation satisfies the cyclic class-field axiom. The abstract p-group induction therefore gives degree-one vanishing. Here we transport that source theorem to the actual relative idele-class rep…
The existing infinite-Galois inverse-limit equivalence detects equality of maximal-abelian automorphisms on finite Galois intermediate fields. On the Artin side, projection at a finite one-place idele is the actual chose…
Inside a fixed algebraic closure of a number field, this file forms the compositum of all finite Galois everywhere-unramified intermediate fields whose automorphism group is a p-group. The results here are the lattice un…
For odd p, the bundled finite extensions are directed under binary compositum. Compactness therefore upgrades finite support in the maximal compositum to containment in one bundled extension.
The power--commutator quotient of the maximal everywhere-unramified pro-p Galois group is the finite Galois group of the elementary Hilbert layer. A finite set of lifts of that quotient topologically generates the full g…
Finite-dimensional intermediate fields are compact in the lattice of intermediate fields. Consequently, an inclusion into the maximal compositum already factors through a supremum of finitely many bundled finite extensio…
The maximal compositum is Galois because each proof-indexed candidate layer is either a finite Galois field or bottom, and arbitrary composita preserve separability and normality. The resulting automorphism group carries…
For odd p, every open normal quotient of the Galois group of the maximal compositum is a finite p-group. The corresponding fixed field is finite Galois, hence lies in one bundled finite p-extension by cofinality; restric…
This file defines the ordinary ideal class group modulo pth powers and its canonical dimension over ZMod p when p is prime.
The dense copy of the infinite cyclic group in ZHat has the expected universal property. A map to a finite discrete group factors through the cyclic quotient determined by the order of the image of 1; the finite-quotient…
The rank-one free-profinite property of ZHat splits the compact profinite central extension attached to every continuous homogeneous two-cocycle. The section supplies an explicit degree-one primitive, so continuous degre…
If the images of A and B generate M over K, restriction embeds Gal(M/B) into Gal(A/K). Inertia restricts into the inertia of A/K. Consequently unramifiedness of A/K gives unramifiedness of M/B; B/K need not be unramified…
This file packages the library predicates for finite and infinite unramifiedness in the exact explicit form used by the Shafarevich benchmark. It also connects finite-place unramifiedness to formal unramifiedness and to…
The stabilizer of an unramified infinite place has order one. Its higher cohomology therefore vanishes, and the proved Shapiro and tensor-block comparisons transfer this to the actual archimedean idele factor. No cyclici…
Continuity gives an open normal kernel. Its actual fixed field is finite Galois, and its Galois group embeds in the target through the quotient by that kernel. In particular a p-group target produces a p-extension; the t…
For a prime p, the absolute Kummer equivalence is linear after giving both power classes and continuous mod-p characters their canonical exponent-p ZMod p-module structures.
Over a field containing a primitive p-th root of unity, the natural mup representation is trivial. This file transports its continuous cohomology through that trivialization and proves that the natural coefficient Kummer…
This file descends the continuous absolute Kummer class with its natural Galois action from field units to p-power classes.
The general field-theoretic implementation is maintained in GaloisCohomology.
The general field-theoretic implementation is maintained in GaloisCohomology.
This aggregate collects absolute and finite Kummer comparisons, local Artin and Hilbert pairings, localization at finite places, and cyclic degree-two norm quotients.
For a finite cyclic extension whose base contains a primitive p-th root, the primitive-root coefficient morphism sends ordinary mod-p degree-two cohomology to unit cohomology. Finite-cyclic periodicity then places the re…
For an actual finite intermediate field, the canonical algebraic-closure equivalence is exactly the choice used by the existing absolute Galois inclusion. This evaluation identity lets finite base changes use the same cl…
The general field-theoretic implementation is maintained in GaloisCohomology.
Generator-fixed coefficients in a representation define positive cyclic carry cocycles after restriction along a group homomorphism. Mapping coefficients commutes with inflation and the degree-two cohomology map; the uni…
This file composes the Kummer factor-set calculation with degree-two naturality. Thus the coefficient-changed cup class on an arbitrary common finite Galois stage is the image of the normalized carry class on its cyclic…
For the chosen simple Kummer extension, the finite-cyclic carry class with a base-field unit coefficient evaluates through the norm quotient to the local Hilbert symbol of that unit.
The general field-theoretic implementation is maintained in GaloisCohomology.
For the normalized generator of a nontrivial simple Kummer extension, the Galois generator coordinate is the negative of the chosen-root coordinate of the Kummer character. The final section records the corresponding sim…
Degree-two cohomology of the Kummer coefficient module is annihilated by its exponent. Its localized image embeds in the product of the actual local torsion groups. The proved kernel containment then gives a surjection f…
Roots of unity are integral at every finite place. The empty-support coefficient map therefore factors through each prescribed finite support, without changing the principal idele in the full idele representation.
Continuous mod-p characters of the absolute Galois group restrict to the absolute decomposition subgroup at every finite place. This file linearizes each restriction and assembles all of them into a dependent product.
Absolute continuous mod-p characters first restrict to a finite-place decomposition subgroup and then to its inertia subgroup. The resulting maps are assembled over all finite places, and their kernels recover the local…
The natural mup representation of the absolute Galois group restricts to each chosen finite-place decomposition subgroup. This file packages the induced map on continuous H¹ and composes it with the linear Kummer map fro…
The natural mup representation on a chosen finite-place decomposition group restricts further to absolute inertia. This file packages the induced map on continuous H¹, its unramified kernel, and the family of inertia res…
A torsion field unit has valuation one at every finite place. Its principal relative idele therefore lies in the actual empty-support subgroup. This gives the supported coefficient map needed to apply the unramified loca…
The general field-theoretic implementation is maintained in GaloisCohomology.
The maximal local Kummer extension and the local Artin map give the local Hilbert pairing on power classes. This file transports that pairing across the absolute Kummer equivalence to continuous additive ZMod p character…
The standard algebraic-closure Kummer character is transported to the local separable-closure model. Its kernel is the stabilizer of the chosen simple Kummer root, without imposing a residue-characteristic restriction.
The finite abelian field is constructed from the character's actual open kernel. Its finite character recovers absolute Artin evaluation, and inertia-triviality puts inertia in the field's fixing subgroup.
Evaluate a continuous mod-p Galois character on the absolute local Artin map. The resulting functional descends to actual multiplicative power classes. Dense image of the Artin map makes the pairing faithful in the chara…
The actual unit/uniformizer decomposition shows that an Artin character trivial on all integer units has a valuation-line power-class functional. The roots-of-unity-free reciprocity range theorem and pairing injectivity…
The roots-of-unity-free reciprocity pairing sends the intrinsic unramified character space onto the valuation line in the dual of actual power classes. The proof evaluates finite Artin reciprocity in the character's own…
The actual Artin--Kummer pairing, restricted to unramified classes in its first argument, vanishes on precisely the valuation-zero Kummer classes. This is the local kernel statement needed to assemble the empty-support u…
The intrinsic inertia-trivial subspace of local continuous H¹ is sent by the Artin--Kummer pairing precisely onto the valuation line in the dual. The proof uses actual unramified Kummer extensions and their Frobenius act…
For a chosen simple Kummer extension which is unramified, its Hilbert character is a Frobenius scalar times normalized valuation. The argument uses the full unramified local Artin formula and therefore also applies at pl…
Unramified Hilbert characters are scalar multiples of reduced normalized valuation. Nondegeneracy shows that the Frobenius scalar of a nonzero class is nonzero, including at places above the Kummer exponent.
The two coefficient paths into actual relative ideles coincide: Kummer coefficients through everywhere-integral ideles, or through field units. The first has zero H² by the proved local block and restricted-product const…
This aggregate collects unramified fixed fields and common extensions, local units cohomology, cyclic restriction maps, and finite-place localization comparisons.
The finite integral and infinite unrestricted tensor blocks have already been proved to have zero H². Coordinatewise primitives assemble across their products, and the actual equivariant S-place factor decomposition iden…
This file evaluates the normalized carry cocycle whose coefficient is a unit from the base field. Under the finite-cyclic H²--norm-quotient comparison, its class is exactly the corresponding norm class.
For a finite cyclic Galois extension, degree-two cohomology of the actual unit representation is identified first with the field norm quotient. Over a nonarchimedean local base this is then transported by finite local re…
Finite local reciprocity identifies the actual unit-coefficient H² with the cyclic Galois group. Its n-torsion therefore has at most n elements for every positive integer n, including n = 2 and every prime n.
For a cyclic extension of number fields, periodicity identifies degree-two cohomology of the unit representation with the global field-norm quotient. Composing this comparison with the concrete Hasse norm diagonal gives…
For a finite cyclic Galois extension, a unit fixed by the chosen generator is fixed by the whole Galois group. This file evaluates its class in the periodic degree-two model through the existing comparison with degree-ze…
Inflation of a cyclic degree-two units class followed by restriction vanishes for an unramified extension of the specified degree. The proof transports the base-units comparison to units cohomology.
A cyclic base-units degree-two class vanishes after inflation and restriction to an unramified relative extension whose degree divides the lower ramification index.
Induction on the actual extension degree uses a central prime-order subgroup of the Galois group. The resulting upper extension is cyclic, so local reciprocity computes its unit H². The lower extension has smaller degree…
A generator of the cyclic auxiliary field's H² inflates into the kernel of relative restriction. Middle exactness lifts it to the p-extension's H², and injectivity preserves its order. The proven cardinality bound then m…
The unramified field of the same degree supplies the auxiliary cyclic extension. Its compositum with the given field is unramified of degree equal to the ramification index. The resulting cyclicity proof transports from…
Pulling the valuation back through the actual embedding and extending that embedding to its localization relates the two Artin actions. Independence of the place above the base removes the auxiliary pullback place.
For an extension of a nonarchimedean absolute value to an algebraically closed algebraic extension, its completion is algebraically closed. Krasner's lemma then shows that the algebraic localization inside that completio…
The actual tensor block is an induced representation. Shapiro and the chosen decomposition-group equivalence identify its cohomology with the local field-unit cohomology. Finite Galois p-extensions therefore have cyclic…
For a number field and a finite place, the chosen extension of the adic absolute value to the algebraic closure defines an absolute decomposition subgroup. Its continuous inclusion in the absolute Galois group induces th…
The restriction maps to all absolute decomposition subgroups are assembled into one linear map with dependent function codomain.
Normality makes the image of the finite global field in the local separable closure independent of its embedding. The actual decomposition comparison therefore makes inertia fix every generator of its chosen finite local…
The chosen topological comparison from a number-field decomposition group to the absolute Galois group of its completion preserves inertia. Consequently it descends to a topological equivalence of the corresponding unram…
Continuous mod-p characters of the chosen decomposition group are quotiented by the characters trivial on absolute inertia.
The chosen algebraic localization embeds the global algebraic closure into the local separable closure. Its pointwise equivariance identifies the actual action used by the decomposition-group comparison. Two canonical sc…
The valuation-subring inertia group is pulled back to the chosen absolute decomposition group. Restriction to this inertia subgroup defines the unramified continuous H¹ subspace.
The unramified continuous degree-one subspaces at every finite place are assembled into a dependent product module. Coordinatewise subtype inclusion embeds it in the corresponding product of local decomposition-group H¹…
The local--global Galois comparison gives a linear equivalence between characters of the global decomposition group and of the completion's separable-closure Galois group. This equivalence identifies inertia-trivial char…
An actual representative of the absolute Artin value acts on every embedded finite abelian extension by its finite Artin automorphism. The representative condition is supplied by the quotient map, not by an Artin-compari…
Finite Artin naturality supplies the action on every finite abelian extension. The profinite finite-quotient realization then identifies the absolute value. The valuation certificate is supplied for the actual completion…
The image of the supplied finite field embedding is constructed inside the local separable closure. Inertia fixes that actual intermediate field; the spectral criterion applies there, and the resulting unramifiedness is…
Restriction to intrinsic inertia defines the unramified submodule of continuous first-cohomology characters. The residue-degree character modulo p spans this submodule, and its scalar parametrization is injective.
For a nonarchimedean local field, the continuous residue-degree map is onto the profinite integers. Its kernel is the kernel of the residue action, and the corresponding quotient is therefore continuously equivalent to Z…
The relative unramified extension is realized as a named fixed field. Its inclusion and algebra structure are compared with the relative field, and its degree, residue degree, Galois property, and unramified valuation ex…
The cohomology class of the S-place factors is determined by its finite coordinates in S when the outside integral blocks and infinite blocks are unramified. This detects classes by actual coordinate maps.
For finite local extensions K → L → M with M/L unramified, a base-field unit has L-valuation divisible by e(L/K). If [M:L] divides that actual ramification index, the unramified norm subgroup calculation produces a unit…
In K → L → N with N/L unramified and [N:L] dividing e(L/K), every K-unit embedded in L has an actual norm preimage from N. The cyclic coefficient criterion therefore kills the whole degree-two map.
The relative unramified fixed field is identified with the compositum of the chosen intermediate fields. The comparison supplies its degree, Galois structure, residue degree, and unramified valuation extension.
If an extension has relative residue degree f, then intersecting its absolute subgroup with the standard unramified degree-f m subgroup produces its own standard unramified degree-m subgroup. Both sides use the actual no…
At an unramified finite place, integer-unit H² vanishes on the chosen localized extension. The actual decomposition-group action, the proved multiplicative Shapiro isomorphism, and the equivariant integral tensor decompo…
The relative degree-m unramified fixed field over an actual finite absolute subgroup is its compositum with the standard absolute unramified extension of degree f m, where f is its absolute residue degree.
The canonical unramified Frobenius and the existing unit-norm theorem identify degree-two cohomology of the actual integer-unit representation with a zero Tate norm quotient. In particular every two-cocycle has an intege…
An absolute finite character supplies an actual principal-trivial idele character. Outside a finite support, inertia-triviality kills integral units. Global reciprocity then proves that the sum of its local pairings on t…
This aggregate collects ideal-power radicals, finite-support reciprocity characters, Kummer pairings, and localization comparisons at finite places.
Absolute continuous mod-p characters restrict at every finite place and then pass to the quotient by unramified characters. The empty-support object is the cokernel of the dual of this global-to-local map, not the cokern…
Dualizing the global-to-local ramified-character map and taking its cokernel is canonically equivalent to the dual of the kernel of the original map. Thus a subsequent self-dual arithmetic comparison can be reduced to id…
The finite valuations give a concrete localization map from global power classes to the product of their valuation defects. Its kernel is exactly the ideal-power radical. Dualizing the localization map therefore gives an…
Over a number field containing the coefficient roots of unity (in particular the chosen cyclotomic base), actual local Artin--Kummer pairing against intrinsic unramified H¹ assembles into a global localization map on Kum…
The selected algebraic-localization embedding first gives equality of the finite Artin actions. Finite projections identify the maximal-abelian global value, and semilinear naturality transports its representative to the…
The canonical comparison of the two completions preserves their valuation relations. Uniqueness of the separable-closure valuation and naturality of residue degree therefore identify their inertia groups. This gives the…
The comparison is an isometry; both valuation relations are exactly the norm comparison relation. This supplies the certificate for actual Artin naturality.
At a finite place of the cyclotomic base, transport the normalized valuation functional from local power classes to intrinsic continuous H¹. Its image is exactly the annihilator of the valuation-zero subspace.
The cyclotomic base used by the ideal-radical construction contains the required primitive p-th roots. At every finite place, those roots remain primitive in the adic completion, so absolute Kummer theory identifies loca…
This file specializes the local Artin--Kummer H¹ pairing to completions of the cyclotomic base used in the ideal-radical construction. The representative formula is also stated for the natural mup Kummer class after the…
This file compares the restriction of the natural mup Kummer class to a finite-place decomposition group with intrinsic Kummer theory over the adic completion. The coefficient map uses the actual algebraic-localization e…
The previously constructed forward map is conjugation by algebraic-closure equivalences. Its inverse is continuous by the same semilinear conjugation theorem; no compactness instance or new Galois structure is installed.
The inverse of the decomposition--adic equivalence transports the already constructed decomposition-group restriction to intrinsic local H¹.
Compatibility of the intrinsic normalized valuation with the distinguished adic valuation identifies its zero kernel with the actual completion's integral-unit subgroup. The roots-of-unity-free local reciprocity criterio…
Global power classes are localized to actual adic completions and paired against intrinsic unramified H¹. The local kernel criterion is proved from Artin--Kummer duality, including at primes above the coefficient prime.…
An ideal-radical class has valuation zero modulo the coefficient prime at every finite place. Consequently, unramified local characters annihilate its localization, and changing a character by an unramified character doe…
The intrinsic local normalization agrees with the distinguished integer-valued adic valuation: the only order-preserving automorphism of the integer value group is the identity. Consequently localization of global power…
Restrict a principal-trivial continuous idele character to finitely many one-place factors. If the original character kills integral units outside that set, the quotient of the original and restricted characters kills ev…
If the local reciprocity functional annihilates the ideal-power radical, exactness of finite-valuation localization expresses it as a valuation functional. Subtracting the corresponding continuous idele character kills a…
The ideal-radical annihilator condition supplies a genuine global abelian character. Actual local Artin compatibility and the integral-unit criterion turn its idele values into equality on inertia, including places outsi…
A finite family of continuous local mod-p characters evaluates on actual idele coordinates. The finite product is continuous, and its value on a principal idele is the sum of the localized power-class pairings.
This file defines the field elements whose principal fractional ideals are positive powers, quotients them by field powers, and maps the resulting radical onto the matching torsion subgroup of the ordinary ideal class gr…
For a number field containing a primitive n-th root of unity, this file embeds the empty-support Selmer group, and hence the ideal-power radical quotient, into the continuous mod-n characters of the absolute Galois group…
For a number field containing the p-th roots of unity, the ideal-power radical embeds canonically into the continuous absolute mod-p character module. Dualizing this inclusion gives the corresponding surjective restricti…
This file supplies the missing maps in the empty-support Selmer sequence: ordinary units modulo powers inject into the ideal-power radical, whose ideal-root class map surjects onto class-group power torsion.
For a prime p, the empty-support ideal-power radical quotient has exponent dividing p. This file packages its additive presentation as the canonical ZMod p-module, proves finite-dimensionality, and records the resulting…
This file converts the cardinality formula for the empty-support ideal-power radical into the dimension formula used in Shafarevich's relation-rank bound.
This file identifies the ideal-power condition on a principal fractional ideal with the empty-support Selmer condition on its Kummer class.
For a number field F and a prime p, this file chooses a primitive p-th root in AlgebraicClosure F, names F(μp), and maps the empty-support ideal p-power radical into an admissible Kummer subgroup over that cyclotomic bas…
The restricted ideal radical over the chosen cyclotomic base is a quotient of the base-field ideal radical. Its dual therefore embeds canonically into the base-field radical dual. This file applies that embedding functor…
The ideal radical over F maps onto the restricted radical generated after adjoining a primitive p-th root of unity. This file makes that quotient and the quotient map linear, then dualizes the surjection to a canonical i…
For a number field F and a prime p, this file adjoins the p-th roots of the empty-support ideal radical after passing to F(μp). Kummer theory identifies the resulting finite abelian exponent-p Galois group with the chara…
The Kummer character isomorphism for the governing extension is linearized over ZMod p. Thus every governing automorphism gives a functional on the cyclotomic restricted ideal radical, and the resulting linear map is fai…
Any algebraic functional on the product of mod-p valuation defects gives a continuous idele character. No continuity of the functional on that product is required: its composite vanishes on the open subgroup of ideles in…
A continuous character trivial on each finite integral one-place idele is trivial on their entire product, by convergence of the finite partial products. Odd powers are surjective on the archimedean factors. Thus an odd…
The arithmetic obstruction space used in the Shafarevich relation-rank argument has two finite pieces: an S-unit Kummer quotient and the elementary ideal class quotient. This file packages those pieces as one finite-dime…
At a finite place of a number field, normalized valuation modulo p descends to a surjective linear map from local p-power classes to ZMod p. Its dual embeds the one-dimensional valuation-defect space into the dual of the…
This file computes the cardinality and ZMod p-dimension of the ordinary number-field unit group modulo p-th powers. The torsion correction is one exactly when the field contains a primitive p-th root of unity. The module…
The quotient of a principal-trivial idele character by its finite restriction has the same real signs, since that restriction has only finite coordinates. The real-signed quadratic idele theorem therefore annihilates its…
Positive real units and all complex units have square roots. A quadratic character killing the real sign generators therefore kills every infinite idele. Finite integral-unit triviality then kills integral ideles and the…
A continuous map from the absolute Galois group to a discrete group has open kernel. Its finite Galois fixed field is ramified at only finitely many finite places. Actual absolute inertia restricts into finite ideal iner…
The actual open-kernel fixed field is finite Galois with p-group Galois group. Pointwise absolute inertia triviality makes it unramified at finite primes; odd p makes its infinite primes unramified. Its inclusion in the…
For an open normal finite p-quotient of the absolute Galois group, finite transgression first lands in the degree-two cohomology of the absolute group modulo its unramified kernel. The topological quotient equivalence th…
Restriction from the absolute Galois group to the maximal everywhere-unramified pro-p extension is a continuous quotient map. Its closed normal kernel is the subgroup fixing that extension, and quotienting by the kernel…
This file defines inflation from the maximal everywhere-unramified pro-p Galois group to the absolute Galois group and records its finite-place localization as pullback along the composite local decomposition map. Provin…
Inflation from the maximal everywhere-unramified pro-p quotient has zero restriction at every finite place. This file bundles that source theorem as a linear map into the kernel of simultaneous localization.
The topological first-isomorphism equivalence for absolute restriction identifies degree-two continuous cohomology of the maximal everywhere-unramified pro-p Galois group with that of the corresponding quotient of the ab…
The quotient/arithmetic-stage equivalence is checked on actual field automorphisms against restriction from the absolute Galois group. Thus the proved arithmetic-stage vanishing applies to every finite quotient. Finite-s…
This aggregate collects arithmetic-stage localization and transgression comparisons, degree-two vanishing results, ramification-support bounds, and relation-rank bounds.
Over a base containing mup, the actual finite unramified stage supplies a field-unit primitive through the supported-idele construction. Hilbert 90 and the root correction turn this into an actual continuous lift of the…
The stage's everywhere-unramified certificate applies at the actual global centre of the chosen finite-place extension. The ideal-to-completion comparison therefore supplies unramifiedness for the chosen local completion…
Adding coefficient coordinates solves the embedding problem of the sum class. Its difference from the chosen solution is a global character, and all three lifts are unramified outside the fixed stage support. On inertia…
A nonzero degree-two class of the maximal everywhere-unramified pro-p Galois group is detected on a finite quotient. The quotient is transported to the Galois group of its concrete arithmetic stage, carrying the cocycle…
At a finite place, restrict the arithmetic-stage quotient to its chosen decomposition group. The restricted degree-two class is the local splitting defect: it vanishes exactly when the pulled-back central extension has a…
Transporting the explicit cocycle-extension projection to its finite everywhere-unramified arithmetic stage does not change its kernel. A nonzero stage class therefore has a cyclic kernel of order p contained in the Frat…
The proved vanishing of absolute inflation supplies an actual continuous global solution of every finite arithmetic-stage central embedding problem. Restricting it to decomposition groups and subtracting the constructed…
The kernel of a finite arithmetic-stage degree-two embedding problem is the lifted ZMod p coefficient. Consequently, an actual character of the cyclotomic ideal radical valued in that central kernel determines a unique a…
Compare a local solution with the unramified solution constructed from the vanishing of unramified local H². Their difference is a continuous ZMod p-valued character on the absolute decomposition group. Its restriction t…
The radical functional detects zero after inflation. A linear section of the map onto the inflation range therefore gives an injective map from that range to the radical dual. This uses only the proved kernel inclusion;…
Finite-stage mod-p H² is a finite set. The union of the ramification supports of all its chosen global lifts is consequently one fixed finite set. On this set the actual local lift differences, transported to the adic ab…
A zero radical functional supplies a global character agreeing with the chosen lift's inertia defects. Correcting the lift by this character kills every finite inertia group. The actual maximal-unramified factor therefor…
The local additivity defect agrees on inertia with one actual global character. Global reciprocity annihilates that character on the ideal radical, while unramified local changes do not affect the pairing. Thus the chose…
The absolute decomposition group modulo inertia is procyclic and has zero continuous H². Pulling a finite arithmetic-stage cocycle extension back to this quotient therefore supplies a continuous lift to the original exte…
The actual stage supplies its p-group Galois group and unramifiedness at every place. The proved supported-idele construction and field-unit H² injection therefore kill its Kummer H² classes and produce field-unit primit…
The open-normal arithmetic stage supplies both finite- and infinite-place unramifiedness. Thus its everywhere-integral relative idele subgroup has zero H², and every supported two-cocycle has an actual idele primitive. T…
The named cyclotomic base has degree strictly below p. Its fixing subgroup in the absolute Galois group is therefore open of index prime to p, and continuous degree-two restriction is injective by the proved transfer arg…
The actual cyclotomic base change of an unramified arithmetic stage is mapped into the standard cyclotomic algebraic closure using exactly the equivalence underlying finite-extension absolute restriction. Evaluation on f…
Inside the fixed algebraic closure of F, let C = F(μp) and let L be the open-normal arithmetic stage. The field below is the actual compositum C L, regarded as an intermediate field over C. Its two generator ranges are p…
Mapping the actual compositum along a supplied algebraic-closure equivalence gives a finite everywhere-unramified p-extension in the cyclotomic base's standard algebraic closure. The equivalence is the concrete closure c…
The actual embedding of the original stage in the mapped compositum defines restriction of automorphisms. Its evaluation law is expressed in the same closure equivalence used to form the mapped field, supplying the finit…
The existing finite-extension identification realizes the absolute Galois group of the top field as its open fixing subgroup in the bottom absolute Galois group. Transporting prime-to-index restriction along this actual…
This file compares the chosen absolute inertia subgroup at a finite place with finite Galois subextensions of the algebraic closure. The finite-level restriction statement is the arithmetic input for showing that absolut…
A represented global power class can ramify only where its representative or the exponent p fails to be a unit. Both exceptional sets are finite. This packages the resulting finite-support statement for every natural-coe…
Away from a prescribed finite set and from the residue characteristics dividing p, an S-unit Kummer extension is unramified. This file applies that arithmetic statement to the chosen algebraic-closure root defining the n…
At a finite place, absolute restriction to the maximal everywhere-unramified pro-p extension kills inertia. It therefore factors through the unramified quotient of the selected decomposition group. The chosen local compa…
The supported-idele primitive and the Hilbert-90 correction apply to an actual finite everywhere-unramified p-extension, independently of how it was obtained as a finite stage. This form also applies to the mapped cyclot…
An injection into the dual ideal-power radical gives finite-dimensionality and the numerical term in Shafarevich's relation-rank bound. The final specialization replaces the p-class rank by the generator rank of the maxi…
This file isolates the three representation differences between the production theorem and the trusted benchmark statement: the explicit everywhere-unramified predicate, finite-set generator rank, and small versus univer…
An open normal quotient of the maximal everywhere-unramified pro-p Galois group is realized by the Galois group of a concrete finite everywhere-unramified p-extension. This is the finite-stage arithmetic bridge used befo…
For every number field and every odd prime, the maximal everywhere-unramified pro-p Galois group has finite-dimensional H². Its relation rank is at most the generator rank plus the unit rank and the roots-of-unity correc…