Class field theory

Public root for abstract degree data, class formations, reciprocity, and the construction and naturality of Artin maps. The public declarations live in the ClassFormation namespace. This library is independent of local c…

Focused aggregate for abstract fields, normalized degrees, Frobenius, norms, prime elements, and valuation laws used by class formations.

This file records the opening datum of abstract valuation theory and the residue and ramification indices attached to inclusions of abstract fields. As in, a field is represented contravariantly by a closed subgroup of t…

For a field of finite residue degree, this file constructs the map dK = (1 / fK) d; division is performed only after proving that d(GK) = fK ℤ̂. The Frobenius is then the unique class mapping to 1.

This file gives the group-dual form of the Frobenius fixed-field theorem. If σ is a Frobenius lift in G(\widetilde L | K), the subgroup Γ fixing the field Σ is the closed subgroup topologically generated by σ.

This file defines the Frobenius semigroup in G(\widetilde L|K) and proves the lifting statement of the finite degree-quotient decomposition. Positivity is explicit, so the convention 0 ∉ ℕ is not lost in Lean's natural n…

This file isolates the group-theoretic index calculation used in abstract valuation theory. For a homomorphism d, an inclusion L ≤ K splits its relative index into the index of the images under d and the relative index i…

This file constructs the norm attached to a finite extension of the abstract fields. An abstract field is represented, as in, by a closed subgroup of the ambient profinite group. The norm is the sum over left cosets (the…

These are the field-conjugation and norm identities used in the abstract reciprocity construction and theorem. They belong before the reciprocity construction: their proofs use only the actual relative norm and the conju…

This file proves the structural laws for the coset-sum norm constructed in Norm.lean.

This file isolates the topological group argument used in the finite-place Frobenius construction. A continuous ℤp-degree with finite kernel detects openness of the closed subgroup generated by any element of nonzero deg…

This file formalizes the prime-element definition and its two immediate consequences for unramified and totally ramified extensions.

This module extends the concrete ZHat reduction maps to every finite-index additive quotient of ℤ. The construction first identifies such a subgroup with the multiples of its index, then uses the existing reduction to ZM…

The multiplicative coefficient module is represented additively, as in . Accordingly a valuation and a norm are additive homomorphisms. This file formalizes the valuation-quotient axiom and constructs the normalized valu…

This file proves the two functorial assertions of normalized-valuation functoriality from the source norm laws.

Public aggregate for the class-formation reciprocity theorem and the canonical construction and naturality of its reciprocity maps.

This file gives the inverse direction of the finite abelian classification: a norm-open subgroup produces its class field. The construction is the inverse of the order isomorphism proved by abstract class field theory, s…

The coefficient group for a finite cyclic extension L / K is the actual fixed module AL, descended to the actual quotient GK / GL. Thus the two numbers below are the orders of the Tate groups occurring in the original st…

This file isolates the source-producing part of finite-classification surjectivity. An open subgroup H ≤ AK contains an actual finite Galois norm subgroup. Modulo that norm subgroup, H gives a concrete subgroup. Transpor…

Aggregate for norm quotients, Frobenius descent, prime independence, transfer naturality, and the canonical abstract reciprocity map.

the valuation-quotient axiom supplies the order of Z / nZ. The construction then uses the canonical reduction inherited from Z ⊆ ℤ̂, rather than an arbitrary isomorphism with ℤ / nℤ. This file constructs that canonical m…

Surjectivity of the normalized degree supplies a Frobenius-semigroup element of exponent one. The chosen object and its specification are kept together here so the multiplicativity proof can consume a named choice bounda…

The operator φn is written additively as the sum of the first n powers of the actual quotient action. This file compares that sum with the relative norm through the Frobenius fixed field Σ constructed in the Frobenius fi…

This module contains the group-theoretic geometry used by the transfer formula: orbit quotients of coset spaces, inversion of double cosets, transport along surjective equivariant maps, and replacement of a cyclic subgro…

This module proves valuation invariance on Frobenius fixed fields and constructs the induced actions, inclusions, and relative norms on the corresponding finite unit groups.

These are the finite-stage closure facts used in the proof of the universal norm-descent lemma. The compositum of two finite intermediate fields is their intersection on the Galois-group side.

This module records the quotient cardinal and common-compositum facts for finite intermediate fields used by the norm-descent tower.

For finite L | K, the universal norm subgroup from \widetilde L is contained in the single norm image from L. Hence the reciprocity construction descends canonically to AK / N{L|K}AL, the target in the finite reciprocity…

This module constructs the unit-valued correction term on a Frobenius fixed-field tower and proves its coefficient and relative-norm identities.

This module packages the fixed-tower action and power correction, applies the unit-cohomology axiom, and proves the corrected universal norm-descent equation on finite fixed-field towers.

This module promotes commutation with a Frobenius generator to its closed procyclic subgroup and derives the conjugation identities for the associated fixed field.

The two maps on G(\widetilde L/K)--restriction to G(L/K) and normalized degree--are jointly injective. This is the group-theoretic fact used when two Frobenius lifts have the same restriction and degree.

This file passes from the group-dual Γ of the Frobenius fixed-field theorem to the actual abstract field Σ. Thus GΣ is the inverse image of Γ under GK → GK / IL, embedded back into the ambient profinite group.

This module defines the action induced on a Frobenius fixed field and proves its compatibility with conjugate-stable actions, relative norms, inclusions, and Frobenius power sums. Mathlib's Rep ℤ G requires its coefficie…

Bundles finite towers of Frobenius fixed fields together with the normality and finiteness data needed for norm and unit calculations.

This module constructs the fixed fields of powers of a Frobenius element and proves their inclusion, exponent, normality, unramifiedness, finiteness, degree, quotient-cardinality, and generator properties.

This module constructs the Frobenius quotient representation, identifies its Birkhoff sums with Frobenius power sums, and proves the finite-support descent from the maximal unramified field. Mathlib's Rep ℤ G requires it…

The set Frob(\widetilde L | K) from is closed under multiplication: normalized degrees are positive natural numbers and add under products.

This module bundles finite intermediate fields over a finite base, defines the infinite unit subgroup, proves its action and norm stability, and descends maximal-unramified norm equations from finite support.

This module defines the finite-level and infinite unit norm ranges, proves their tower compatibility, and compares them with the ambient norm subgroups.

This file carries out the descent preparation. The reciprocity value on the Frobenius semigroup is first mapped to the finite norm quotient. We then compare two lifts by their positive Frobenius exponents, construct the…

This aggregate exposes the construction proving that the abstract reciprocity map respects multiplication.

This file transports prime elements across Frobenius-action conjugation and proves equality of their relative norms in the base fixed field. Mathlib's Rep ℤ G requires its coefficient ring and acting group in the same un…

This file packages the three correction coefficients and action elements, proves their degree-zero property, and identifies their action-difference sum.

This file proves that the alternating Frobenius power sum and each coefficient of the three-term correction identity are genuine finite-stage units.

This file develops the Frobenius exponent, conjugation, quotient-action, and action-remainder identities used by reciprocity-map multiplicativity. Mathlib's Rep ℤ G requires its coefficient ring and acting group in the s…

This file proves the three-term action identity obtained from the Frobenius action remainders and their associated fixed-field prime elements.

This file passes the alternating Frobenius power-sum norm relation to the maximal-unramified norm quotient and then to the reciprocity map.

This file proves that differences of Frobenius fixed-field primes, including differences from quotient-action translates, come from finite-stage units.

This file assembles the Frobenius conjugation, finite-stage unit, correction sum, and universal norm-descent results into reciprocity-map multiplicativity. Mathlib's Rep ℤ G requires its coefficient ring and acting group…

The two vertical maps are constructed here on the actual finite Galois quotients and the actual finite norm quotients. Their defining commutativities are proved from norm transitivity and conjugation, so the eventual the…

Constructs the transfer map for intermediate Galois quotients and relates it to Frobenius restriction and norm naturality. Mathlib's Rep ℤ G forces its representation-bearing group G to Type 0. Mathlib's Rep ℤ G forces i…

This module continues the geometric transfer construction with the chosen norm-orbit representatives, fiber calculations, fixed-field arithmetic, and the final Frobenius transfer formula. Mathlib's Rep ℤ G requires its c…

For a finite Galois extension and an intermediate field, this module builds the Frobenius-side subgroup and orbit equivalences used in transfer--norm naturality. The reusable orbit and double-coset constructions are isol…

For an infinite abstract extension E | K, the abstract class-field construction defines N{E|K} AE as the intersection of the norm images from all finite intermediate fields. This file records that definition literally.

Surjectivity of the normalized valuation supplies a prime element in every finite abstract field. Any two choices differ by a unit (additively, their difference has value zero).

For a Frobenius element σ, let Σ be its fixed field. The reciprocity class is the class of N{Σ|K}(πΣ) in AK / N{\widetilde L|K} A{\widetilde L}. Independence of the prime element is proved separately from the unit-cohomo…

This file supplies the finite-Galois cofinality and compositum argument used to prove that the reciprocity construction is independent of its prime element.

The norm calculation in the proof of transfer--norm naturality partitions the left cosets for an extension by the orbits of an intermediate subgroup. This file constructs that partition from Mathlib's class-formula equiv…

This file supplies the group-theoretic source used in transfer--norm naturality. If a surjection has kernel contained in a finite-index subgroup, it identifies the two left-coset spaces and transfer commutes with the ind…

For a finite-index subgroup H and an element g, the intersection of the closed cyclic subgroup generated by g with the stabilizer of a coset is generated by the power whose exponent is that orbit's minimal period. This i…

The coefficient group in the unit-cohomology axiom is the actual unit subgroup UL, with the action of the actual quotient GK / GL. The two Tate groups are the homology objects of the finite-cyclic norm complexes.

Proves the universal norm-descent argument from maximal-unramified units to finite intermediate norm subgroups.

This module contains the representation-theoretic lifting and correction calculation used by the abstract reciprocity construction, together with the norm, action, and iterate identities it requires.

unramified norm quotient For a finite unramified Galois extension L / K, normalized valuation identifies the actual norm quotient AK / N{L/K} AL with ℤ / [L : K]ℤ. The only non-formal part of injectivity is the unit corr…

The class field axiom implies the unit-cohomology axiom for every finite unramified extension. The proof follows: degree minus one is reduced to the corresponding assertion for AL, after correcting a primitive by an elem…

For a finite cyclic abstract extension L / K, this file identifies the actual quotient AK / N{L/K} AL with the degree-zero Tate homology object used in the class-field axiom. This is the source comparison needed before t…

This file identifies the invariant carrier used by extensionFixedRepresentation A K L with the actual fixed group AL, and compares the representation norm with N{L/K}.

The first paragraph of the finite classification proof uses the two restriction maps from the Galois group of a compositum. This file constructs those maps on the actual finite quotients and proves that they are jointly…

the finite abelian class-field classification classifies finite abelian extensions L | K by their norm subgroups. This file builds the extension side of that correspondence independently of the reciprocity isomorphism: a…

The norm topology is indexed by the actual finite Galois extensions of a fixed abstract field. This file packages those extensions and their composita contravariantly as intersections of closed subgroups.

For the three reductions in the proof of the abstract reciprocity theorem, this file supplies the finite Galois correspondence in the direction used by the construction. If L / K is a packaged finite Galois extension and…

This file assembles the three reductions. The terminal cyclic totally ramified calculation is proved in AbstractClassFieldTheory.Reciprocity.TotallyRamifiedCase. Reciprocity naturality states three diagrams for the norm…

The maximal-unramified norm-residue symbol is realized by the valuation--Frobenius map whose restriction to every finite unramified extension is the inverse of the unramified norm-quotient equivalence. This file first pr…

This file constructs the source maps used in maximal-unramified reciprocity. In particular, the maximal unramified quotient is projected to every finite unramified Galois quotient, and its Frobenius is sent to the finite…

For a finite extension L / K, the base change to L of a finite Galois extension M / K is finite Galois. Norm transitivity then sends its norm subgroup into , providing the key continuity input.

The neighbourhood basis at zero consists literally of the norm subgroups N{L/K} AL as L / K ranges over finite Galois extensions. Composita make this family downward directed.

This file supplies part (i), whose finite-index assertion uses the actual reciprocity isomorphism of the abstract reciprocity theorem. Parts (ii)--(iv) are proved in the imported valuation-, norm-, and norm-topology modu…

This module specializes the three principal finite reciprocity endpoints to a bundled profinite group. The bundle supplies the ambient topology, compactness, separation, and total disconnectedness instances required by t…

This file isolates the field- and quotient-theoretic content of the three reductions. In particular, the Sylow reduction uses an intermediate field which need not be normal over the base. We therefore construct its norm…

This file formalizes the source-producing group-theoretic part of the first reduction. For a Sylow p-subgroup P of the actual finite quotient G(L/K), the already constructed fixed field M = L^P is an actual (not necessar…

This file isolates the calculation. The input from the finite reciprocity equivalence is an equality in an actual finite norm quotient. Such an equality is first turned into an equality of actual norms. For the cyclic to…

This aggregate module exposes the constructed Frobenius tower, restriction equivalences, fixed-source calculation, and the final reciprocity theorem.

This file derives exponent vanishing, injectivity, and finally bijectivity of finite reciprocity from the constructed fixed source.

This file converts a finite cyclic extension to the canonical finite Galois boundary and carries out the source-producing fixed-element calculation.

This file constructs degree-one Frobenius lifts and the finite auxiliary Galois extension used in the totally ramified reciprocity argument.

This file constructs the Frobenius element in the auxiliary extension and proves its restriction, commutation, action, and relative-norm identities.

This file constructs quotient restriction maps, their coset equivalences, and the compatible relative actions and norms used in ramified towers.

This file identifies the lower Galois group with the original totally ramified quotient and constructs its cyclic generator.

The proof uses the neighbourhoods f ℤ̂. We construct the required unramified extension of degree f as the fixed field of the kernel of reduction modulo f after the normalized degree map dK. The norm--valuation formula th…

Compatible equivalences of the base and extension fields identify their Galois automorphisms and preserve the abelian Galois property. These results use only Mathlib's algebra and Galois APIs; they do not depend on local…

Aggregate of the modules and subdirectories in ClassFieldTheory.Algebra.

An algebra equivalence of ambient fields transports finite-dimensionality and the abelian Galois property of every intermediate field.

An algebra equivalence of ambient fields induces an order equivalence of their intermediate-field lattices. This is the ambient-change step used for Mathlib's chosen separable closures.

The chosen finite K-basis of L identifies 𝔸K ⊗[K] L with a finite family of base adeles. The support file constructs and controls the forward coefficients; this file supplies the inverse assembly map. It is the global re…

This file is the finite-place counterpart of InfinitePlaceTensorBlock. It compares the concrete completion Kv used by the idele restricted product with the absolute-value completion used by the canonical local tensor dec…

This file flattens the finite local tensor factors of a relative idele over K into the ordinary finite-place factors of L. The local map is The canonical local tensor decomposition followed by the comparison between an e…

The concrete archimedean completion w.Completion used by the adele library is canonically the completion of the underlying absolute value w.1. Base change along this equivalence connects the actual archimedean component…

For a finite place w of the base field, the canonical local tensor decomposition identifies Kw ⊗K L with the product of the completions of L above w. This file packages each projection as an actual ring homomorphism and…

This file continues the finite-support construction for relative tensor decompositions. A single nonzero integer is chosen which carries every vector of the fixed K-basis of L into 𝓞 L. Their 𝓞 K-span is a full lattice i…

Public aggregate for the lattice, localization, local tensor decomposition, and finite-support results controlling integral relative ideles.

This module compares the absolute-value and adic-completion models at finite places and records how the resulting maps preserve norms and integrality.

This module combines coefficient support with the exceptional places of the local tensor decomposition, producing one finite set that controls integrality of a relative idele and its inverse.

This module chooses a common integral scale for a field basis, constructs the associated integer lattice, and isolates the finite set of primes where its local integrality properties can fail.

This module identifies integrality and units in a finite-place tensor factor with the corresponding componentwise conditions in the completions above that place.

Away from the finite exceptional set, this module compares the localized integer lattice with the integral closure and derives coordinatewise integrality after localization.

The archimedean and finite tensor components jointly determine an element of 𝔸K ⊗[K] L. This file records the corresponding injective homomorphism on relative ideles. Surjectivity onto the restricted local product is han…

The Galois action on 𝔸K ⊗[K] L commutes with evaluation at every place. Consequently the exact restricted-product equivalence for relative ideles is equivariant, and the transported action is the coordinatewise tensor-co…

Using the chosen finite K-basis of L, a family of local tensor components comes from 𝔸K ⊗[K] L precisely when each basis coefficient is integral at almost every finite place. Applying the same condition to a family of lo…

This file upgrades the relative-to-ordinary idele comparison to the underlying adele rings. The additive structure is needed to transport determinant norms in a field tower.

Public root for the reusable global algebraic-number-theory layer used by class field theory. It exports finite abelian composita, idèles and idèle classes in extensions, normal-closure and splitting results, ray class g…

The completion map attached to an exact extension of a finite-place absolute value agrees with the canonical map between the concrete adic completions at the corresponding finite places.

A finite place above a base finite place determines the continuous extension of the number-field algebra map to their concrete adic completions.

This file equips the actual chosen localization of a finite number-field extension with its canonical valued local-field structures. It also defines unramifiedness for that actual completed extension.

For an exact extension w of the normalized absolute value at a finite place v of K, its centre W is a finite place of L. The absolute values w and the standard normalized absolute value at W differ by a positive real pow…

This file supplies the finite-place index comparison needed to pass from the relative adelic tensor product to the ordinary adeles of the extension field. It is deliberately independent of the restricted-product construc…

The existing continuous maps of adic completions along an equivalence of number fields are mutual inverses. This bundles them as a field equivalence for transporting local Hilbert pairings.

This file restricts the canonical equivalences between the absolute-value and adic completion models to their valuation rings. It also identifies the residue field of a rational finite-place completion.

This file equips nonarchimedean absolute-value completions and their algebraic localizations with the norm-induced valuation structures. It identifies the localized valuation ring with the integral closure of the base va…

This file recovers ideal-theoretic unramifiedness from the actual chosen localized completion and propagates it to every place above the base place in a finite Galois extension.

This file proves that ideal-theoretic unramifiedness at the centre of the actual chosen finite-place extension implies unramifiedness of its localized completion.

This file proves that the concrete adic integer units lie in the actual local norm subgroup of the chosen localized completion.

The ideal-theoretic ramification index at the centre of a finite-place extension agrees with the ramification index of the corresponding explicit localized completions. The comparison uses a global integral uniformizer:…

Two finite normal extensions embedded in a common field generate the same compositum as their chosen realizations in the separable closure. This normality argument is the field-theoretic mechanism used to place the local…

This file gives a common realization, in a chosen separable closure, of the compositum of two finite abelian Galois extensions. It also records the canonical factor embeddings and their elementary degree bounds.

For an arbitrary field, this module identifies the topological abelianization of the Galois group of its separable closure with the Galois group of the maximal abelian subextension. Working inside the separable closure m…

This file supplies an induction field for finite cyclic extensions. If L / K is a nontrivial finite cyclic Galois extension, choose a prime p ∣ [L : K]. For a generator σ of its Galois group, the subgroup generated by σ…

This file constructs a prime-degree intermediate field. For a nontrivial cyclic Galois extension whose group has order p ^ exponent, the index-p subgroup constructed in SplittingGroupTheory is sent through the finite Gal…

Small order-theoretic facts about fixed fields of automorphism subgroups. They do not depend on class field theory and belong with the general Galois infrastructure rather than a concrete reciprocity construction.

This module supplies the field-theoretic passage from finite Galois layers to their union after a change of base field. It is stated entirely in terms of mathlib's actual intermediate fields and uses no abstract replacem…

Restriction from the algebraic closure to the separable closure identifies Mathlib's absolute Galois group with the separable-closure model. The induced map on topological abelianizations is a homeomorphism of groups, no…

A field equivalence extends to an equivalence of the chosen algebraic closures. Conjugation then identifies the absolute Galois groups, including their Krull topologies, and hence their topological abelianizations.

For a finite extension L / K, its chosen finite normal closure contains a distinguished copy of L. The subgroup fixing that copy, together with the commutator subgroup of the full Galois group, cuts out the largest abeli…

This file records the intrinsic image of a normal field extension inside an ambient field: every embedding over the base has the same intermediate-field range.

For a possibly infinite Galois extension M/F, this file identifies the topological abelianization of Gal(M/F) with the Galois group of the intermediate field fixed by the closed commutator subgroup.

A finite-dimensional extension has only finitely many automorphisms. An infinite Galois group therefore supplies arbitrarily large linearly independent finite families. Their finite Galois closures give the required actu…

Public aggregate for the idele group and the idele class group of a number field.

The finite restricted-product comparison is combined here with the archimedean form of the canonical local tensor decomposition. Infinite places above a fixed infinite place of the base field are identified with exact ex…

This file defines the ideles of a number field. The finite ideles are defined as the restricted product of the multiplicative groups of the finite completions with respect to the unit groups of their valuation rings. Thi…

If two finite extensions of a number field are isomorphic over the base, their tensor-product presentations of the relative adeles are canonically isomorphic. This file descends that canonical isomorphism to relative ide…

The archimedean factor is a product of continuous completion maps. The finite factor is a continuous map of restricted products because each completion map preserves the local valuation subring.

The finite-completion map associated with a field equivalence preserves the local valuation subring. This is the restricted-product compatibility needed for continuity of adelic transport.

The continuous adele-ring transport induces continuous transport of units and then of the quotient by principal idèles. These topological equivalences have the previously defined algebraic maps as their underlying maps.

The finite-completion map used by adeleCongr is continuous. This is the local continuity input for transporting the restricted-product topology.

Public aggregate for the ordinary ideal class quotient of the ideles and its base-change, norm-comparison, tower, and algebra-equivalence constructions.

For a pushout square of finite extensions K ─→ M │ │ ↓ ↓ L ─→ N this file constructs the maps on relative ideles and idele classes that occur after adjoining roots of unity. Keeping the bottom adele ring fixed makes the…

A topological group equivalence carries the connected component of one onto the connected component of one. It therefore induces an equivalence of the corresponding quotient topological groups.

This file proves that quotienting the idele group by the ideles integral at every finite place and by the principal ideles gives the ordinary ideal class group.

The completion maps along an isomorphism of number fields are mutually inverse. This is the archimedean local input for the topology of adeleCongr.

The restricted-product idèle group and Mathlib's adele-unit idèle group are already multiplicatively equivalent. The principal subgroups correspond, so the equivalence descends to idèle classes. The one-place map compari…

The algebraic equivalence from the restricted-product idèle class group to Mathlib's adele-unit quotient is continuous. This is the quotient descent of the continuous map on idèles.

The determinant norm on relative ideles and the ordinary idele norm give the same map after the canonical scalar-extension equivalence C(𝔸K ⊗K L) ≃ CL. This comparison lets the cohomological results proved in relative co…

The distinguished copy of a finite extension inside its normal closure is an intermediate field. Norm transitivity therefore puts every norm from the normal closure inside the norm subgroup of that copy. Transport across…

For a tower K ⊂ M ⊂ L, keep the bottom field K fixed and write 𝔸M = 𝔸K ⊗[K] M, 𝔸L = (𝔸K ⊗[K] M) ⊗[M] L. This gives an actual norm CL → CM whose composite with CM → CK is the tower norm. The resulting three concrete norm…

The ordinary idele group of a finite extension is obtained from the relative tensor presentation by scalar extension. This file proves that this comparison is natural when both fields in the extension are replaced by com…

For a tower K ⊂ M ⊂ L, IdeleClassTower presents the ideles of L as units of (𝔸K ⊗[K] M) ⊗[M] L. Here we compare that presentation with the actual relative idele group 𝔸M ⊗[M] L, by passing through the ordinary ideles of…

For a finite set S of finite places, this file identifies the actual subgroup IK^S with the product of all archimedean local groups, the full multiplicative groups at places in S, and the local unit groups away from S. T…

This file realizes the low-degree exact sequence on the actual relative idele group 1 → Lˣ → IL → CL → 1. The Galois actions are the concrete conjugation actions from the tensor-product model of relative adeles. The clas…

This file isolates the final cardinality argument in the idele-class Herbrand calculation. The Herbrand quotients of the supported ideles and of the corresponding principal ideles have a common nonzero local-degree facto…

Public aggregate for the local, finite-family, and factor-transport Herbrand calculations.

This leaf transports the finite-family Herbrand calculation to the actual unrestricted relative S-idele factors.

This leaf computes the two finite-family Herbrand cardinalities from the finiteness results and the canonical family instance providers.

This leaf assembles the local Herbrand calculations over the finite family of unrestricted places.

This file combines finite local class field theory with the explicit real/complex norm calculation. It treats the finite family consisting of all infinite places and the finite places in S.

For a finite set S of finite places, the unrestricted factors consist of every infinite place and the finite places in S. This file packages those two kinds of concrete tensor factors into one finite dependent family and…

This is the public import entry point for the local integral induced-block construction and its chosen-finite-place specialization.

This file specializes the integral induced-block construction to the actual chosen localization above a finite place and proves its unramified Tate cohomology consequences.

This file exposes the decomposition-group action and the direct local cohomology endpoint used by the integral induced-block construction. Keeping this localization boundary in a lower leaf prevents downstream transport…

This file combines the independent induced-block and tensor-block equivariance lemmas into the transport used by the cohomology layer.

This file constructs the equivalence between the chosen integral tensor block and the induced module of chosen local integer units.

This file compares the integral-block inclusion with the finite-place tensor equivalence on underlying field units.

This file embeds the chosen induced module of local integer units into the ordinary local multiplicative block and proves injectivity.

This file proves that the inclusion of the chosen integral induced block is equivariant for the global Galois action.

This file proves equivariance of the finite-place tensor-unit block under the restricted global Galois action.

This file transports completion fields and their valuation rings from every right coset of a decomposition group to the chosen algebraic localization.

This file identifies the product of valuation-ring unit groups over the extensions of a finite place with the corresponding induced module.

Public facade for the shared completion spine, action, product equivalence, and inclusion leaves.

This leaf identifies the product of completed integer-unit groups with the induced integer-unit module.

This leaf embeds the induced integer-unit module into the ordinary local multiplicative induced block and proves injectivity.

This file names the coherent algebra, valuation, and integral-closure structures used by every integral local-induction leaf.

The factor model of a supported relative idele is reassociated into the finite family of unrestricted places and the product of integral factors outside the support. The comparison respects the concrete Galois actions.

This file constructs the finite set used in the idele-class Herbrand calculation. It contains the contractions of a sufficiently large set of places of L and every finite place of K at which some place of L ramifies. It…

Public aggregate for base change, extension, and norm maps on ideles and idele classes.

This file uses the canonical presentation 𝔸L = 𝔸K ⊗K L. This makes extension, Galois conjugation, and the idele norm formal linear-algebra operations.

The tensor-product model makes the key intersection calculation IK ∩ Lˣ = Kˣ an elementary linear-algebra statement. A linear retraction of K → 𝔸K shows that an equality a ⊗ 1 = 1 ⊗ x forces both factors to come from the…

This file proves the embedded-subextension determinant-norm formula. If L/K is embedded in a finite Galois extension M/K, extending the determinant norm of an element of A ⊗[K] L to A ⊗[K] M gives the product over all K-…

For a finite Galois extension L/K, the Galois action on relative ideles preserves principal ideles and hence descends to the relative idele class group. Noether's form of Hilbert 90 then shows that every fixed class has…

This file proves that, in the tensor-product presentation 𝔸L = 𝔸K ⊗K L, extension of the determinant norm back to 𝔸L is the product of all Galois conjugates.

For a finite Galois extension of number fields, scalar extension of the relative adele algebra followed by the relative-to-ordinary comparison gives the usual extension map on ideles. This file descends that map to idele…

The tensor-product presentation of the ideles of a finite Galois extension is canonically equivalent to the ordinary restricted-product presentation. This file descends that equivalence through principal ideles and ident…

The relative idele group carries the determinant norm. The scalar-extension equivalence with the ordinary ideles of the extension field transports that existing norm to the usual map N{L/K} : IL → IK.

The ordinary idele norm is transported from the determinant norm on the relative idele group. At each place, the canonical local tensor decomposition identifies that determinant with the product of the ordinary field nor…

For an infinite place W of an extension field, a unit of the completion at the place below W can be extended to W and inserted as a one-place idele. Its ordinary idele norm remains supported at the place below W; the sur…

For a finite place v of K, evaluation on the finite-adele coordinate is a K-algebra homomorphism 𝔸K → Kv. Scalar extension along L/K therefore gives the actual local component map 𝔸K ⊗[K] L → Kv ⊗[K] L. This is the map n…

The local algebra at a place of the base field is a finite product of the completions above it. This file proves that the determinant norm on a finite product is the product of the norms of its factors. The last theorem…

For a finite extension of number fields and a place upstairs, the order of the concrete local field norm is the inertia degree times the upstairs order. The proof uses the actual norm–valuation theorem for finite separab…

In the tensor-product presentation 𝔸L = 𝔸K ⊗K L, the idele norm is the determinant norm of a finite free algebra. Thus transitivity is the general transitivity theorem for determinant norms. The remaining statements reco…

For a finite place v of an extension field, embed a unit of the completion at the place below v into the completion at v, and support it only at v. Its ordinary idele norm is supported only at the place below v; the surv…

The algebraic equivalence from finite idèles to units of the finite adele ring is continuous for the restricted-product topology on idèles and the graph topology on units. Both the value and inverse-value maps are induce…

This file defines the idele supported at one finite place with normalized local order one, and computes its associated fractional ideal and ideal class. These constructions are independent of class field theory.

This file formalizes the ideal map from ideles. Its construction is explicit: local discrete valuations form a finitely supported integer vector, and unique factorization of fractional ideals identifies that vector with…

This module packages the connected component of the identity in the idele class group as a closed normal subgroup and names the corresponding quotient.

The topology on the finite ideles is the restricted-product topology from AlgebraicNumberTheory.Idele.Topology. We prove local compactness by showing that every finite completion is proper, that its integral unit group i…

This module exposes the absolute norm on the idele group and assembles compatible local determinant-norm preimages into a global relative idele.

For a finite Galois extension L / K and a finite set S of finite places of K, this file chooses an actual extension of every v ∈ S, forms the corresponding algebraic localization Lw / Kv, and transports its local norm su…

This file supplies the archimedean source used in the norm-approximation argument. At a real place the positive units have an n-th root, while at a complex place every unit has one. Consequently the standard positive sub…

This file constructs the homomorphism 𝓝 : IK → ℝ₊ˣ. At a finite place a uniformizer contributes the norm of its prime ideal; at infinity we divide by the normalized archimedean norm. This is the convention for which prin…

This module combines local compactness, the logarithmic unit lattice, and the principal-idele norm formula to prove compactness of the norm-one subgroup of the idele class group.

The positive archimedean norm, and consequently the absolute idele norm, is preserved by the ordinary norm in a finite number-field extension.

The norm on ideles in a finite number-field extension is continuous. The proof works first on the open chart with integral finite components and then uses the topological-group structure to obtain continuity everywhere.

Scalar extension raises the finite, archimedean, and absolute idele norms to the degree of the number-field extension. The rational relative-idele base-change realization is included as the endpoint used by cyclotomic re…

This file relates the finite components of the ordinary idele norm to local orders and positive prime norms. It also proves the degree formula for the finite positive norm under scalar extension.

The ordinary idele-class norm preserves the absolute norm and restricts to the norm-one idele-class subgroups.

The ordinary idele norm restricts to a homomorphism between the actual norm-one idele subgroups.

This module constructs an idele supported at one infinite place whose absolute norm is a prescribed inverse. Its finite components are trivial and all of its infinite components lie in the standard positive subgroups.

This module exposes the diagonal embedding and idele class group, identifies field units with principal relative ideles, and transports low-degree Tate cohomology across that identification.

This file formalizes the diagonal embedding of Kˣ into the idele group and the resulting idele class group.

This file proves that the absolute idele norm is trivial on the diagonal copy of Kˣ, and hence descends to the idele class group.

This file proves that the principal ideles form a discrete, and hence closed, subgroup of the idele group. The proof uses the same arithmetic separation as the classical argument. The finite-place condition forces a prin…

If a finite local component is both a determinant norm and a local integer unit, its determinant-norm preimage can be chosen integral in every factor of the canonical local tensor decomposition. This is the local restric…

This file specializes the local tensor norm calculation to a height-one prime of a number field. The canonical comparison (K, |·|v)^∧ ≃ Kv identifies the determinant norm on (K, |·|v)^∧ ⊗[K] L with the determinant norm o…

For a finite Galois extension L / K, the determinant-norm image on Kv ⊗[K] L is the field-norm subgroup of any completion of L above the infinite place v. This is the archimedean counterpart of the finite-place tensor-no…

This file packages a restricted-product assertion for relative ideles. At every finite place outside a finite set, a relative idele belongs to the actual product of valuation-ring unit groups supplied by the completion d…

This file supplies the finite-support input for the actual scalar-extension model 𝔸K ⊗[K] L. Fixing the canonical chosen K-basis of L, every relative adele has finitely many base-adele coefficients. For a relative idele…

For the cofinite restricted product, Mathlib's algebraic unitsEquiv is a topological group equivalence when each distinguished local submonoid is open. The units on the left carry their graph topology; the right side has…

This file formalizes finite-support objects for ideles and units. Since every archimedean place is always included, a finite set S below records only its finite places.

Local-to-global diagrams use the canonical embedding of a local multiplicative group into the idele group. This file constructs that embedding at finite places and the corresponding one-component relative idele.

Finiteness of the ordinary ideal class group lets us choose one idele representing each ideal class. The union of the (finite) supports of those representatives is a finite set S for which IK = IK^S Kˣ.

The idele group IK carries the restricted-product topology. This file records the topological-group structure and the continuity of every local component map.

This file places the normal-closure construction used throughout the global theory below the adelic and splitting developments that consume it. The closure is formed inside mathlib's fixed algebraic closure, and the orig…

The Galois orbit of the centre of one actual extended finite place is free when the rational prime splits completely. Its prime ideals form a finite set of cardinality equal to the number-field degree.

Unramified degree-one primes in a finite Galois number field give complete splitting above the canonical rational finite place. Such primes exist outside any specified finite set.

A finite Galois number field admits completely split rational primes congruent to one modulo four and outside any specified finite set. The construction passes through an extension containing a square root of minus one.

Good prime divisors of primitive polynomial values give prime ideals of residue degree one. Every number field admits an unramified degree-one prime outside any specified finite set of rational primes.

This file combines finite-prime and infinite-place unramifiedness and records its tower and intermediate-field properties.

This file transports finite-place unramifiedness across an equivalence of top fields and connects the number-theoretic predicate to the commutative-algebra notions of formal unramifiedness and étaleness for rings of inte…

This file records the tower properties of being unramified at every finite prime. The transitivity and intermediate-field arguments are proved from multiplicativity of ramification indices.

The local factor P^e of q times the integer ring has absolute norm q^(ef). The Galois fundamental identity makes ef a divisor of the extension degree, so it is prime to q. The literal CRT trace witness then proves that P…

Every number field has an integral primitive element. Its order has full integer rank, so its additive index is nonzero and lies in its conductor. Consequently the exponent used in Kummer--Dedekind is nonzero.

The implementation quantifies over primes of the extension, while the public definition quantifies over primes of the base. These are equivalent because every prime above a nonzero base prime is itself nonzero.

A field equivalence bijects both the finite and infinite places. These equivalences reindex placewise products without changing their mathematics.

A nonconstant integer polynomial has a nonzero value A. On any progression through that argument with step A times the product P of forbidden primes, its values have shape A (1 + Pb). Finite fibres allow a value differen…

A number field has finite dimension over the countable field ℚ, so its underlying type has a representative in the lowest universe. The ring equivalence to that representative preserves the number-field structure.

Every prime factor of the different lies above a rational divisor of the discriminant. The CRT trace bound controls its exponent by the exponent in the corresponding rational prime ideal. Hence the different divides (c),…

For a coprime factorization of q times the integer ring, the Chinese remainder idempotent (1, 0) has trace equal to the dimension of the first factor. If that factor has norm q^m and q does not divide m, its trace is non…

For a finite field k of cardinality q and n ∣ q - 1, the tame power-residue symbol is u ↦ u ^ ((q - 1) / n). Its kernel is exactly the subgroup of n-th powers.

Let K contain the n-th roots of unity and let P be a prime ideal whose absolute norm is coprime to n. Reduction identifies μₙ(𝓞 K) with μₙ(𝓞 K / P). Pulling the finite-field symbol back along this identification gives (a…

This file proves Gauss reciprocity and its supplementary laws. Mathlib's Jacobi symbol has a natural-number denominator, so an integer denominator b is written canonically as jacobiSym a b.natAbs, as is forced by the pri…

Public aggregate for finite ramification support, rational prime ideals, everywhere-unramified rational extensions, and global degree bounds.

This combines three generic steps in the global degree estimate: coverage by one prime over each member of S, generation of the full Galois group by all finite-prime inertia, and the finite abelian product bound.

Once the chosen inertia groups generate the full abelian Galois group and their orders satisfy the local prime-power bounds, the global degree is at most the totient of the conductor candidate. This file isolates that fi…

In a finite separable extension of Dedekind domains, only finitely many height-one primes of either the extension ring or the base ring ramify.

This file identifies the height-one ideal of ℤ attached to a positive rational prime with its usual principal ideal.

For a finite Galois extension of number fields L / K, this file attaches an actual decomposition subgroup to every finite place of K. The extension of the adic absolute value is the one constructed in LocalNormApproximat…

For a finite Galois extension of number fields, an exact extension of a normalized finite absolute value and its centre prime ideal have the same decomposition group. This file makes that comparison independent of the ch…

This file formalizes the normal-closure reduction for complete splitting. For a finite Galois extension M / K, an intermediate field L, a nontrivial absolute value v of K, and an extension w to M, put G = Gal(M / K), H =…

This file formalizes a prime-order fixed-field reduction. From a nontrivial finite Galois extension L / K we choose an automorphism σ of prime order p and form K' = L ^ ⟨σ⟩. The extension L / K' is an actual cyclic Galoi…

The global Kronecker--Weber argument forms a fixed field which is unramified at every finite prime. Minkowski's discriminant bound to show that this field is ℚ. This file records that source theorem directly in terms of…

Public aggregate for approximation, congruence subgroups, and ray class groups of number fields.

This file extracts the simultaneous approximation statement needed for ray class groups. At finitely many finite places one may prescribe an arbitrary open multiplicative coset and move a given idele into all of those co…

This file contains the finite local data used by ray congruence subgroups. A full modulus, including a selected set of real places, is defined in AlgebraicNumberTheory.RayClass.FullModulus.

A ray modulus consists of a finite modulus together with the real places at which positivity is imposed. This file defines the corresponding idèle and idèle-class congruence subgroups without fixing an archimedean conven…

This file defines the subgroup of fractional ideals prime to a modulus, connects it with the corresponding finite-idele higher-unit conditions, and develops the approximation maps used in ray-class ideal constructions.

For a finite extension L / K, the norm of a prime of L above v is v raised to the inertia degree. Extending this rule multiplicatively gives the genuine norm on nonzero fractional ideals. If m is a modulus of K, a modulu…

This file records the one-place higher-unit subgroups used to compare ray-class moduli with local conductors. The constructions are idele- and ray-class data and do not depend on the existence of a global class field.

This file proves the exact sequence from global unit signs through the narrow and ordinary class groups.

The ray modulus with zero finite part and no real conditions gives precisely the ordinary ideal class group. The equivalence below also identifies their finite-prime classes.

The fractional ideals prime to a modulus are generated by their prime ideals away from the modulus. This is the algebraic input for comparing Frobenius-normalized ray reciprocity maps.

The reader-facing higher-unit group agrees with the group used in the existing ray-class and idelic implementation. Keep this definitional comparison at the boundary between the two APIs.

This file computes ray class groups of the rational numbers. A positive integer m determines a full narrow ray modulus: its finite part has exponent m.factorization p at p, and its real place imposes positivity. The posi…

The local higher-unit groups are open, the ray congruence subgroups are open (and hence closed) of finite index, and the congruence subgroups are cofinal among the closed finite-index subgroups of the idele class group.

Public aggregate for the rank and logarithmic-lattice theory of S-units.

This file supplies the equivariant input for the S-unit calculation. A Galois automorphism acts on finite places through its restriction to the ring of integers, on infinite places by precomposition, and on field units i…

This file computes the Herbrand quotient of the global S-unit group. It connects the actual S-unit group to its logarithmic lattice, adds the invariant diagonal integer direction, and combines the resulting exact sequenc…

This file develops the logarithmic lattice of S-units. The finite set S consists of the finite places; all infinite places are understood to belong to the set of places used in the theorem. The first construction uses th…

This file supplies the algebraic rank and torsion input for S-units. The finite set S contains the finite places; all infinite places are understood to be present.

This file provides the common realization of a separable extension inside the chosen separable closure of its base field.

The roots-of-unity descent uses the following concrete fact. If finite field extensions M / K and L / K have coprime degrees, then M ⊗[K] L is a field. If L / K is Galois, the resulting extension over M is Galois of the…

Local and global class field theory, including reciprocity laws, the class field axiom, Hasse–Arf and Kronecker–Weber. Supporting constructions cover idèles, Kummer theory and Lubin–Tate theory.

Reader-facing vocabulary used by the headline theorem modules. Primitive leaves import Mathlib only; derived leaves import only the prerequisite definition leaves. Topic-level All modules and this root module are aggrega…

This aggregate collects conductor and modulus conditions, ray class groups and realizations, ideal norms, and ray Artin maps.

The norm sends a finite-prime factor upstairs to the prime below it, with exponent multiplied by the inertia degree. Prime factorization extends this rule to a multiplicative map on all nonzero fractional ideals.

A finite prime of an extension contracts to a finite prime of the base. The norm sends its exponent to the prime below, multiplied by the inertia degree. The resulting map on finitely supported exponent vectors is additi…

The narrow class group is the group of nonzero fractional ideals modulo principal ideals generated by elements positive at every real place. This ideal-theoretic definition does not depend on the ray class group.

Enlarging a modulus strengthens its finite congruences and real positivity conditions. The induced inclusions of prime-to-modulus ideals and ray-principal ideals give the canonical quotient map from the larger modulus to…

The domain consists of fractional ideals of L with zero valuation at every prime lying above the finite support of m. The relative ideal norm maps this group into the fractional ideals of K prime to m; composing with the…

A modulus consists of finite-prime exponents and a finite set of real places.

The prescribed subgroup is identified with the Artin kernel before applying the first isomorphism theorem.

This aggregate collects arithmetic Frobenius, splitting and unramified place conditions, Hilbert class fields, and fractional ideals of number fields.

Mathlib's FractionalIdeal.count and unique-factorization theorems identify the multiplicative group of nonzero fractional ideals with the finitely supported integer exponents of finite primes. This equivalence is formula…

This module collects the reader-facing finite and topological vocabulary. It imports definitions only; assertions are in the corresponding Theorems module.

This module packages finite abelian extensions inside Mathlib's chosen separable closure. It contains no class-field-theory implementation.

The interface is ideal-theoretic: a ray-class Artin map is normalized by arithmetic Frobenius away from its modulus.

This is the specific isomorphism induced by the Artin map in FiniteAbelianReciprocityData, not an arbitrarily chosen isomorphism.

The local algebra of L / K at a finite place v is Kv ⊗[K] L. Its determinant norm on units defines a subgroup of Kvˣ. This definition retains the whole tensor algebra, including all factors above v; it does not choose a…

For a number field K, Mathlib's idèle class group is the unit group of the adele ring modulo principal idèles. Its quotient by the connected component of 1 is the group appearing in topological global reciprocity.

This predicate records surjectivity and kernel equal to the identity component of the idèle class group. These properties alone do not determine the normalized Artin map: finite-level Frobenius compatibility is a separat…

This aggregate collects lower and upper ramification groups and jumps, Herbrand functions, and inverse Herbrand functions.

Between consecutive nonnegative integers, the function interpolates linearly between the rational Herbrand values. On the negative half-line it is the identity. Its slope on (m, m + 1) is |G(m+1)| / |G0|.

The defining choice is verified to be a two-sided inverse for finite Abelian local extensions in the theorem layer.

The right-limit group is the supremum of upper groups at strictly larger indices. A jump occurs exactly when that right limit differs from the group at the index itself.

The ideal exponent at a real index s is max(0, ceil(s + 1)). Consequently, indices at or below -1 give the whole decomposition group, and natural indices recover the usual m^(n+1) displacement condition.

The upper group at t is the public real lower group at the inverse Herbrand index ψ(t).

This aggregate collects local and global Hilbert pairings and their laws, Kummer algebras and norm subgroups, and power classes.

This set depends on the two nonzero global arguments and the exponent. A finite place is excluded exactly when all three have valuation one there.

This is the image of the determinant norm on units of K[X] / (X^n - a). The algebra need not be a field, so this subgroup is defined without any irreducibility assumption on the polynomial.

This aggregate collects field norm maps, subgroups and quotients, finite abelian local extensions, open subgroups of finite index, and topological profinite completions.

This module defines the profinite completion of a topological group using its open finite-index normal subgroups. The construction records the topology on the source group, unlike the abstract profinite completion by all…

This aggregate collects extending absolute values and norm conditions at finite places, infinite places, and every place.

This index type uses only Mathlib's absolute values and algebra map. Its elements are precisely the absolute values on L extending v on K.

This aggregate imports the implementation modules for global Artin reciprocity, the class-field correspondence, Hilbert and power-residue reciprocity, ideal Artin maps, decomposition, and principalization. Reader-facing…

This aggregate exports the cyclic idele-class norm-index calculation, the Hasse norm principle, and the rational idele-class formation.

This file proves the cyclic idele-class norm-index formula. The first input is the H⁻¹ calculation for the principal-idele term in 1 → Lˣ → IL → CL → 1. For a cyclic extension this term vanishes by Hilbert 90. The result…

This file proves the Hasse norm principle on the actual idele and field norm maps. The local condition is expressed canonically: at a place v it is the image of the determinant norm on Kv ⊗[K] L. At finite places this is…

This module identifies the fixed-field idele-class representation with concrete relative idele class groups and transfers the cyclic low-degree Tate cohomology calculation to prove the abstract class-field axiom.

This aggregate preserves the public import path while the implementation is organized by the mathematical stages of the norm-index argument.

This file defines the concrete idele-class subgroup attached to local power conditions and computes its archimedean local indices.

This module installs the complete discrete valuation, characteristic-zero, and finite residue-field structures used by finite-place class-field arithmetic.

This file supplies the completion instances and local cardinality formulas used to evaluate finite-place factors in idele power quotients.

This file relates global ideal norms to the residue fields and ramification invariants of the corresponding finite completions.

This file proves that the concrete local-condition subgroup lies in the global idele norm range, and descends that inclusion to idele classes.

This file combines the supported local index, principal-ideles exact sequence, and norm containment to prove the prime-power Kummer norm-index theorem.

This file expresses the supported idele quotient as the product of its local archimedean and finite-place power indices and evaluates its cardinality.

This file identifies supported principal ideles with the corresponding S-unit group and derives the exact-sequence cardinal identities.

This module packages the finite-place local norm conditions and proves the global norm containment and principal-intersection identity used in the idele-class norm-index argument.

This module defines the subgroup of ideles that are local powers at selected places and integral units elsewhere, together with its intersection with principal ideles and the corresponding subgroup of S-unit powers.

This module proves that local powers, and then the concrete simple-Kummer power subgroup, lie in the norm subgroup at a chosen finite place.

This module translates the idele-theoretic implementation of the cyclic Hasse norm theorem into the implementation-independent predicates in ClassFieldTheory.Definitions.NormTheorems.

This aggregate module exposes the restriction-kernel construction, prime selection, decomposition-field identifications, and the final local-power kernel theorem.

This file constructs infinite full-decomposition candidate sets and chooses pairwise distinct base places outside the finite avoidance set. Distinctness is obtained from Mathlib's Hall marriage theorem.

This file proves that the selected local power conditions cut out exactly the finite Kummer radical and records the support-enlargement consequence used by the global reciprocity argument.

This file lifts the chosen base places to coordinate places in the full Kummer extension and proves the required decomposition and unramifiedness properties.

This file identifies the chosen decomposition groups with the cyclic coordinate subgroups, proves complete splitting in the prescribed extension, and identifies the associated decomposition fields.

This file relates relative and absolute finite-place decomposition groups and proves cyclicity for the decomposition group at a chosen unramified place. The results are independent of the S-unit Kummer construction.

This file packages the chosen base places as a finite set and proves its cardinality and disjointness properties.

This file specializes the chosen restriction-kernel coordinates of an enlarged S-unit Kummer extension to coordinate generators, their required number, and their cyclic fixed fields.

This module constructs the localization map from an S-unit group to the finite product of local unit power classes and proves its kernel and surjectivity properties for the Kummer prime set.

This module restricts the power-local-unit subgroup to ideles supported at the prescribed finite places and identifies the resulting quotient with the product of its archimedean and finite local power-class groups.

For a finite extension of number fields L / K, if all but finitely many finite places of K split completely in L, then L / K has degree one. The normal-closure and splitting-transport constructions used in the proof live…

This file proves the infinitude of full-decomposition places in cyclic prime-power extensions. For a cyclic group of prime-power order, every proper subgroup is contained in the chosen subgroup of index p. Consequently e…

This file joins the unrestricted local calculation, the vanishing of the unramified integral factors outside the support, and the exact sequence from S-units to supported ideles and idele classes.

For a finite abelian extension, the modulus constructed from the actual chosen local norm groups has support exactly the ramified finite places. At the archimedean places, the determinant-norm image is the whole local mu…

For a finite abelian extension, the modulus constructed from the actual local norm groups is zero exactly when every chosen finite completion is unramified. Its support therefore gives the exact chosen-completion ramific…

At a finite place, the absolute-value completion used by local class field theory is canonically equivalent to the adic completion used by the idèle and ray-class libraries. This file proves that the equivalence identifi…

For a finite abelian extension of number fields, the selected local higher-unit exponent of the actual idèle-class norm subgroup vanishes exactly at the finite places where the chosen completed extension is unramified. T…

This public root exports the finite abelian class-field correspondence for closed finite-index idèle-class subgroups, exact conductor and ramification theory, and the actual big and small Hilbert class fields with their…

For a closed finite-index subgroup H ≤ CK, the selected actual class field has norm range exactly H. This module records the canonical arithmetic reciprocity homeomorphism Gal(L/K) ≃ₜ CK/H, so both the field and the topo…

The canonical ideal-theoretic Artin map uses arithmetic Frobenius. Accordingly, these equivalences use arithmetic global reciprocity before identifying the intrinsic Hilbert norm quotient with the narrow or ordinary idea…

This is the canonical topological isomorphism Gal(Kᵐ/K) ≃ₜ CK/CKᵐ with arithmetic Frobenius normalization. It uses the actual selected ray class field, its exact idèle norm range, the finite Krull topology, and the nativ…

The pre-existing local class-formation coordinate has geometric Frobenius normalization. This file supplies the canonical prime Artin element used in the ideal-theoretic formulation: the ordinary normalized prime idèle m…

The big Hilbert class field is the ray class field of modulus one (the zero finite modulus in the exponent-valued representation). This file identifies its defining norm quotient with the narrow class group. The maximal-…

The maximal finite-prime-unramified abelian extension has the same idèle-class norm subgroup as the selected big Hilbert class field. Arithmetic global reciprocity therefore gives its narrow-class-group Artin isomorphism…

An equivalence of number fields preserves both finite integrality and positivity at the real infinite places. Consequently the actual idele-class transport carries the big-Hilbert norm subgroup exactly onto the correspon…

The selected big Hilbert class field is constructed over a canonical fixed-field copy of the input number field. The canonical equivalence with the original field supplies the actual scalar map used here. Thus the select…

A finite abelian subextension in the abstract class-formation lattice is represented by two nested closed subgroups of an ambient Galois group. Its upper relative fixed field is an actual finite extension of the lower fi…

This leaf fixes the finite Galois norm neighbourhood, abstract subextension, and canonical fixed-field presentation attached to a closed finite-index idèle-class subgroup. Norm-range and reciprocity statements live in la…

This leaf compares the selected abstract norm subgroup with the actual idèle-class norm range over the canonical fixed-field base.

This leaf installs the original-field algebra tower and transports the canonical norm-range computation back to the original idèle class group.

This facade exports the underlying multiplicative equivalence of the already compiled topological reciprocity provider and its evaluation formula.

The algebraic equivalence is obtained by forgetting topology from the named continuous provider. This avoids a second specialization of the full finite global reciprocity instance tower.

Since the algebraic equivalence is definitionally the underlying multiplicative equivalence of the continuous provider, its evaluation theorem is inherited without reconstructing the selected class-field instance tower.

This facade exports the degree formula and the topological and algebraic reciprocity equivalences after their command-sized leaves have elaborated. Keeping the expensive equivalence constructions in separate compiled lea…

This leaf derives the degree of the selected class field from its exact idèle-class norm range.

This leaf proves that the selected class-field reciprocity equivalence sends the global norm-residue symbol to the corresponding quotient class.

This facade exports the generic norm-range transport, the continuous reciprocity composite, and its evaluation law.

The final equivalence composes finite global reciprocity with the generic continuous transport induced by the exact norm-range equality. Equality elimination preserves the native quotient topology, so no discrete topolog…

The public theorem uses the named reducible value provider and specializes the generic transported-reciprocity calculation.

This theorem works for an arbitrary finite abelian extension and subgroup equality. It proves the composition formula once without unfolding a domain-specific selected-field construction.

The expanded inverse norm-residue expression is kept behind one reducible value provider. Public evaluation statements can therefore mention the selected class-field instance tower once while remaining definitionally equ…

Equality of normal subgroups identifies their quotient groups with the same native quotient topology. Eliminating the equality therefore gives the continuous multiplicative equivalence directly; no discrete-topology inst…

This file constructs the finite part of the conductor in the convention where every real place has the positive ray condition. It is therefore a narrow finite conductor, not yet the full global conductor of an arbitrary…

The one-place idèle of normalized order one defines two compatible prime classes: one in the ray class group at the exact narrow finite norm conductor, and one in the actual idele-class norm quotient. The canonical narro…

This file gives the one-place archimedean step toward the full conductor. Removing the positivity condition at a real place preserves the defining property exactly when the whole one-place idèle-class image is already co…

Increasing a modulus decreases its ray congruence subgroup. This contravariance makes the narrow finite conductor of an intersection of norm subgroups the pointwise maximum of their narrow finite conductors. Under class-…

The narrow finite conductor is the finite component of the conductor in the all-real-positive convention. We formulate its local condition directly inside the idele class group: insert a higher unit at one finite place a…

For a conductorial idèle-class subgroup H, a normalized one-place prime idèle determines compatible classes in the ray class group at H.narrowFiniteConductor, in CK / H, and—away from that finite conductor—in the ideal A…

For a conductorial subgroup H of the idèle class group, the ray class group at its exact narrow finite conductor maps canonically onto CK / H. This file characterizes injectivity of that map by equality of the two finite…

There are two source statements in the ramification criterion: a prime belongs to the support of the narrow finite conductor exactly when its one-place finite local conductor exponent is nonzero; a finite abelian local e…

Two finite cyclic extensions whose exact narrow finite conductors agree and whose degrees exhaust the corresponding ray class number determine the same actual idèle-class norm subgroup. Thus their concrete norm quotients…

For a finite cyclic extension, the actual idele-class norm quotient has order equal to the extension degree. Substituting this norm-index theorem into the narrow finite conductor ray-class factorization identifies the ra…

For a tower of cyclic Galois extensions, the first map in the concrete idele-class norm-quotient sequence is injective. Together with the already available right exactness, this gives the short exact norm sequence and it…

For a finite cyclic extension, the actual idèle-class norm quotient has order equal to the extension degree. The ray class group at the exact narrow finite conductor surjects onto this norm quotient. This file identifies…

This file implements the roots-of-unity descent in the existence proof of global class field theory. Starting from a finite seed of finite places of K, it enlarges the seed just enough that its full inverse image in Cycl…

An embedding of an actual finite abelian extension into the rational separable closure determines a finite abelian subextension of the fixing subgroup of the embedded base field. This file also allows that base fixing su…

For actual finite abelian extensions of a number field, containment is exactly reverse containment of their genuine idèle-class norm ranges. The proof first realizes an arbitrary extension in the same rational separable…

The abstract finite abelian classification is formulated on the fixed parts of the rational absolute idele-class representation. For a finite abstract base field, the canonical fixed-field comparison transports its norm…

The ordinary norm subgroup attached to a finite abelian subextension is the genuine determinant-norm range on its canonical actual fixed fields. Consequently it is open and closed in the ordinary idele-class topology and…

For a closed finite-index subgroup H of the idele class group, the canonical ray modulus inside H supplies the finite seed for the full S-unit Kummer construction. When H is proper, the Kummer exponent is the index of H;…

For a finite abelian extension of number fields, the chosen local Artin homomorphism has image equal to the actual decomposition group and kernel equal to the chosen local norm subgroup. Restricting its codomain and appl…

This module identifies the full conductor of a finite abelian extension as the least modulus of a selected ray class field into which the extension embeds. The proof combines the ray-field embedding criterion with the mi…

This file identifies the canonical transition from the big-Hilbert reciprocity quotient to the small-Hilbert reciprocity quotient with the canonical map from the narrow class group to the ordinary class group. It then tr…

The selected big Hilbert class field is characterized here in actual field order. Its abstract norm subgroup in the rational absolute idele-class formation is identified exactly with the intrinsic big-Hilbert subgroup of…

An unramified cyclic extension reaches the big or small Hilbert norm subgroup exactly when its degree reaches the corresponding narrow or ordinary class number. Thus a maximal-degree unramified cyclic extension has the c…

Suppose a cyclic extension is unramified at every finite and infinite place and its degree is the ordinary class number. Its actual idèle-class norm quotient is then the small-Hilbert reciprocity quotient. This file tran…

The big and small Hilbert norm subgroups are closed and have finite index. The finite-index class-field construction therefore supplies genuine finite abelian subextensions of the rational separable closure. This file fi…

This compatibility facade exports the generic transport core and the independently compiled big/small, realized-base/original-base reciprocity specializations.

This leaf specializes the shared reciprocity transport to the actual base field of the selected big Hilbert class field.

The original-base specialization is compiled separately from the realized-base specialization and reuses the shared reciprocity transport provider.

This leaf specializes the shared reciprocity transport to the actual base field of the selected small Hilbert class field.

The original-base specialization is compiled separately from the realized-base specialization and reuses the shared reciprocity transport provider.

The quotient transport and its norm-residue evaluation are compiled once in this leaf. Big/small and actual/original Hilbert reciprocity specializations reuse the named data provider without rebuilding the generic recipr…

The selected big and small Hilbert class fields have the prescribed idele-class norm ranges. Exact local--global narrow finite conductor compatibility therefore turns the vanishing of their intrinsic finite conductors in…

For a finite Galois extension with no ramified finite prime, the actual idele-class narrow finite conductor is zero. Consequently its norm subgroup contains the big-Hilbert norm subgroup. This is the norm-subgroup form o…

Maximal abelian reciprocity transports closed subgroups of the idele-class component quotient to closed subgroups of the maximal abelian Galois group. Composing this transport with the infinite Galois correspondence give…

For a finite extension L / K, the norm of a local n-th power is again an n-th power. At a finite place outside a prescribed support, the norm of an integral unit is an integral unit. Combining these statements over all p…

This module supplies the implementation proofs for the compact public statements in ClassFieldTheory.Theorems.FrobeniusAndHilbertClassFields. The prime element exposed below is the arithmetic-normalized prime Artin eleme…

This is the implementation layer for the reader-facing global CFT module. It collects the existing finite reciprocity, maximal abelian reciprocity, class-field existence, and infinite correspondence modules without addin…

For a finite Galois extension of number fields, the image of the idele-class norm contains an explicitly constructed ray congruence subgroup. At a ramified finite place we choose a sufficiently deep higher-unit group ins…

For an arbitrary finite extension L / K, let N be its chosen finite normal closure, let E be the distinguished copy of L in N, and let A be the largest abelian Galois intermediate field contained in E. This file proves N…

For every finite Galois extension, the ray class group at the exact narrow finite conductor surjects onto the actual idèle-class norm quotient. This file characterizes when that presentation has no residual kernel: the n…

For a finite tower K ⊂ M ⊂ L, norm transitivity places the actual idele-class norms from L inside those from M. This produces the canonical quotient transition CK / N{L/K} CL → CK / N{M/K} CM. The transition is surjectiv…

An actual finite Galois norm subgroup contained in an ordinary idele-class subgroup makes the transported subgroup norm-open in the rational absolute class formation. Finite abelian classification then constructs its cla…

Let H be a closed finite-index subgroup of the idele class group and let n = [CK : H]. Every n-th power belongs to H. If a finite set of finite places contains the support of a congruence subgroup lying in H, the ideles…

The public finite ray-class Artin map is normalized on all primes away from its modulus. Frobenius rigidity identifies its kernel with the genuine idèle-class norm kernel. We then compare that kernel with the established…

The forward inclusion of the ideal-theoretic norm-kernel formula follows prime by prime. The reverse inclusion needs a separate approximation argument and is not asserted here.

The source ideal norm is defined before quotienting by principal ray ideals. The public ideal-norm image is its image in the ideal ray class group. This file records the exact comparison, including the principal-ray kern…

This module supplies the implementation proofs for the compact conductor and ray-class-field statements in the parent Theorems directory.

For a prime q away from a rational modulus (m), the normalized one-place prime idèle represents the direct residue unit q in (ZMod m)ˣ. This is the ideal-theoretic arithmetic input needed to compare rational ray reciproc…

For a modulus m of a number field K, its ray congruence subgroup CK^m is closed and has finite index. The finite-index class-field construction therefore selects an actual finite abelian extension whose determinant-norm…

The idèle-class quotient gives the canonical map from a larger ray modulus to a smaller one. The public ray-class groups use the comparison equivalence to transport this map.

A normalized one-place prime idèle is prime to every modulus whose finite support omits that prime. Its fractional ideal is the corresponding prime ideal, so the idelic and ideal-theoretic ray-class constructions use exa…

The selected field of a larger ray-class subgroup is contained in that of a smaller subgroup, as actual subfields of the fixed separable closure.

Arithmetic reciprocity on a ray-class fixed field agrees, at each ordinary prime idèle, with the arithmetic global Artin symbol of that field.

An isomorphism from a ray class group to the Galois group of a finite abelian extension which sends every prime class to its genuine arithmetic Artin symbol forces the ray modulus to be defining for that extension. The p…

Prime idèle classes away from a modulus determine homomorphisms out of the ray class group. This follows from factorization of prime-to-modulus fractional ideals and the idelic-to-ideal ray-class equivalence.

Starting from a prescribed finite set of finite places, we enlarge it by a fixed idelic support and by a chosen support of the exponent. For this enlarged set, a principal idele satisfies the local power conditions exact…

When the base field contains the required roots of unity, the full S-unit Kummer extension realizes the canonical power-local-unit subgroup exactly as its ordinary idele-class norm subgroup. The forward inclusion is the…

The small Hilbert class field corresponds to the image in the idele class group of the ideles integral at every finite place. Its reciprocity quotient is canonically the ordinary ideal class group; consequently its order…

The intrinsic small Hilbert class field is unique up to a base-field equivalence. Therefore its actual idèle-class norm subgroup is the same as that of the selected class field. Arithmetic global reciprocity then gives t…

The selected small Hilbert class field is characterized in actual field order. Its rational absolute class-formation norm subgroup is exactly the intrinsic small-Hilbert subgroup of its fixed-field base. The order-revers…

An equivalence of number fields carries the small-Hilbert norm subgroup exactly onto the small-Hilbert norm subgroup. Consequently it induces the canonical equivalence of the corresponding reciprocity quotients. Transpor…

The finite class-field construction realizes the small Hilbert class field over a canonical fixed-field copy of the input number field. The fixed-field copy is canonically ℚ-algebra equivalent to the original field. This…

For a finite Galois extension which is unramified at both finite and infinite places, every idele integral at all finite places is an actual relative-idele norm. It follows that the actual idele-class norm range contains…

For a finite abelian extension of number fields, the global Artin image of the normalized one-place prime idèle is the chosen local Artin image of an element of normalized order one. At a chosen unramified finite place,…

For a finite abelian extension of number fields, the normalized order-one element at a finite place defines a class in the chosen local norm quotient. Under local reciprocity this class is the actual prime Artin element…

The Galois correspondence realizes a subgroup S ≤ Gal(M / K) as an intermediate field. The transfer construction independently realizes Gal(M / M^S) as a subgroup of Gal(M / K). The first theorem below identifies these t…

This public root exports ideal Artin maps and quotients, Frobenius classes, splitting in the small Hilbert class field, the genuine idèle-extension transfer square, and principalization of every integral and fractional i…

For a defining modulus of a genuine finite abelian class field, this module composes the ideal ray-class quotient with the topological arithmetic global norm-residue equivalence. The resulting map sends an ordinary prime…

This module states the order calculation in the unramified decomposition law with arithmetic Frobenius normalization. The underlying ideal-class quotient is unchanged by inversion of the reciprocity map, while the image…

Let N ≤ CK be a class-field norm subgroup and let m be a defining modulus, so CK^m ≤ N. The idelic quotient map then factors through the ideal ray class group. Composing with the projection from ideals prime to m gives t…

For a defining modulus m, the ideal-theoretic Artin map is surjective and has kernel Hm. The first isomorphism theorem therefore identifies JK^m / Hm with the corresponding idelic norm quotient CK / N.

This file identifies the ideal Artin symbol of a prime with the genuine global and local Frobenius automorphism. For an unramified prime it then combines this identification with the Dedekind-domain fundamental identity…

This file records the ideal-class-field ingredient of the decomposition law. A prime outside a defining modulus gives an element of the ideal Artin quotient, and the first isomorphism theorem preserves its order. The gen…

For a finite abelian extension L / K and a defining modulus m, the genuine ideal group N{L/K} JL^m PK^m is RayClass.idealNormSubgroup. This module identifies it with the kernel of the arithmetic ideal Artin map, descends…

For a finite extension L / K, norm limitation identifies its idèle-class norm range with that of the maximal abelian subfield in the chosen finite normal closure. This leaf transports that equality to the corresponding i…

This leaf proves the packaged statement using the idèle-class norm-range equality and the finite-extension ideal Artin kernel theorem.

This leaf packages the ideal norm-limitation equality behind a named proposition. Keeping the expanded normal-closure expression out of later declaration signatures avoids repeatedly normalizing the full finite tower.

This file descends genuine idele extension to the reciprocity quotients defining the two small Hilbert class fields and proves that the resulting map forms the naturality square with the existing ideal-class extension Cl…

The principal ideal theorem uses two successive finite abelian class fields. The upper field is Galois over the original base once its absolute Galois subgroup is stable under conjugation by the base subgroup. This file…

At the generic level, the Galois correspondence realizes a subgroup S ≤ Gal(M / K) as an intermediate field, while the transfer construction independently realizes Gal(M / M^S) inside Gal(M / K). Identifying these subgro…

Compatibility of abstract extension with ordinary idele classes.

This compatibility facade exports the fixed-field instance spine and the independently compiled representative, quotient, compatibility, membership, zero-transport, and final finite-norm-class leaves.

This compiled leaf preserves the original public declarations while reusing the shared fixed-field instance providers.

This leaf names the finite-dimensional, scalar-tower, number-field, Galois, and quotient instances reused by the rational finite-norm transport modules. The public dependent type aliases are compiled once here.

This compiled leaf preserves the original public declarations while reusing the shared fixed-field instance providers.

This compiled leaf preserves the original public declarations while reusing the shared fixed-field instance providers.

This compiled leaf preserves the original public declarations while reusing the shared fixed-field instance providers.

This compiled leaf preserves the original public declarations while reusing the shared fixed-field instance providers.

This compiled leaf preserves the original public declarations while reusing the shared fixed-field instance providers.

Compatibility of abstract fixed-field inclusion with ordinary idele-class extension after base change.

The selected second small Hilbert class field is Galois over the canonical fixed-field copy of the original base, and its maximal abelian intermediate field is the selected first small Hilbert class field. Witt transfer…

The small Hilbert class field has reciprocity quotient the ordinary ideal class group. Thus the Frobenius class of a finite prime is its ordinary ideal class, and it is trivial precisely when the prime ideal is principal…

For a finite abelian tower, conjugation by the lower base carries the relative norm subgroup of the upper extension to the relative norm subgroup of the conjugate extension. In the rational absolute idele-class formation…

The first small Hilbert class field is the actual finite abelian subextension selected in HilbertClassFieldRealization. Over its actual fixed field, the closed finite-index small-Hilbert norm subgroup has a finite Galois…

The second-stage class field is selected in the rational absolute class formation. This file transports its exact abstract norm subgroup back to the ordinary idele class group of the actual middle fixed field. The intrin…

An abstract finite abelian subextension of the rational absolute Galois group determines an actual finite abelian extension between its two fixed number fields. This file transports the abstract norm-residue symbol direc…

This public root exports global Artin maps, cyclotomic comparisons, local norm kernels, the principal-idèle product formula, the concrete cyclotomic idèle-class valuation, local--global compatibility, and the descended g…

The valuation used by the local class-formation implementation is the logarithm of the multiplicative absolute value. Consequently its distinguished element of value 1 is the inverse of a DVR uniformizer. The resulting f…

This compatibility module reexports the semantic layers constructing the rational fourth-root complexification, its compositum with a number field, the complex-conjugation overextension at a ramified real place, and the…

This module compares the real fixed place and the original ramified place, then transports the special overextension computation through global norm-residue naturality.

This module realizes the embedded field L(i) inside ℂ, constructs its complex place, and identifies ambient complex conjugation on that field.

This module forms the actual compositum with the rational fourth-root field and proves that restriction to the rational cyclotomic factor is faithful.

This module proves principal-idele triviality, descends the chosen Artin product to the norm quotient, and identifies it with global reciprocity.

This module constructs the real fixed field of complex conjugation, the quadratic overextension above it, and the faithful cyclotomic restriction.

This module realizes the quadratic complexification as the fourth-root cyclotomic field and proves the rational principal-idele Artin formula.

The cyclotomic degree datum on the rational absolute Galois group has an actual maximal-unramified field over every finite abstract fixed field. This file identifies its genuine Galois group with Multiplicative ZHat, usi…

The cyclotomic idele value is trivial on principal ideles, so it descends to the ordinary idele class group. Its restriction to the compact norm-one idele class group still has dense image in ZHat; compactness therefore…

For a number field K, the actual cyclotomic ZHat-extension is the compositum of the embedded copy of K with the rational cyclotomic ZHat-extension. Its normalization factor is the actual intersection degree fK = [K ∩ ℚ̃…

The rational cyclotomic idele value is constructed multiplicatively in CyclotomicIdeleValue. For descent to the additive idele class group and for the valuation package, this file records its genuine continuous additive…

The positive archimedean section over ℚ gives the source term in the cyclotomic norm-one reduction. After taking a positive [K : ℚ]-th root of the absolute norm of an idele, scalar extension of that section cancels the a…

This file isolates the part of the rational principal-idele product formula which follows from the existing archimedean reciprocity API. Every rational idele is split into its archimedean and finite parts. The archimedea…

rationalCyclotomicField now denotes the actual field ℚ(μ∞) inside SeparableClosure ℚ. Its actual Galois group is therefore the standard mathlib type rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField; its finite cyclo…

An abstractly unramified finite abelian subextension is contained in the actual cyclotomic maximal-unramified fixed field. This file realizes that containment as an algebra tower and proves that the finite restriction de…

For an unramified finite abelian subextension of an abstract rational fixed field, the actual global norm-residue homomorphism agrees on every finite one-place idele class with the chosen local Artin homomorphism.

For an unramified finite abelian subextension of an abstract fixed number field, this file constructs the genuine restriction from the cyclotomic maximal-unramified Galois group to the finite Galois group. It then identi…

The rational cyclotomic ZHat-extension lives inside the fixed separable closure of ℚ. To form its compositum with an arbitrary number field, we first embed that number field into the same separable closure. The intersect…

This module equips the compatible fixed-field realization of L / K with the finite-dimensional and number-field instances needed by global class formation, then transports abstract reciprocity back to the original tower.

An actual tower L / K / ℚ must be realized by compatible embeddings before the rational absolute class formation can be applied. We choose only the upper embedding L →ₐ[ℚ] SeparableClosure ℚ; the lower embedding is its r…

This module extends a chosen finite place of L to the common rational separable closure and compares its decomposition data with the corresponding places and completions in the original number-field tower.

This module identifies the abstract fixed fields with the embedded copies of K and L, and transports the resulting idèle-class norm quotient and reciprocity data to the original finite Galois extension.

This module realizes L / K as a finite Galois subextension inside the common rational separable closure. It packages the relevant fixing subgroups, normality, and finite-index data for abstract reciprocity.

For a finite abelian extension of number fields L / K, the local Artin factors of an idele are trivial at all but finitely many finite places. This file forms their finprod directly in the actual global Galois group.

A finite family of local elements, extended by 1, is the product of its one-place ideles. Applying the global norm-quotient map gives the finite product identity. The quotient map itself factors through idele classes and…

The finite-place factor of the transported adic pairing agrees with the established finite-place Hilbert symbol.

The finite-place family already constructed from the local norm-residue pairing satisfies the local laws. Its finite factors agree with the factors of the global Hilbert product formula.

The distinguished integer-valued valuation on a number-field completion provides the valuation relation required by local reciprocity. The valuation relation is passed explicitly, not registered globally.

This aggregate collects finite-place Artin maps, their construction and unramified normalization, and compatibility with conjugation, norms, towers, and cross-local restriction.

This module identifies localized completions associated with conjugate extensions and proves conjugation invariance of the resulting finite-place Artin map.

This module constructs the local Artin map for a chosen extension of a finite place and transports it through the actual decomposition group into the global Galois group.

This module identifies the image with the chosen decomposition group and the kernel with the chosen local norm subgroup.

This module compares localized completions in a square of number fields with different base fields and transports restriction through the corresponding decomposition groups.

This module proves norm--restriction naturality for finite-place Artin maps in an actual square of number fields and their chosen completed local extensions.

This module restricts finite-place extensions through an intermediate field and proves restriction naturality for the corresponding global Artin homomorphisms.

The chosen order-one input has normalized local valuation -1 in the geometric finite-place construction. Its local Artin image is therefore inverse arithmetic Frobenius in the actual chosen completion.

The finite-place reduction in the local--global compatibility theorem uses automorphisms in a specified decomposition group, not arbitrary lifts in the ambient absolute Galois group. This file begins with the source map…

For a finite abelian extension L / K, the global norm-residue symbol on ideles is the product of its archimedean and finite-place local Artin factors.

For a finite abelian extension of number fields, the preliminary global Artin map is the product of the chosen local Artin maps. The finite-place and infinite-place compatibility theorems identify every one-place factor…

For a finite abelian extension L / K, only finitely many finite local Artin factors of an idele are nontrivial. Keeping precisely those finite components, together with every infinite component, gives an idele with finit…

Public aggregate for the finite-place Kummer character comparison, finite support of the Hilbert factors, and the infinite-place comparison.

This module starts the local-to-global Hilbert-symbol layer. At a finite place, global units are mapped into the canonical absolute-value completion, the genuine local Hilbert symbol is evaluated there, and its value is…

The comparison is compiled through an S-valued map from the chosen global Kummer extension to the Kummer extension chosen over the completion. The localized completion and its instance tower occur only in the provider bo…

This file isolates the completion factor used to compare the global Kummer root character with the local Hilbert symbol. The algebra, finiteness, root, and splitting-field data are named separately so downstream proofs d…

The finite-place Hilbert-symbol family is obtained by applying the Kummer root character to the finite-place Artin factors of a principal idele. Its finite support therefore follows directly from the existing finite-supp…

This file compares the two splitting fields of the finite-place Kummer polynomial: the simple Kummer extension chosen directly over the completion and the localization of the chosen global simple Kummer extension. The co…

At a complex place the Hilbert symbol is trivial. At a real place, once the base field contains the relevant roots of unity, the only nontrivial case is the quadratic one: its value is -1 exactly when both arguments are…

This file connects the infinite-place Hilbert factor to the Kummer root character of the actual infinite-place Artin map. The complex-place branch is completed here. The real quadratic action is kept as the next arithmet…

When the radicand is positive at a real place, it is a square in the local completion. The existing Kummer tensor-norm theorem then makes the local norm subgroup all of the completion units, so the actual infinite-place…

This is the arithmetic input for the positive-radicand branch of the real infinite-place Hilbert-symbol comparison.

For a finite abelian Galois extension L / K, the rational absolute idele-class formation realizes the abstract finite norm quotient as the actual quotient CK / N{L/K} CL. The concrete cyclotomic valuation supplies the va…

For an arbitrary finite Galois extension of number fields, the global norm-residue quotient is the abelianization of the genuine Galois group: CK / N{L/K} CL ≃ Gal(L / K)ᵃᵇ. The abelian specialization in GlobalNormResidu…

For a finite tower K ⊆ M ⊆ N with N / K Galois, this file proves that ordinary idèle-class norm from M to K corresponds to restriction from Gal(N / M) to Gal(N / K), after passing both Galois groups to their abelianizati…

This file records the same-base restriction specialization of abstract norm-residue naturality in the rational absolute class formation. All closed subgroups remain in one fixed separable-closure ambient, so the statemen…

A number-field equivalence permutes finite places and identifies the corresponding adic completions. The local pairings and their finite factors can therefore be transported without changing their normalization.

The factor obtained by evaluating a local pairing on global units commutes with equivalences of both the number fields and their completions. The commuting square for the two field embeddings is the only geometric input.

The finite- and infinite-place Hilbert factors constructed in the preceding files all take values in the same group of n-th roots of unity in the base field. Their product is the image, under the global Kummer root chara…

The product formula is invariant under a number-field equivalence. The finite product is reindexed by the induced equivalence of finite places, and the ordinary infinite product by the equivalence of infinite places.

Fixed-point comparisons for finite-index closed subgroups and their actual abstract fixed fields.

Finite Galois relative idele class groups over ℚ, their scalar-extension maps, and the induced absolute Galois representation.

The fixed representation of a finite abstract extension is compared with the relative idele class group of its two actual fixed fields.

Naturality of the fixed-field comparison for automorphisms and the finite-extension Galois action.

Compatibility of fixed-field inclusion and relative norm with the actual idele-class extension attached to the abstract subgroup tower.

This endpoint leaf contains the tensor-unflattening comparisons and the resulting injectivity theorems. The finite-level normal-closure maps and their tower compatibility live in the reusable core leaf.

Normal closures, finite-level scalar extension, tower base change, and the canonical embeddings into the rational idele-class direct limit.

This internal provider isolates the tensor base-change, embedding-product, and direct-limit comparison lemmas used by the non-Galois finite-tower norm theorem. Keeping these commands in their own leaf prevents the endpoi…

This proof leaf installs the canonical finite-tower context once and splits the normal-closure embedding calculation, the pointwise coset action, and the finite product calculation into separate commands. The public theo…

This leaf compares the abstract relative norm in the rational idèle-class direct limit with the ordinary idèle-class norm for a finite fixed-field tower. The upper field need not be Galois over the lower field. The const…

This endpoint leaf turns the reusable fixed-point comparisons into actual descent witnesses first at one finite Galois level and then in the rational idèle-class direct limit.

An element of the rational idele-class direct limit which is fixed over a finite intermediate field is represented at a finite Galois level. Its actual tower base change is Galois-fixed, hence descends to an idele class…

The actual idele class group of a finite rational intermediate field is identified with the corresponding fixed subgroup of the direct limit.

The abstract finite norm subgroup and quotient are identified with the ordinary idele-class norm range and quotient of the actual fixed-field extension.

On every actual fixed field inside the rational separable closure, the canonical fixed-part model identifies each abstract finite norm subgroup with the range of the corresponding ordinary idele-class norm. Since the lat…

This file assembles the finite global Artin homomorphisms in the FiniteGaloisIntermediateField inverse limit supplied by mathlib. The first target is the actual ZHat-extension of ℚ constructed in CyclotomicZHatBaseChange…

The finite global Artin product formula at every finite Galois intermediate field shows that the infinite global Artin homomorphism kills principal ideles. This file descends that homomorphism to the idele class group an…

The absolute idele norm is split, up to inversion, by an idele supported at one infinite place. Its local component is positive, so every finite global Artin homomorphism, and hence the infinite global Artin homomorphism…

The real-place sign in the explicit infinite Hilbert factor is unchanged under an equivalence of number fields. This reindexes the infinite part of the product formula when a field is replaced by a small model.

This file compares the actual Artin homomorphism at an infinite place with the global norm-residue homomorphism on idele classes. The one-place norm statements are proved from genuine relative ideles supported at the cho…

At a ramified infinite place, the local extension is complex over real. Its Artin homomorphism sends the sign of a real unit to the corresponding complex-conjugation element of the decomposition group. At an unramified i…

For a finite Galois extension and an arbitrary intermediate field, this file identifies the image of abelianized restriction with the image of the fixing subgroup. It then proves naturality for the ordinary idèle-class n…

This compatibility module reexports the semantic layers that construct the separable-closure lift, its finite p-adic auxiliary field, and the resulting factorization of the global norm-residue map through every finite-pl…

This module completes the auxiliary-field argument, factors the global norm-residue map through each local Artin quotient, and proves the finite-place local-global compatibility theorem.

This module realizes the simultaneous finite/cyclotomic lift as an actual number field and proves the subgroup and intermediate-field identities needed by the auxiliary-field argument.

This module packages the simultaneous finite-quotient and cyclotomic coordinates and the corresponding abstract auxiliary subextension.

This module constructs the finite-place decomposition restriction maps and the positive p-adic cyclotomic lifts used in the local-global comparison.

The established product formula is transported from the internal subgroup of roots of unity to Mathlib's rootsOfUnity.

The existing maximal-abelian Artin isomorphism is transported through the topological comparison of idèle class groups and the canonical comparison of absolute Galois abelianizations. This module proves the small-univers…

This module specializes the continuous infinite global Artin map to the maximal abelian subextension of the separable closure. It also exposes the idele-representative evaluation and its finite Galois projections.

This module identifies the kernel of the maximal abelian global Artin map with the identity component of the idele class group. It then descends the map to the component quotient. The separation argument is intrinsic to…

This file supplies the useful composite from ideles to the quotient of CK by the range of the ordinary norm CL → CK, used by the global norm-residue-symbol constructions.

At the source level, the key calculation is that an idele supported at one finite place is a global relative-idele norm exactly when its local component is a norm from the corresponding local tensor algebra. The determin…

For two global units a and b, the local Kummer factor can be nontrivial only where a, b, or the exponent fails to be a valuation-ring unit. This file records that concrete finite set, proves triviality outside it from th…

This file isolates the exact quotient calculation used by the Hilbert-symbol product formula. The one-place embedding sends the chosen local norm group directly into the ordinary idele-class norm group, so it descends wi…

The arithmetic norm-residue symbol sends an ordinary unramified uniformizer to arithmetic Frobenius. At the ramified prime of a prime-power cyclotomic layer, a local unit u therefore acts by u⁻¹. This file records those…

The actual rational cyclotomic character is detected by all of its prime-power reductions. In particular, if every reduction of every p-adic character coordinate has square one, then the underlying automorphism of the fu…

This file connects the cyclotomic ramification-index formula over ℤ to the finite-place completions used by the global Artin map. A rational prime outside the conductor is unramified at the actual chosen extension of its…

At a rational prime away from the cyclotomic level, the chosen completed extension is unramified. Its normalized local Artin map is therefore the arithmetic Frobenius raised to the local valuation. The genuine primitive…

This file identifies the algebraic localization of an actual finite rational cyclotomic level with a cyclotomic extension of the completed base. The primitive root is the image of a genuine primitive root in the global l…

For the cyclotomic level p ^ k, this file reindexes the actual chosen finite-place Artin characters over rational primes. Away from p, the unramified formula makes the multiplicative support lie in the ordinary finite pr…

The level-zero factor is trivial. At every positive level, the finite-place character specification reduces the claim to the ramified chosen-Artin formula proved in RationalCyclotomicFinitePlaceArtin.

The ramified local factor at p is the direct p-adic unit character. Every other finite local factor is the inverse Frobenius power prescribed by the rational prime factorization. Their product is the image of the rationa…

For a positive integer m, the genuine idèle-class norm range of the actual cyclotomic level ℚ(μm) is the rational ray congruence subgroup modulo (m). The local input is the cyclotomic higher-unit calculation: at a ration…

Prime-power reductions of the genuine cyclotomic character detect the full rational cyclotomic automorphism. Restricting that automorphism through actual finite cyclotomic levels then detects every finite coordinate of t…

This file records the elementary rational factorization needed for the principal-idele calculation over ℚ. At a fixed rational prime p, removing the p-power from x : ℚˣ leaves the sign of x times the finite product of th…

For a nonzero rational number x and a rational prime p, removing the p-power from x produces an actual p-adic unit. This file identifies that unit simultaneously in the height-one completion used by global reciprocity, i…

The dyadic correction specializes power-residue reciprocity over ℚ and derives Gauss's quadratic reciprocity law.

For a finite abelian extension of number fields, the genuine idele-class norm range is open in the ordinary idele-class topology. Hence its native quotient topology is discrete. The finite Krull Galois group is discrete…

For a finite Galois extension L / K, global norm-residue reciprocity identifies the native idele-class norm quotient with the abelianization of the finite Krull Galois group. This file records the identification as a Con…

Reader-facing facade for the Hasse--Arf theorem: upper ramification jumps of finite Abelian local extensions are integral. Reusable ramification, Lubin--Tate, and local reciprocity infrastructure is exported by its owner…

Collects the local cyclotomic embeddings, inertia bounds, and rational ray class comparisons used in the Kronecker–Weber theorem.

The reader-facing entry point for the local and global Kronecker--Weber theorems. Importing this module exposes both supported endpoints. Every finite abelian extension of ℚ is contained in a cyclotomic field. The arithm…

The synchronized prime above each member of the finite ramification support has inertia cardinality at most the corresponding prime-power totient. Outside that support the auxiliary compositum is unramified. The finite i…

At a ramified prime p, the structured local embedding of L has order (p^f - 1) p^e, while the global conductor has order p^e c with c prime to p. Their common target has order ((p^f - 1) c) p^e; crucially, it uses the sa…

The global conductor cyclotomic field embeds, after base change and enlargement of the order, into the common p-adic cyclotomic target used by the synchronized valued compositum construction.

The chosen localization remains internal to the proof. The public statement mentions only a ring embedding from L to the common local cyclotomic target, so elaborating its type never unfolds completion or transported-alg…

The synchronized global embedding is an isometry for the pulled-back place. It therefore extends to completions. Compatibility on the completed base identifies the restriction to the chosen localization as a genuine ℚp-a…

At each chosen ramified prime, the localization of the single global compositum embeds in the common local cyclotomic field whose p-power part is exactly the exponent selected from L. The arbitrary-coprime local bound th…

The left factor is embedded through its chosen localization. Consequently the pullback of the canonical absolute value on the common local cyclotomic target is exactly the chosen p-adic place. The corrected normal-compos…

This endpoint combines the localization–inertia comparison, the structured local cyclotomic embedding, and the ramification comparison to replace the full cyclotomic totient by the exact p-primary factor φ(p ^ n).

This module proves local Kronecker--Weber through norm-subgroup order reversal, then applies it to localizations of finite abelian extensions of ℚ.

This module uses an ordinary rational uniformizer, not its inverse, and the arithmetic global norm-residue map. Consequently an unramified prime q acts on roots of unity by the direct power q. The finite Galois/ray-class…

For a nonzero natural number m, the selected ray class field for the rational modulus (m) is isomorphic over ℚ to the actual cyclotomic field CyclotomicField m ℚ. The field comparison is obtained from the exact idèle-cla…

For K = ℚ, both the ray class quotient modulo (m) and the Galois group of the m-th cyclotomic field are canonically (ℤ/mℤ)ˣ. This file composes the two independently constructed equivalences and verifies the degree/index…

This file begins the global Kronecker–Weber construction. Two finite abelian extensions, embedded in one separable closure, have a finite abelian compositum. In particular this applies to the given number field and a cyc…

Let S be the finite set of rational primes ramified in L, let n = ∏ p∈S, p ^ ep, and put M = L(μn). This file proves the global ramification assertion used in the inertia count: every finite prime of M outside S is unram…

Public root for the reusable Kummer-theory layer used by abstract class formations.

Root characters, radical quotients, finite and infinite generation, the local unramified unit criterion, and the perfect Kummer pairing for actual field extensions.

This file constructs the roots-of-unity base change for a prime-degree extension. If L / K has prime degree p, the cyclotomic extension K(μp) / K has degree strictly smaller than p. The two degrees are therefore coprime,…

For a finite Galois extension containing an n-th root β of a base-field unit a, this file identifies the local n-th-power condition on a with membership of β in the decomposition field. The proof uses the canonical compa…

This file supplies the ramification input in the existence proof for the global norm topology. Every defining root of K(√[n]{Kˢ}) / K is first rescaled to the root of an actual S-unit. Its simple intermediate field is th…

Collects the finite radical support, local power kernels, and power quotients used to prepare full S-unit Kummer extensions.

The endpoint of the S-unit preparation construction: the rank bound, the exact restriction-kernel cardinality, and prime-power coordinates.

The concrete embedding and Galois restriction map, its fixing subgroup, and the cyclic fixed fields attached to kernel elements.

A chosen finite enlargement of places containing representatives of every class in a finite Kummer radical.

Construction, finite generation, Galois structure, cardinality, and coordinates for the Kummer extension generated by all S-unit roots.

The localization map on S-units, its kernel, its quotient by global powers, and the associated Kummer radical.

The finite n-th-power quotient of an S-unit group, its cardinality, and explicit ZMod n coordinates.

This file proves the local unit case of the Kummer ramification criterion. If both b and the exponent n are units at a finite place, then the chosen localization of K(ⁿ√b) / K at that place is unramified. The proof uses…

This is the canonical root of the complete local class field theory library. It reaches every supported implementation layer. Clients that need a smaller dependency closure should import the semantic owner aggregate for…

Public aggregate for the normal-basis, unit-filtration, valuation, and cohomology calculations establishing the local class-field axiom.

The degree-minus-one assertion for the archimedean local block is independent of the nonarchimedean local reciprocity theorem. It follows directly from Hilbert 90 for the algebraic localization, and therefore applies als…

At a ramified infinite place the local extension is ℂ/ℝ. Its norm subgroup consists exactly of the positive real units, so the sign map identifies the norm quotient with ℤˣ, a group of order two.

This file compares the concrete multiplicative Herbrand quotients from low-degree cyclic cohomology with the Tate objects built from mathlib's actual Galois representation on Lˣ. The comparison uses the standard Galois a…

This file proves the final Herbrand-quotient calculation for the local class-field axiom. Its only input beyond the local-field hypotheses is the preceding normal-basis calculation h(G, OLˣ) = 1 for the actual action on…

This file isolates the dependent-choice bookkeeping in the infinite-product argument of the local class-field-axiom theorem. A one-step lift in a filtered commutative group produces compatible correction and remainder se…

For a finite field extension with a chosen generator of its automorphism group, the cyclic comparison between first group cohomology and negative Tate cohomology transports Hilbert 90 to the statement that the latter gro…

This file proves the final integer-unit Herbrand-quotient calculation. For a sufficiently deep normal-basis neighbourhood V = 1 + πK^n M, the exact sequence 1 → V → 𝒪Lˣ → 𝒪Lˣ / V → 1 has the actual Gal(L / K) actions. Va…

Aggregate for the local block families, their induced and tensor constructions, and the resulting class-field axiom.

Public facade for the canonical family instances and the degree-zero and degree-minus-one Herbrand equivalences.

This file combines the local induced-module calculation over a finite family of places. It is the finite-support part of the localized class formation.

This file combines the local class-field calculation with the finite-product description of local idele blocks. It supplies the finite-place-family part of the finite family of localized class-formation blocks: degree-ze…

For a place w of a Galois extension above a base absolute value v, its decomposition group acts on the local multiplicative group. The product of all conjugate local factors is therefore the induced module from that deco…

This file connects the induced module in LocalBlock with the actual local factor of the scalar-extended adele algebra. The natural Galois action on Kv ⊗[K] L is conjugation on the second tensor factor. The completion ten…

For a finite Galois extension L / K, the completion tensor-product theorem decomposes Kv ⊗[K] L as the product of the completions above v. After choosing one extension w, Galois conjugation identifies every factor with L…

This file provides named algebra, finite-dimensional, Galois, scalar-tower, and global-to-local embedding providers for localized completions.

Public facade for the change-of-group, localized algebra, Galois generator, low-degree Herbrand equivalence, finiteness, and cardinality leaves.

Public facade for the degree-zero, degree-minus-one, triviality, and Herbrand quotient leaves.

This file supplies the localized-completion input for the class formation. First it proves change-of-group equivalences for low-degree multiplicative Tate cohomology. It then applies the canonical algebraic-localization…

For a cyclic extension of nonarchimedean local fields, the actual Tate cohomology of Lˣ has cardinalities [L : K] in degree zero and 1 in degree minus one.

Provides the public declarations in the LocalClassFieldTheory.ClassFormation.NormalBasis Lean module.

The recursive norm and coboundary constructions are converted here into the actual quotient statements H⁰(G,V)=H⁻¹(G,V)=1 used in the local class-field-axiom theorem.

Provides the public declarations in the LocalClassFieldTheory.ClassFormation.NormalBasisFiniteQuotient Lean module.

Provides the public declarations in the LocalClassFieldTheory.ClassFormation.NormalBasisGaloisAction Lean module.

Provides the public declarations in the LocalClassFieldTheory.ClassFormation.NormalBasisGradedLifting Lean module.

Provides the public declarations in the LocalClassFieldTheory.ClassFormation.NormalBasisInfiniteProduct Lean module.

This is the recursive core of the local class-field-axiom theorem. The one-step graded lifting is iterated, its correction factors are multiplied, and completeness of the local field turns the resulting formal recursion…

The map sending an integer unit to its difference from one compares successive principal-unit quotients with the corresponding lattice quotients. The file proves injectivity and constructs this comparison at sufficiently…

Provides the public declarations in the LocalClassFieldTheory.ClassFormation.Valuation Lean module.

This file applies the Herbrand-quotient multiplicativity theorem to the actual valuation sequence from integer units through field units to the value group. All three actions are the concrete actions from ValuationReal:…

Provides the public declarations in the LocalClassFieldTheory.ClassFormation.ValueGroupCohomology Lean module.

Public focused entry point for finite local reciprocity, local conductors, the local Artin map, and the unconditional finite local existence order isomorphism.

For a finite abelian extension L / K, define its conductor exponent as the least n ≥ 0 for which the n-th principal-unit group of K lies in the norm subgroup. The conductor itself is the corresponding power of the maxima…

The prime-power and prime-to-p norm-subgroup computations used by local Kronecker--Weber, exposed as reusable finite local class field theory.

For a primitive p ^ (k + 1)-st root of unity generating L / ℚp, the norm subgroup is exactly the subgroup generated by p and the (k + 1)-st principal units. The odd and dyadic calculations are kept separate before being…

The p-adic prime element used by the cyclotomic norm calculation has normalized valuation -1. This file records the corresponding orientation of the standard unramified/principal-unit intersection lemma.

This file joins the canonical-valuation form of the unramified cyclotomic theorem to the unramified norm computation. For a field generated by a primitive root of order p ^ f - 1, that theorem supplies the unramified ext…

The ordinary norm-subgroup assignment is an order embedding into the opposite poset of native open finite-index subgroups. Kummer theory in characteristic zero and transported Lubin--Tate levels in positive characteristi…

Kummer theory supplies a finite Galois norm subgroup inside the power subgroup attached to any finite-index subgroup of Kˣ. Consequently the ordinary norm-subgroup order embedding is surjective, hence an order isomorphis…

Combining the mixed- and equal-characteristic existence arguments gives the unconditional order isomorphism between finite abelian subextensions of the fixed separable closure and open finite-index subgroups of the local…

For an exponent nonzero in the base field, adjoining the roots of unity, applying maximal Kummer theory, and descending the norm inclusion produces a finite Galois extension whose norm subgroup is contained in Kˣⁿ.

The explicit Lubin--Tate level over the Laurent-series model is transported to an arbitrary equal-characteristic local field. Together with an unramified extension, it supplies a finite Galois extension whose norm subgro…

Every finite abelian extension of a positive-characteristic local field embeds into the fixed field represented by a finite abelian compositum of an unramified factor and a transported Lubin--Tate factor. This is the sou…

The abstract local class formation already constructs, for every positive d, a canonical finite unramified abelian subextension of the local absolute Galois group. This file takes its actual fixed field in the chosen sep…

Let H ≤ Kˣ have finite index n, with n nonzero in K, and suppose that K contains a primitive n-th root of unity. Lagrange's theorem gives Kˣⁿ ≤ H; the maximal Kummer extension constructed above has norm group exactly Kˣⁿ…

This file isolates the common abstract Galois-theoretic realization of the absolute Galois group, its unit representation, and the ground-field fixing subgroup. Both the characteristic-zero and equal-characteristic exist…

This module constructs the diagonal descent field attached to an arbitrary explicit uniformizer. The unramified factor has the exact order of the inverse finite Lubin--Tate unit action. Arithmetic Frobenius on that facto…

The finite-existence theorem is formulated internally using closed subgroups of the absolute Galois group. Here we identify those objects with finite abelian intermediate fields of Mathlib's chosen separable closure.

When the base field contains the n-th roots of unity, Kummer duality and finite local reciprocity identify the norm subgroup of the maximal exponent-n Kummer extension with the subgroup of n-th powers.

A finite abelian subextension of the fixed separable closure determines an ordinary norm subgroup of the local multiplicative group. This module proves that the resulting assignment is an order embedding into the opposit…

Compatible field equivalences carry the actual group of field norms to the actual group of field norms. This is the norm comparison needed when finite local class-field theory is transported to a small representative.

This file translates the abstract existence theorem into ordinary field norms. It proves the compositum and intersection formulas, isolates the norm-topology criterion which makes the ordinary norm-subgroup order embeddi…

This module realizes a finite abelian extension inside a fixed separable closure and packages it as an abstract finite abelian subextension. It then transports the abstract order reversal for norm subgroups back to ordin…

The base equivalence and the equivalence between the two chosen separable closures together transport finite abelian intermediate fields, preserving their inclusion order.

The finite-abelian-field order equivalence carries the actual field-norm subgroup, not merely an abstract subgroup assigned by a classification.

The intermediate field itself is unchanged as a subfield of the original separable closure. Its finite-dimensional and abelian Galois properties are transported along the base-field equivalence.

The field norm from an intermediate field is unchanged after re-expressing that intermediate field over the equivalent small base field.

The base-field equivalence Shrink K ≃+ K does not change the subfields of the original separable closure. This file records that fact as an order isomorphism, with the actual underlying subfields unchanged.

The concrete classification for a small local field transfers to an arbitrary nonarchimedean local field. The transfer respects the actual field-norm subgroup.

The topological field equivalence between K and its small representative induces an order equivalence between their open finite-index subgroups of units.

The existing separable closure of K is also a separable closure of Shrink.{0} K after transporting the base-field embedding. This gives a compatible equivalence with Mathlib's chosen separable closure of Shrink K.

Every finite abelian local extension embeds into the fixed field represented by a compositum of a canonical unramified factor and a canonical standard Lubin--Tate factor. Reverse inclusion of norm subgroups supplies the…

The canonical standard Lubin--Tate level is already an intermediate field of the fixed separable closure. This module retains it as a named finite abelian subextension, identifies its represented fixed field and norm sub…

The unramified degree-d factor forces the normalized valuation to be divisible by d. The totally ramified Lubin--Tate factor forces an element to lie in ⟨ϖ⟩ U^n. Their intersection therefore lies in ⟨ϖ^d⟩ U^n. This is th…

This module is the standard-uniformizer specialization of LubinTateUniformizerDiagonal. The construction itself is carried out for an arbitrary explicit uniformizer there; specializing it here keeps the canonical API def…

For the canonical unramified extension of degree d, every relative norm has normalized valuation divisible by d. This file transports that abstract norm subgroup from fixed coefficients to the ordinary multiplicative gro…

For a nonarchimedean local field, the norm subgroup of an unramified extension of degree n is characterized by divisibility of the normalized valuation by n. This file packages that subgroup, its quotient map, and the ca…

The converse to the small-base transport: an intermediate field over Shrink K in the original separable closure remains finite abelian over K.

For local reciprocity the coefficient module in the abstract class formation is A = (K^sep)ˣ. This file identifies its subgroup fixed by the actual closed fixing subgroup of an intermediate field E with the image of Eˣ.…

The abstract class-formation framework indexes finite fields by closed subgroups, whereas the local norm calculation is stated for their concrete fixed intermediate fields. This file identifies the two presentations. In…

For a finite abstract tower represented by closed subgroups L ≤ K, this file identifies the descended coefficient representation on AL with the ordinary representation of Gal(L/K) on the units of the concrete upper fixed…

Exhaustive aggregate for the finite-level reciprocity equivalence, the continuous local Artin map, its norm kernel and surjectivity, and the local class-formation construction beneath them.

The construction of local reciprocity realizes a finite Galois extension in a fixed separable closure. This file proves that the transported reciprocity isomorphism is independent of that realization. Two embeddings are…

The abstract prime-norm formula is transported through an explicit separable-closure realization. The resulting concrete norm-residue symbol sends the transported base-field norm to the represented Galois automorphism.

This file contains the final comparison step in the proof of the local reciprocity law. Once the actual absolute-Galois datum, henselian valuation, and class-field axiom have been constructed, the abstract reciprocity th…

Two realizations of a finite Galois extension inside the fixed separable closure are related by conjugation. This module transports that conjugation to the actual Galois group, records the algebraic norm-residue square,…

Lower acyclic aggregate for the finite reciprocity implementation. Filtered specializations import this module without depending on the public aggregate that later re-exports them.

This file transfers unramifiedness from the residue-degree datum on the absolute Galois group to the concrete valuation on the corresponding finite fixed field. It is the bridge from the canonical abstract unramified ext…

Public aggregate for the filtered Artin-map API and its unramified, equal-characteristic, compositum, and finite-Abelian specializations.

At a nonnegative ramification index, an unramified factor contributes trivially to both the principal-unit Artin image and the upper ramification group. Equality on the other factor can then be recovered upstairs from th…

The principal-unit filtration transported to a finite Abelian Galois group by the local Artin map. Its comparison with upper ramification groups is the filtered reciprocity theorem; this file first records the Artin side…

Every finite abelian extension of a positive-characteristic local field embeds in a standard finite abelian compositum. Passing to the field range inside the fixed separable closure lets filtered reciprocity descend by r…

The fixed field of the standard finite abelian compositum is the compositum of its canonical unramified factor and its named transported Lubin--Tate factor. The first factor has trivial Artin and upper groups at nonnegat…

An arbitrary finite abelian extension embeds into a standard finite abelian compositum. Passing to its field range inside the fixed separable closure permits descent by restriction, and the resulting algebra equivalence…

A finite Galois intermediate field of a local separable closure whose fixing subgroup contains the kernel of the residue-degree map is unramified for its canonical spectral valuation. The proof constructs its finite abst…

The characteristic-independent standard compositum consists of the canonical unramified factor and a canonical standard Lubin--Tate factor. At nonnegative indices the unramified factor contributes trivially, while filter…

The Artin map kills valuation-ring units in an unramified finite extension, so every positive principal-unit image is trivial.

A finite abelian quotient is determined by its action on all intermediate subgroups together with its action on a sufficiently large cyclic quotient. The group-theoretic statement below isolates the part of uniqueness of…

At a fixed finite abelian stage, every Galois subgroup is the fixing subgroup of an intermediate field. Transporting that field into the chosen separable closure lets the common norm-kernel and tower conditions compare t…

For a finite abelian local extension E, adjoining the unramified extension of degree divisible by |Gal(E/K)| produces a Galois group annihilated by that degree. Restriction to the unramified factor sends the normalized A…

The abstract fields to which the class field axiom is applied are the open closed subgroups of the absolute Galois group. This file turns the explicit finite-index witness from the abstract class-formation data into the…

The local class-field-axiom theorem on finite extensions of a local field. Mathlib's local-field predicate is topology-first, while the local class-field-axiom theorem also needs a compatible local-field structure on the…

Every finite Galois extension L/K is embedded into the chosen separable closure of K. Its image supplies the concrete closed subgroup used by the abstract class-field theory. The resulting abstract fixed coefficient grou…

The residue-action exact sequence presents the residue field of a finite fixed field intrinsically, inside the selected residue algebraic closure. The norm formula uses the literal residue field of the spectral valuation…

The degree map used in local reciprocity comes from the arithmetic Frobenius on the algebraic closure of the finite residue field. This file constructs the finite-level source of that map: for every finite extension of a…

The valuation on an algebraic ambient field can be restricted to a finite intermediate field. Over a complete discrete valuation field this restriction is the unique extension valuation ring, so it agrees with any other…

This file compares the residue action used by localResidueDatum with the same residue action after changing the ground field to the fixed field of a closed subgroup. The comparison is made on the common selected residue…

The algebraic norm--restriction and transfer--inclusion diagrams are upgraded here to diagrams of continuous homomorphisms. Every finite fixed field uses the spectral norm extended from the original local field. Thus no…

Aggregate for the comparison of intrinsic Frobenius and norm-residue maps in fixed fields, including their ambient-prime and base-change transports.

This module defines the ambient fixed-field norm-residue value attached to a unit of the intrinsically presented base field, both before and after identifying the abelianization of an abelian Galois group with the group…

The local Artin map and the ambient embedded norm-residue construction agree on norm classes and therefore agree pointwise.

This module transports valuation-one units and norm classes through compatible field equivalences, and evaluates abstract fixed-field norm-residue symbols on transported prime norms.

This module identifies the ambient norm-residue symbol of the chosen prime witness with the Frobenius target transported back to the original embedded Galois group.

This module constructs the ambient norm-residue value, a valuation-one prime witness for each abelianized Galois element, and the corresponding ambient Frobenius target.

The chosen ambient prime witness represents the prescribed abelianized Galois element both under the concrete local Artin map and under the ambient fixed-field norm-residue construction.

This aggregate exposes the intrinsic-to-ambient base, extension, inertia, and norm-quotient comparisons for finite fixed fields.

This module identifies extension subgroups transported through an embedded finite Galois extension and constructs the resulting ambient quotient equivalence with the actual Galois group.

This module transports extension inertia between an intrinsic finite extension and its realization inside an ambient separable closure.

This module compares cohomological finite norm quotients with ordinary field-norm quotients and records their compatibility with fixed-field norm-residue symbols.

This module specializes the embedded subgroup and inertia comparisons to actual finite fixed fields and packages the intrinsic Frobenius quotient.

This module compares the intrinsic absolute Galois base of a finite extension with its realization as a fixing subgroup in an ambient separable closure.

This module transports inertia, Frobenius elements, and fixed fields across an explicit equivalence of separable closures.

This module identifies the canonical local Artin homomorphism of an actual finite fixed-field extension with its ambient fixed-field norm-residue symbol.

This module compares the intrinsic and ambient Frobenius closures after the quotient transport has been constructed.

This module transports Frobenius-fixed subgroups and fixed fields through the intrinsic-to-ambient closure equivalence.

This module constructs the intrinsic-to-ambient quotient transport and maps Frobenius elements before the closure comparisons.

This module proves norm--restriction naturality for actual finite abelian local Artin maps.

This module compares intrinsic local Artin maps with the ambient fixed-field norm-residue symbol.

This file compares the normalized valuation induced on a finite abstract field by the local class formation with the ordinary normalized valuation of its concrete fixed field. The concrete field is equipped with the cano…

This file transports norm-restriction and transfer-inclusion naturality from the closed-subgroup class formation to actual fixed fields in a single Galois ambient field.

This file identifies the class-formation relative norm on ambient fixed units with the ordinary field norm between two concrete fixed fields. The intermediate extension need not be normal: relative left cosets are identi…

For a Galois ambient extension Ω/K, the abstract class-formation model represents K by the closed fixing subgroup of the bottom intermediate field and an intermediate normal extension E/K by the closed subgroup fixing E.…

The fixed-separable-closure form of finite local reciprocity naturality is transported here to an arbitrary tower K ⊂ E ⊂ L. The two extensions are realized compatibly in the chosen separable closure by first embedding L…

The normalized valuation of the base local field is transported to the actual fixed coefficient group in the separable closure and then embedded in ℤ̂. Its range is proved to be exactly the ordinary integers inside ℤ̂, a…

The abstract class formation supplies restriction naturality. This file constructs the field-facing restriction map for two finite Galois intermediate fields in the fixed separable closure and transports the naturality i…

This module packages the absolute Galois group of a field, its integral unit representation, and its distinguished abstract base field using the chosen separable closure.

For a finite cyclic abstract tower L / K / k, the closed subgroups are replaced by their concrete fixed fields. The lower fixed field is finite over the local ground field and the upper fixed field is finite Galois over…

For a nonarchimedean local field, the normalized discrete valuation on the base unit group satisfies the Henselian valuation condition. The value group is the copy of the ordinary integers in the profinite integers. For…

For a nonarchimedean local field K, this file makes the choices implicit in the construction explicit. The canonical local valuation is packaged as a complete DVF, Chevalley's theorem chooses an extension to AlgebraicClo…

The residue Frobenius datum, the normalized henselian valuation, and the class-field axiom constructed over the fixed separable closure are inserted into the abstract reciprocity theorem. The resulting isomorphism is ind…

This is the implementation layer for the reader-facing local CFT module. It collects the existing finite, absolute, naturality, normalization, and existence results without renaming them or wrapping them in an existence…

For a finite abelian Galois extension, finite local reciprocity takes values in the actual Galois group, not merely its abelianization. This module provides both the algebraic homomorphism and its continuous refinement f…

The actual algebraic and continuous Artin maps commute with restriction between finite abelian intermediate fields of the fixed separable closure.

For a finite field k, arithmetic Frobenius identifies the absolute Galois group of k with the profinite integers. This file proves the missing global statement from the compatible finite Frobenius coordinates: every posi…

The finite Frobenius exponent maps are compatible with restriction. This file therefore assembles them in the actual inverse-limit presentation of an infinite Galois group. It produces the canonical continuous homomorphi…

This file separates the two group-theoretic comparisons used by the local degree map. The residue-action exact-sequence theorem supplies the actual action of an absolute decomposition group on the selected residue algebr…

The residue field obtained from a valuation ring in a separable closure is not definitionally Mathlib's chosen AlgebraicClosure. The construction of the degree map must therefore work on any algebraically closed algebrai…

The residue field of a valuation ring in an algebraically closed field is algebraically closed. This is the missing source needed to apply the intrinsic finite-field degree map to the residue of an algebraic closure of a…

The arithmetic-Frobenius degree on an algebraic closure of a finite field is packaged as the initial datum of the abstract class-formation framework. For every finite residue subextension, the image of its fixing subgrou…

The actual finite local Artin map is natural when both the base local field and the finite abelian extension are replaced by compatible field equivalences. The proof realizes the base equivalence as a degree-one vertical…

The henselian condition in the abstract class-formation framework quantifies over every finite abstract field, not only over normal ones. For an intermediate finite separable field E in a separably closed Galois ambient…

For a finite separable extension, the field norm becomes the product over all base-field embeddings after mapping into a separably closed ambient field. The ambient field need not be a normal extension of the base field.

The coefficient module in local class field theory is the unit group of a separable closure. This file compares the norm defined in the abstract class-formation framework by a sum over abstract Galois cosets with the ord…

The fixed-field realization of an abstract extension changes both the presentation of its cyclic group and the presentation of its coefficient module. This file records the two honest functorial comparisons needed to tra…

This module upgrades the algebraic finite local reciprocity isomorphism to a homeomorphic group isomorphism. The key input is that the norm subgroup of a finite Galois extension is open. Consequently its quotient is disc…

This module compares the residue-degree construction on a fixed separable closure with the ordinary unramified valuation extension and its arithmetic Frobenius.

For a finite unramified Galois extension, the field-norm subgroup is exactly the subgroup of elements whose normalized valuation is divisible by the extension degree. The inclusion is the normalized norm formula; the rev…

The canonical local norm-residue symbol is identified with the field-facing unramified Artin map. An element of normalized valuation one maps to arithmetic Frobenius, both algebraically and in the topological abelianizat…

For a finite unramified Galois extension, this module composes the actual norm quotient with its normalized valuation model, the generator-normalized Frobenius model of the Galois group, and the canonical equivalence wit…

For an unramified finite abelian extension, the arithmetic q-power action on residues determines the Galois automorphism uniquely. The canonical local Artin map takes an inverse uniformizer to this automorphism.

The base valuation certificate supplies the pullback on base elements. Henselian uniqueness then identifies the selected valuation rings on the separable closures; no equality of the extension valuations is assumed.

Provides the public declarations in the LocalClassFieldTheory.Finite.Unramified Lean module.

For an unramified extension of local fields the actual low-degree Tate cohomology of the integer units and of every principal-unit group is trivial. The norm statements are the corresponding actual norm surjections.

Provides the public declarations in the LocalClassFieldTheory.Finite.Unramified.Norm Lean module.

Provides the public declarations in the LocalClassFieldTheory.Finite.Unramified.PrincipalUnits Lean module.

Provides the public declarations in the LocalClassFieldTheory.Finite.Unramified.PrincipalUnits.Basic Lean module.

Provides the public declarations in the LocalClassFieldTheory.Finite.Unramified.PrincipalUnits.Lift Lean module.

Provides the public declarations in the LocalClassFieldTheory.Finite.Unramified.PrincipalUnits.NormSide Lean module.

Provides the public declarations in the LocalClassFieldTheory.Finite.Unramified.PrincipalUnits.Trace Lean module.

Provides the public declarations in the LocalClassFieldTheory.Finite.Unramified.ResidueNorm Lean module.

This file connects the real valuation quotient Kˣ / unramifiedNormSubgroup K n from NormSubgroup with the chosen inverse DVR uniformizer from IdealQuotients. This is the unramified norm calculation uniformizer side of th…

For an unramified finite abelian extension, normalized valuation identifies the norm subgroup and shows that all base-field units are norms. Hence its conductor ideal is 1. Conversely, conductor one identifies the norm q…

Finite local reciprocity supplies a surjective Artin map at every open finite quotient of the absolute topological abelianization. This module assembles those maps into the absolute Artin map and records its finite-stage…

Projecting the absolute Artin map to a finite abelian subextension recovers its canonical finite Artin map, not merely the same norm kernel.

The canonical finite quotient identifications commute with quotient transition on the profinite side and restriction on the Galois side.

Every open normal subgroup of the profinite topological abelianization of the absolute Galois group determines a finite abelian subextension of the fixed separable closure. The corresponding finite quotient is canonicall…

The field-generic construction is owned by AlgebraicNumberTheory.Galois.AbsoluteAbelianization. This module preserves the established local names as definitional wrappers for downstream users.

The abstract profinite completion of a group is the completion formed from all finite-index normal subgroups, without reference to a topology. We realize it by applying the open-quotient construction to a discrete copy o…

Public aggregate for the topological profinite completion, compatible finite Artin maps, the absolute local Artin map, and the profinite local reciprocity equivalence.

Every finite abelian subextension of the fixed separable closure determines an open normal subgroup of the absolute topological abelianization. This module identifies its pullback along the absolute Artin map with the or…

The open normal subgroups of the absolute abelianized Galois group index three covariant finite diagrams: its finite quotients, the corresponding finite abelian Galois groups, and the corresponding norm quotients. This f…

Every nontrivial element of Kˣ is detected by an open finite quotient. A nonzero valuation is detected by a finite cyclic quotient of ℤ; an element of valuation zero is detected by a finite quotient of the profinite unit…

This module constructs the topological profinite completion of a topological group from its open finite-index normal subgroups. Unlike the abstract completion by all finite quotients, the indexing category records the to…

The universal lift to a profinite target is onto when the original map has dense range. It is one-to-one when pullbacks of open normal subgroups of the target are cofinal among the defining open finite-index normal subgr…

The absolute Artin map constructed from the compatible finite reciprocity maps is transported from the fixed separable closure to Mathlib's usual algebraic-closure absolute Galois group. Its canonical extension to the to…

A continuous multiplicative equivalence carries the closure of the commutator subgroup onto the corresponding closure. It therefore descends to a continuous multiplicative equivalence of topological abelianizations.

Aggregate for the local Hilbert symbol, its laws, and the maximal local Kummer pairing, including the tame power-residue formula.

When X^n - a is irreducible, the canonical algebra obtained by adjoining a root is isomorphic to the chosen simple Kummer field. This file transports the algebra norm through that isomorphism.

If m ∣ n and the base contains μₘ, an m-th root of a differs from the (n/m)-th power of an n-th root by a base-field root of unity. Thus the chosen simple extensions form an actual tower in the separable closure.

Implementation-level comparisons for the chosen simple Kummer extension. The reader-facing Hilbert-symbol theorems state these results without exposing this particular choice of a radical in their types.

The source Hilbert symbol uses its first argument as the local Artin input and its second as the Kummer radical. Artin restriction along the actual simple Kummer tower makes its values compatible as the exponent varies.

The chosen simple Kummer extension attached to one radical lies in the maximal finite Kummer extension. Restriction of the maximal local Artin automorphism to that simple extension, together with functoriality of root qu…

The maximal finite Kummer extension identifies the common kernel of the local Hilbert-symbol characters with the subgroup of powers. The resulting symbol therefore descends to a nondegenerate pairing on the local power-c…

This file constructs the local Hilbert symbol from the public Kummer-theory and local-reciprocity APIs. For b : Kˣ, a root β of X ^ n - b is chosen in the separable closure and the literal simple extension K(β) is formed…

The local Hilbert-symbol character is the composite of the local Artin map, the injective character obtained by evaluating automorphisms on the chosen Kummer radical, and the equivalence that transports roots of unity ba…

The existing local Artin construction is transported to the public power-class group and root-of-unity subgroup.

The maximal exponent-n Kummer extension of a nonarchimedean local field is finite. Evaluating its Kummer pairing at the local Artin automorphism therefore gives a multiplicative character in the radical variable. This fi…

This file constructs reduction of local roots of unity, proves its injectivity, identifies the arithmetic-Frobenius root quotient with the finite-field power residue symbol, and derives the tame formula for the local Hil…

The Type 0 local construction can be applied to a small representative of a local field. This file transports its public power-class and Kummer-norm statements back across the field equivalence.

This is the dependency boundary between reusable Lubin--Tate theory and its local-class-field-theory application. Finite local reciprocity identifies the exact norm subgroup both for the canonical characteristic-independ…

This file extends the integral comparison between standard local Artin images and upper ramification groups to every nonnegative real index. It separately packages the zeroth and terminal cases, then combines them with t…

The exact transported norm-subgroup formula and finite-tower naturality of the local Artin map identify the image of a target-field principal-unit group with the kernel of restriction to the corresponding lower transport…

The transported Lubin--Tate level used by equal-characteristic existence is represented inside the fixed separable closure by a named finite abelian subextension. The canonical algebra equivalence to that fixed field tra…

The explicit level fields form a tower inside the Laurent separable closure. After transporting their base algebra to the target local field, the same inclusions are target-field linear. This file packages the resulting…

The integral target-field comparison is extended to every nonnegative real index. The upper filtration is transported from the Laurent model, while the zeroth and terminal Artin groups use the exact transported norm subg…

The explicit Lubin--Tate level field is unchanged when its Laurent-series base algebra is transported to an arbitrary equal-characteristic local field. The normalized Laurent equivalence preserves the valuation rings, so…

At an integral upper index, the explicit Laurent Lubin--Tate upper group is a restriction kernel. The base-field transport equivalences commute with level restriction, so the same kernel description holds for the transpo…

This file identifies the image of the k-th higher-unit subgroup under the explicit finite-level Artin map a ↦ [a⁻¹] with the actual upper ramification group G^k.

The normalized Laurent-series equivalence used in the equal-characteristic Lubin--Tate construction restricts to an equivalence between the power-series coefficient ring and the target integer ring. Consequently it carri…

The reusable Lubin--Tate calculation is carried out over the standard Laurent-series model. This application-layer file transports its exact norm-subgroup result to an arbitrary equal-characteristic local field. The chos…

The equality between the norm-subgroup index and the extension degree uses finite local reciprocity. It therefore belongs to the concrete local class field theory application layer, not to the reusable Lubin--Tate librar…

The reusable Lubin--Tate layer proves containment of the standard subgroup and computes its quotient. Finite local reciprocity computes the norm-subgroup index here, in the application layer, so the containment becomes a…

This file compares the actual finite local Artin map with the explicit multiplicative Lubin--Tate action. The first source-produced comparison is on the deepest invisible principal-unit group: a unit in U^(n + 1) is an a…

This file compares the principal-unit filtration transported by the standard finite local Artin map with the actual upper ramification filtration of an explicit equal-characteristic Lubin--Tate level. The proof uses rest…

This module records the characteristic-independent part of the filtered Artin comparison for the canonical standard Lubin--Tate tower. The local Artin image of a lower level's norm subgroup is the kernel of restriction f…

The canonical standard Lubin--Tate level is retained by local existence as a finite abelian subextension of the fixed separable closure. Its canonical algebra equivalence with the represented fixed field transports both…

Finite local reciprocity identifies the cardinality of the norm quotient of a finite abelian Galois extension with its field degree. Applied to a standard Lubin--Tate level over the canonical local-field package, this gi…

The changed-uniformizer comparison shows that every (n + 1)-st principal unit is a norm from the standard level n. Together with the known norm of the chosen uniformizer, this contains the canonical standard open subgrou…

For the topology-first nonarchimedean local field K, the canonical Lubin--Tate uniformizer and the (n + 1)-st principal units generate a subgroup of Kˣ of index (Nat.card 𝓀[K] - 1) Nat.card 𝓀[K] ^ n. The proof passes fro…

The exact principal-unit transport upgrades the transported equal-characteristic Lubin--Tate norm containment to the sharp standard subgroup formula.

Public root for reusable local-field infrastructure. This layer may depend on ValuationTheory, but not on RamificationTheory, ClassFormation, or LocalClassFieldTheory.

Aggregate for p-adic additive subgroups, units, local-field instances, and cyclotomic extensions.

Aggregate for the totally ramified and unramified cyclotomic constructions.

The prime-to-p cyclotomic construction and its arithmetic Frobenius.

The unramified cyclotomic construction is proved for the additive exponential valuation. This file identifies that presentation, for ℚ[p], with the concrete complete-DVF valuation used by the local class field theory fil…

This is the public aggregate for Lubin--Tate theory. It exports the formal module foundations, the characteristic-independent standard finite-level division fields and their lower/upper ramification formulas, and the exp…

Public aggregate for the equal-characteristic Lubin--Tate construction. It includes the Laurent-series model, finite and completed Lubin--Tate levels, and the Frobenius and theta constructions. The local-class-field-theo…

Public aggregate for completed level fields, Frobenius fixed fields, and completed norm calculations.

For u ∈ κ⟦T⟧ˣ, the theta construction used in the completed theta-intertwining theorem intertwines the target parameter T with the source parameter u⁻¹T. This file therefore base-changes the primitive polynomial for u⁻¹T…

The theta relation in the completed theta-intertwining theorem uses the source parameter u⁻¹T. We first prove, genuinely by Eisenstein over (AlgebraicClosure κ)[[T]], that its primitive polynomial stays irreducible over…

This small interface identifies the changed polynomials over k((T)) with their ambient Lubin--Tate endomorphisms. Keeping the evaluation layer separate avoids rebuilding the larger algebraic changed-uniformizer construct…

If u is a unit of κ[[T]], then uT is again a uniformizer. This file repeats the mechanical part of the Lubin--Tate construction with P{uT}(Y) = Y^q + uT Y. The primitive level polynomial is monic and Eisenstein at (T), h…

The parameter aT, with a a power-series unit, is a prime element of the canonical Laurent integer ring. Consequently its inverse has normalized additive value one. This is the concrete prime certificate used in the chang…

The prescribed completed lift is semilinear over the completed maximal unramified field. Arithmetic Frobenius on that field fixes the embedded Laurent base k((T)); hence the lift is an actual k((T))-automorphism.

For every prescribed bracket unit a, pullback of the completed-level spectral norm along the semilinear Frobenius lift is a power-multiplicative algebra norm extending the original norm of the completed maximal-unramifie…

Let delta be the completed lift whose action on the standard primitive point is [u⁻¹]. This file defines the Frobenius fixed field Sigma, places the fixed analytic value theta(lambda) in it, and factors the finite target…

This light leaf names the base algebra already determined by the completed Frobenius action. Naming it prevents repeated fallback searches through generic scalar-action instances in later norm calculations.

Expansion in the direct-theta power basis turns Frobenius fixedness into coefficientwise fixedness. The coefficients therefore descend from the completed unramified field to the original Laurent base.

The direct theta value has the changed primitive polynomial over k((T)). Together with the fixed-field generation theorem this gives the exact extension degree (q - 1) q^n.

The coefficient-descent inclusion and the already proved fixedness of the direct theta value identify the fixed field with its simple Laurent-base extension.

The direct theta value supplies the power basis used to descend coefficients of elements fixed by the prescribed completed Frobenius.

The direct theta value has the changed completed primitive polynomial as its minimal polynomial over the completed maximal-unramified Laurent field. Comparing degrees shows that this point generates the whole completed l…

The fixed field of the prescribed completed Frobenius lift is the finite Lubin--Tate level for the changed uniformizer aT. Under this identification its generator is the distinguished element pidelta = theta(lambda). Its…

Arithmetic Frobenius on (AlgebraicClosure κ)((T)) fixes the primitive Lubin--Tate polynomial. Using its primitive power basis, we extend Frobenius to the completed level while prescribing the image of the primitive point…

Let k be the residue field and put K∞ = (AlgebraicClosure k)((T)). This file base-changes the primitive Lubin--Tate polynomial to K∞, takes its genuine splitting field, and equips that finite extension with the spectral…

The completed level used in the proof of the completed theta-intertwining theorem is the splitting field of the base-changed primitive division polynomial. This file records that its chosen root is genuinely primitive of…

The primitive Lubin--Tate polynomial remains Eisenstein after replacing the finite residue field κ by its algebraic closure. Consequently it remains irreducible over (AlgebraicClosure κ)((T)). This is the algebraic input…

point The first theta identity uses the independently constructed formal bracket, whereas the completed Frobenius lift acts through the finite bracket from the finite Lubin–Tate bracket construction. This file proves tha…

In the proof of the completed theta-intertwining theorem the standard Lubin--Tate series is eT(Y) = Y^q + T Y. For a unit u, this file constructs the endomorphism [u] of this standard Lubin--Tate group. Its linear coeffi…

The standard bracket constructed from its contracting coefficient equations agrees with the recursive T-adic bracket used in the finite Lubin–Tate bracket construction. At the formal series level the required identity is…

level The analytic value theta(lambda) is primitive torsion for the target parameter uT. We identify uT with the changed Laurent uniformizer, deduce the actual primitive-polynomial equation, and obtain the canonical embe…

The standard completed primitive point lambda is a division-level n + 1 point for the source parameter T. This file genuinely evaluates the direct theta series at lambda, iterates theta^φ ∘ eT = e(uT) ∘ theta, and proves…

For the standard source prime T and target prime uT, this file proves theta^φ = theta ∘ [u]. The bracket [u] is the independently constructed endomorphism of the standard Lubin--Tate group from EqualCharacteristicDirectL…

For the direct change of parameter T -> uT, the completed Frobenius lift is prescribed by [u⁻¹] on the standard primitive point. This file proves that it fixes the genuine convergent value theta(lambda). The proof first…

For the direct orientation T → uT, this file applies coefficient Frobenius repeatedly to the formal identity theta^φ ∘ eT = e(uT) ∘ theta.

This file constructs the theta series in the orientation used directly in the completed theta-intertwining theorem: the source prime is pi = T and the target prime is barpi = uT. Thus the second identity is theta^φ ∘ eT…

This file evaluates the theta series analytically at the chosen primitive division point in the completed level field.

The theta series has a unit linear coefficient and integral higher coefficients. This file records the resulting nonarchimedean local isometry on the maximal ideal.

Public aggregate for the reusable Laurent-series model and its normalized uniformizer. Transport of the exact norm-subgroup calculation to an arbitrary equal-characteristic local field uses finite local reciprocity and i…

For a finite field k, the valuation ring in k((T)) is the image of k[[T]]. With the coefficientwise product topology the latter is compact by Tychonoff. This file proves that its inclusion into the native Laurent valuati…

For the positive-characteristic branch of the existence theorem, the local-field classification identifies a local field with a Laurent-series field over its residue field. The earlier complete-DVR development constructs…

The Laurent-series valuation sends T to exp (-1). The power-series description of its integer ring makes T a genuine prime element, so the canonical normalized additive valuation sends T⁻¹ to 1.

Public aggregate for division torsion, finite level fields, and their Galois and norm structure.

The kernel of the n-fold distinguished endomorphism in any ambient field is stable under all truncated brackets. Units of κ⟦T⟧ therefore act on it by actual additive automorphisms. This is the version needed in the separ…

Let P(Y)=Y^q+TY. Its n-fold compositional iterate has degree q^n. The polynomial Q(n+1)(Y) = P^n^(q-1) + T cuts out the primitive level-n+1 division points. Here we construct these polynomials over κ((T)), prove the degr…

A unit power series modulo its first n+1 coefficients is represented by a nonzero constant coefficient and n arbitrary further coefficients. We use the concrete finite parameter type κˣ × (Fin n → κ), construct its genui…

rank one For the standard equal-characteristic Lubin--Tate series, the points killed by the (n + 1)-st iterate form a free rank-one module over κ⟦T⟧/(T^(n+1)). The shift is intentional: the existing division-tower The pr…

The finite unit parameters constructed previously exhaust the automorphisms of a level field. To prove commutativity genuinely, we express each truncated bracket as evaluation of a polynomial over the Laurent-series base…

The explicit Lubin--Tate brackets preserve the simple level field. Each finite unit parameter therefore gives a root of the generator's minimal polynomial inside that field, hence an automorphism obtained from its power…

The level-n+1 field is the simple extension generated by a primitive division point. Eisenstein irreducibility identifies its minimal polynomial with the primitive division polynomial and gives the exact degree (q - 1) q…

The primitive roots used to define the finite levels are chosen independently inside one separable closure. This file proves that the resulting standard level fields nevertheless form an increasing tower.

For a primitive level-n+1 division point λ, its Eisenstein minimal polynomial has constant coefficient T. The power-basis norm formula therefore gives the norm identity N(-λ) = T.

The genuine truncated Lubin--Tate bracket attached to a unit power series sends a primitive level-n+1 point to another root of the same Eisenstein polynomial. This is the source of the finite-level Galois action; no auto…

The primitive level-n+1 polynomial is lifted from κ((T)) to κ[[T]]. Modulo T this lift is the single monomial Y ^ ((q - 1) q ^ n), while its constant coefficient is exactly T. It is therefore Eisenstein at (T), and Gauss…

The primitive factor Q(n+1) constructed in the preceding file has roots which are killed by the (n+1)-st Lubin--Tate iterate but not by the n-th iterate. This file chooses one such root in the fixed separable closure and…

This file constructs the finite-level Galois action of a power-series unit with the local-Artin orientation: a sends the chosen primitive generator to [a⁻¹]. Its kernel is the (n + 1)-st higher-unit subgroup, so the acti…

Public aggregate for the Lubin--Tate action and its division-module endomorphisms.

Division points do not in general lie in the base Laurent-series field. This file therefore constructs the same genuine brackets in an arbitrary ambient field A of the same characteristic, from a chosen coefficient embed…

For the standard equal-characteristic Lubin--Tate module, scalar brackets identify the endomorphism ring of the level-m division module with κ⟦T⟧/(T^m), and its automorphism group with the quotient of κ⟦T⟧ˣ by the m-th h…

This file proves the algebraic identities needed to turn the finite brackets from EqualCharacteristicLubinTateEnd into the action of (κ⟦T⟧ / T^n)ˣ on the T^n-division points.

After identifying an equal-characteristic local field with κ((T)), the Lubin--Tate polynomial used in the equal-characteristic construction is e(Y) = Y ^ q + T Y, where q = #κ. This file constructs e as an actual additiv…

Public aggregate for coefficient Frobenius, Laurent-series Frobenius, and the completed unramified field.

the completed unramified ring For a finite field k, arithmetic Frobenius acts on AlgebraicClosure k by the #k-power map and hence coefficientwise on (AlgebraicClosure k)[[T]]. These definitions belong to the completed ma…

field in equal characteristic For a finite field k, the equal-characteristic model of the completion of the maximal unramified extension of k((T)) is (AlgebraicClosure k)((T)). This file equips that field with the genuin…

The coefficient recursion in the proof of the contracting Frobenius equation repeatedly solves α - γ φ(α) = β in a complete discrete valuation ring, where γ has positive valuation. For an equal-characteristic power-serie…

extensions in equal characteristic For a finite extension l / k of finite fields, coefficientwise extension makes l((T)) a finite extension of k((T)) of the same degree. Every automorphism of l / k extends coefficientwis…

Public aggregate for higher-unit norms, containment of the standard subgroup in the finite-level norm subgroup, and the corresponding finite quotient calculation. The exact norm-subgroup equality, which uses finite local…

higher-unit fixed field For a coefficient unit in U^(n+1), the standard completed-level embedding lands in the completed theta-intertwining theorem fixed field. This leaf packages its canonical codomain restriction for t…

field The standard-level embedding is an equivalence because its source and target have the same degree (q - 1) q^n.

fixed field

embedding The standard level and the fixed field have the same finite degree (q - 1) q^n; hence the canonical injective embedding is surjective.

If a is congruent to one modulo T^(n+1), the completed the completed theta-intertwining theorem Frobenius attached to a acts trivially on the standard primitive (n+1)-division point.

level map

The power-series coefficient ring k[[T]] is the canonical integer ring of k((T)). The induced equivalence on units carries the explicit kernel used in the Lubin--Tate construction to the canonical principal-unit filtrati…

The fixed-field norm N(-pidelta) = aT from the completed theta-intertwining theorem is transported through the standard-level equivalence. Cancelling the already known norm T then puts every level-n+1 higher unit in the…

finite level This light leaf names the canonical base algebra and its norm subgroup once, so the later inclusion and index arguments do not repeat expensive fallback typeclass searches.

The higher-unit norm calculation and the uniformizer norm combine to give the division-level inclusion (T⁻¹) × U^(n+1) ≤ N(Ln/K).

The normalized Laurent uniformizer T⁻¹ is the inverse of the norm of the negative primitive Lubin--Tate division point. This light leaf isolates the valuation factor of the norm-subgroup calculation from the later openne…

At repository level n, reduction modulo T^(n+1) identifies the quotient of the power-series unit group by its explicit higher-unit kernel with the units of the truncated power-series ring. Its elements are parametrized b…

This file packages the genuine composite k[[T]]ˣ ≃ 𝒪[k((T))]ˣ → k((T))ˣ used in the sharp norm-subgroup calculation. Its range is the full valuation-zero unit subgroup, and it carries the explicit Lubin--Tate kernel to t…

Collects primitive points, their Galois displacements, and the resulting lower ramification groups.

The lower-group calculation is integrated here to compute the actual Herbrand function and the resulting upper ramification groups of the chosen equal-characteristic Lubin--Tate level.

This module computes the normalized additive valuation of the displacement of the chosen primitive Lubin--Tate point from the first visible coefficient of the corresponding unit parameter.

This module identifies the action of every finite-level Galois automorphism on the chosen primitive division point with the corresponding truncated Lubin--Tate bracket.

This module identifies the actual lower ramification groups attached to the chosen complete valuation, both by visible unit-parameter coefficients and by their exact cardinalities.

This module constructs the actual complete discrete valuation on an explicit finite equal-characteristic Lubin--Tate level. It proves that the chosen primitive point generates the integral closure and is a uniformizer.

This file packages the ceiling behavior of the chosen real lower filtration and the integral values of its inverse Herbrand function. Together they show that, on the positive range covered by an explicit finite Lubin--Ta…

Public aggregate for theta coefficients, the theta series, evaluation, and the first theta identity.

This file constructs the coefficient sources behind the power series theta in the equal-characteristic specialization of the equal-characteristic theta construction. For a finite field k, the completed maximal unramified…

The theta series of the completed theta-intertwining theorem has coefficients in (AlgebraicClosure k)[[T]]. This file evaluates it at a topologically nilpotent element of the valued integer ring of the completed unramifi…

For the normalization pi = T and barpi = u⁻¹ T, this file constructs the Lubin--Tate endomorphism [u] over the base integer ring k[[T]] and proves the first identity of Corollary the Lubin–Tate endomorphism commutation l…

The coefficient recursion of the contracting Frobenius equation produces a sequence bj in the completed maximal-unramified integer ring. The series used in the completed theta-intertwining theorem is the genuine sparse p…

This file proves the uniqueness lemma used for the first theta identity in the equal-characteristic specialization. The identity theta^phi = theta o [u] itself is a separate required endpoint.

Public aggregate for the characteristic-independent standard division polynomials, primitive torsion fields, analytic formal-module action, explicit finite Galois parameterization, integral-closure valuation, ramificatio…

The standard level for a uniformizer π and the standard level for a unit change uπ both live in the fixed separable closure of the base field. Their compositum therefore gives a literal common overfield. This file choose…

Let π be a uniformizer, let u be a unit with u - 1 ∈ m^(n+1), and put π' = uπ. The parameter difference π' - π then lies in m^(n+2). At the standard primitive level n + 1, whose ramification index is d = (q - 1) q^n, thi…

For a local field F, a chosen uniformizer π, and a valuation-ring unit u, the product uπ is again a uniformizer. Consequently all of the standard finite-level Lubin--Tate constructions are available for uπ. This file pac…

The scalar endomorphisms of a Lubin--Tate formal module are genuine infinite power series. This file evaluates them in the complete valuation ring of a standard finite level. The coefficient map is the canonical map of v…

At primitive level n + 1, the i-fold standard Lubin--Tate iterate has normalized additive valuation q ^ i for i ≤ n. The proof uses the two-term formula f(y) = y ^ q + π y. The first summand has valuation q ^ (i + 1). Th…

For a local field F and an element π of its valuation ring, this file packages the polynomial f(X) = X ^ q + π X, where q is the cardinality of the residue field. Its compositional iterates and the factors Qₙ(X) = (f^n)…

The parameter group at primitive level n + 1 is OFˣ / UF^(n + 1). The image of UF^k gives its natural decreasing filtration. For 1 ≤ k ≤ n + 1, that image has cardinality q ^ (n + 1 - k).

For a local field F, the unit parameters visible at primitive level n + 1 are the valuation-ring units modulo the higher principal-unit subgroup U^(n + 1). This file records that quotient, chooses representatives, and co…

The multiplicative equivalence between finite unit parameters and the Galois group transports the image of UF^k to a subgroup of the Galois group. This file records membership both for quotient parameters and for valuati…

The explicit lower ramification groups determine the slopes of the Herbrand function. Summing those slopes sends the lower breaks q ^ k - 1 to the integral upper breaks k. Consequently the upper ramification group at k i…

This file develops the quantitative inputs for comparing the standard level attached to a uniformizer π with the standard level attached to uπ, when u is a sufficiently deep principal unit. ChangedPrimitiveEvaluation sup…

The finite unit parameter group OF^ / UF^(n + 1) acts multiplicatively and faithfully on the primitive level-n + 1 division point. The finite-level automorphism calculation identifies this parameter group bijectively wit…

The finite unit parameters at primitive level n + 1 act on the chosen primitive division point. Once the resulting roots are regarded as elements of the simple level field, the canonical power basis lifts them to algebra…

The primitive roots defining the standard finite levels are chosen independently in one separable closure. Exact torsion and normality show that the resulting simple fields nevertheless form an increasing tower.

The standard level field is finite and Galois over the local base field. Consequently the complete discrete valuation selected from its integral closure is the unique extension of the base valuation. This is the bridge n…

For the canonical LocalField package attached to a nonarchimedean local field, the explicit complete-DVF valuation chosen in the standard Lubin--Tate construction is equivalent to the valuation chosen by the local upper-…

This file places the genuine real lower ramification filtration on a standard Lubin--Tate level. Since the integral closure is generated by the primitive Lubin--Tate uniformizer, membership at a natural index is detected…

The displacement formula for a primitive Lubin--Tate point identifies the lower ramification filtration with the principal-unit filtration transported to the finite-level Galois group. At the break q ^ k - 1, and through…

This file introduces the local norm subgroup attached to a standard finite Lubin--Tate level. The norm identity for the negative primitive generator shows that the chosen base uniformizer is an actual norm. Consequently…

The minimal polynomial of the chosen primitive level generator is the standard Eisenstein polynomial, whose constant coefficient is the base uniformizer. The power-basis norm formula therefore gives N(-lambda) = pi.

The standard polynomial fπ(X) = X ^ q + π X depends polynomially on its parameter. Hence two parameters which become equal after applying a ring homomorphism give the same polynomial, all the same compositional iterates,…

The formal scalar endomorphism [a] is in general an infinite power series. It is therefore evaluated on the primitive point only after that point has been placed in the complete integral closure constructed in PrimitiveU…

For the primitive point at level n + 1, a unit whose first nontrivial principal-unit layer is k displaces that point by an element of normalized additive valuation q ^ k. The analytic input is proved here rather than ass…

Let F be a local field, let π be a uniformizer, and put f(X) = X ^ q + π X, where q is the cardinality of the residue field. Reduction modulo the maximal ideal sends the n-fold compositional iterate of f to X ^ (q ^ n).…

For a local field F with uniformizer π, this file maps the primitive division polynomial from the valuation ring to the fraction field. Gauss's lemma transfers its Eisenstein irreducibility to the field. We also prove se…

This file records the exact torsion level of the primitive roots chosen in PrimitiveRoot. The standard division-polynomial iterates are first mapped from the valuation ring to the base field and to its fixed separable cl…

Let F be a local field, let π be a chosen uniformizer, and let Lₙ = K(λₙ) be the simple extension generated by a chosen root of the standard primitive division polynomial. This file puts the integral-closure complete dis…

A topology-first nonarchimedean local field carries the canonical valuation used by finite local reciprocity. This file packages that valuation as a LocalField and identifies its valuation ring and principal-unit filtrat…

This file names the lower filtration, Herbrand function, inverse Herbrand function, and genuine real upper ramification groups attached to the chosen integral-closure valuation on a standard finite Lubin--Tate level.

Public aggregate for the formal-series constructions used by Lubin--Tate theory: composition, linear terms, intertwiners, coefficient equations, reduction, the standard Lubin--Tate series, and the coefficientwise recursi…

For a positive degree, the scalar factor 1 - π ^ r is a unit whenever π is a uniformizer. Consequently the corresponding scalar coefficient equation has a unique solution in the valuation ring.

The coefficient of an intertwining defect in total degree at most m depends only on the coefficients of the proposed intertwiner in total degree at most m. This is the finite-degree continuity statement needed to pass fr…

For two Lubin--Tate series with the same prescribed linear coefficient, this module defines the multivariable intertwining equation and its additive defect.

A multivariable power series has a prescribed linear term when its difference from the corresponding linear form has total order at least two.

This module connects the two coefficient-level inputs for the recursive construction of a same-uniformizer Lubin--Tate intertwiner. Reduction makes every coefficient of the current defect divisible by the uniformizer. In…

The coefficient selected in RecursiveCoefficient is inserted as a single monomial. This file proves that the insertion preserves the prescribed linear term and cancels the defect coefficient in precisely that total degre…

For a fixed total degree there are only finitely many monomials. This file orders those monomials, applies the coefficient correction from RecursiveCorrection one at a time, and then iterates the resulting degreewise cor…

After reduction to the finite residue field, both series become the Frobenius power series. The two sides of the intertwining equation then agree, so every coefficient of the defect is divisible by the chosen uniformizer…

A Lubin--Tate power series over a chosen valuation ring has zero constant coefficient, prescribed linear coefficient, and reduces to the residue-field Frobenius power series. The chosen element is not required to be a un…

The recursive same-uniformizer intertwiner applied to the standard Lubin--Tate series produces the formal group law and all of its scalar endomorphisms. The structural identities are proved from the uniqueness of an inte…

For a uniformizer π, the polynomial power series π X + X ^ q, where q is the cardinality of the residue field, is a Lubin--Tate series. This gives the general formal-module construction a canonical polynomial input witho…

Aggregate for the multiplicative Lubin--Tate series and its completed-level, Frobenius, residue, fixed-field, and changed-uniformizer constructions.

Let k be an algebraic closure of ZMod p. The Witt ring W(k) is the integer ring of the completed maximal-unramified coefficient field used in the changed-uniformizer construction. Mathlib's WittVector.frobeniusRotation s…

This aggregate exposes the completed series, defect correction, intertwiner construction, scalar endomorphisms, and final semilinear compatibilities.

This module extends the multiplicative and changed-standard Lubin--Tate series to the completed unramified Witt ring and records their coefficients and residue reductions.

This module computes how a degreewise correction changes the semilinear substitution defect and constructs the unique coefficient that kills that defect.

This module builds compatible finite-degree approximations, assembles the changed-uniformizer intertwiner, proves its functional equation, and establishes uniqueness.

This module proves that the changed-uniformizer intertwiner commutes with every scalar endomorphism and identifies its coefficientwise Frobenius twist.

This module constructs the completed multiplicative and changed-standard scalar endomorphisms and proves their linear terms, composition laws, Frobenius invariance, and substitution commutation.

The completed level contains two finite abelian extensions of ℚ[p]: the image of the ordinary standard multiplicative Lubin--Tate level; the fixed field of the inverse-unit completed Frobenius lift, identified with the c…

Inside the finite standard/changed compositum, the cyclic subgroup generated by the inverse completed Frobenius has fixed field exactly the changed Lubin--Tate factor. Thus the automorphisms over the changed factor are p…

The finite standard/changed compositum is unramified over the completed changed-uniformizer fixed field. Its explicit relative Artin candidate is the restriction of inverse completed coefficient Frobenius. Both automorph…

The finite standard/changed compositum is realized inside the completed Lubin--Tate level. Uniqueness of the finite extension of the p-adic valuation therefore gives a canonical injection from its residue field into the…

The genuine changed-uniformizer theta point is a uniformizer of the ambient completed Lubin--Tate level. Uniqueness of finite separable extensions of the p-adic valuation transports this fact to both the changed fixed fi…

The completed Frobenius lift whose action on the standard primitive point is indexed by u⁻¹ is an actual ℚ[p]-automorphism. Its fixed field is exactly the finite changed-uniformizer Lubin--Tate level generated by the gen…

For a p-adic valuation-ring unit u, the primitive polynomial attached to the changed uniformizer u p remains Eisenstein after extension to the completed-unramified Witt valuation ring. Consequently the genuine theta valu…

The Frobenius lift whose primitive-point action is indexed by the inverse unit is the genuine diagonal action relevant to change of uniformizer. Semilinear evaluation changes theta coefficients by Witt Frobenius, while t…

The completed unit-indexed Frobenius lift preserves the actual integral closure valuation ring. Its restriction is continuous for the maximal- ideal adic topology and transports convergent Witt-coefficient power-series e…

Arithmetic Frobenius on the completed maximal-unramified p-adic field fixes the standard primitive Lubin--Tate polynomial, since that polynomial descends to ℚ[p]. Using the completed primitive power basis, it therefore e…

For the completed maximal-unramified coefficient field E = Frac(W(AlgebraicClosure (ZMod p))), this file base-changes the standard primitive Lubin--Tate polynomial from ℚ[p] to E and takes its actual splitting field. The…

The completed level is defined as the splitting field of the standard primitive Lubin--Tate polynomial over the completed maximal-unramified field. This file identifies all of its roots with the genuine finite unit-param…

The standard multiplicative Lubin--Tate primitive polynomial remains Eisenstein after extending its integer coefficients to the valuation ring of the completed maximal unramified field. In particular it remains irreducib…

The primitive multiplicative Lubin--Tate polynomial remains Eisenstein over the completed-unramified valuation ring. This file uses that actual Eisenstein equation and the fundamental ramification identity to prove that…

The completed multiplicative Lubin--Tate level is totally ramified over its completed-unramified coefficient field. Hence the canonical residue map is an isomorphism. Under this identification, every unit-indexed complet…

The ordinary standard Lubin--Tate level embeds in the completed level by sending its primitive generator to the chosen completed primitive point. This file proves that the embedding also preserves the integral analytic a…

The coefficient ring used by the mixed-characteristic changed-uniformizer construction is W(AlgebraicClosure (ZMod p)). Its fraction field is the completed maximal-unramified coefficient field. This file equips that exis…

Witt Frobenius on W(AlgebraicClosure (ZMod p)) has exactly the canonical copy of ℤ[p] as its fixed ring. Passing to fraction fields shows that the arithmetic Frobenius on the completed maximal-unramified coefficient fiel…

Collects finite-level evaluations and primitive roots together with completed coefficient evaluations, scalar endomorphisms, and primitive points.

This module equips completed Lubin--Tate levels with the direct p-adic coefficient maps used by polynomial and power-series evaluation. It also establishes the exact completed primitive-point torsion relations and the ge…

This module evaluates the completed multiplicative comparison at the chosen completed standard primitive point. It proves the exact standard and changed-uniformizer torsion bounds and constructs the actual unit action on…

This module extends the standard-to-multiplicative comparison and scalar endomorphisms to the completed unramified Witt ring. It proves the genuine composition, torsion, and injectivity identities for their analytic acti…

This endpoint evaluates the genuine changed-uniformizer intertwiner at the completed multiplicative primitive point. It proves the exact scalar, Frobenius, root, and level-embedding identities used by the completed Lubin…

This module evaluates the standard-to-multiplicative Lubin--Tate comparison on topologically nilpotent integers in a standard finite level. It proves the functional equation, compatibility with scalar endomorphisms, the…

The evaluated multiplicative point yields an actual primitive p ^ (n + 1)-st root of unity. This module proves its exact order and identifies the genuine finite-level Galois action with the cyclotomic power action.

The characteristic-independent same-uniformizer recursion supplies the canonical series with linear coefficient 1 satisfying (1 + X)^p - 1) = H(pX + X^p). Consequently, evaluation of H carries standard Lubin--Tate divisi…

Mathlib's binomial series at the natural exponent p is (1 + X) ^ p. After subtracting 1, this has zero constant coefficient, linear coefficient p, and reduction X ^ p. Thus it is the Lubin--Tate series attached to the mu…

Public root for reusable finite and profinite ramification infrastructure. It is downstream of ValuationTheory and LocalFieldTheory and upstream of local class field theory.

Focused aggregate for valuation-subring actions and their ramification groups.

Decomposition groups, inertia groups, fixed fields, and tower formulas for primes in finite Galois extensions of Dedekind domains.

For an abelian Galois extension of ℚ, all primes above one rational prime have the same inertia group: primes above the same rational prime are conjugate, and conjugation is trivial in an abelian group. Consequently, if…

The preceding fixed-field lemma shows that a subgroup containing all inertia groups has an everywhere-unramified fixed field. Minkowski's discriminant bound makes that fixed field equal to ℚ, and Galois correspondence th…

An extension w of the rational p-adic absolute value determines a valuation subring of a number field M. This file synchronizes that valuation subring with a concrete prime ideal of 𝓞 M, proves that the prime lies over (…

This file identifies the inertia cardinality of the canonical valuation on a finite Galois extension of ℚp with the intrinsic value-group ramification index, then applies the prime-power cyclotomic ramification bound.

A cyclotomic field of order r p ^ n, with r prime to p, splits into an unramified prime-to-p branch and a p-power branch. This file records that only the latter contributes to the local ramification index.

The localization constructed in is transported from the absolute value completion of ℚ to the concrete field ℚp. Uniqueness of the absolute-value extension identifies its valuation ring with the canonical norm-formula va…

Stable reader-facing statements of the main class field theory results.

The local norm condition is satisfied at the conductor exponent and at every larger exponent, and at no smaller exponent. The norm is taken from the whole completion tensor algebra, with no arbitrary place above v.

The finite exponent of the conductor is characterized by the determinant norm from Kv ⊗[K] L. This formulation does not choose a place of L above v; the implementation proves that the tensor norm image agrees with the no…

The finite support is exactly the set of base primes ramified somewhere upstairs. This does not identify an arbitrary defining ray modulus with the minimal conductor.

The conductor of the ray class field for a modulus m is bounded above by m. Equality need not hold: a modulus may contain redundant conditions.

For a finite abelian number-field extension, the conductor exponent at a finite place is at most one exactly when the residue characteristic does not divide the ideal-theoretic ramification index at any place above it.

This All module collects the implementation-independent finite class-field correspondence for ray-class subgroups, full ray class fields, their degree and prime-splitting formulas, and conductor minimality. Each theorem…

The existential definition of EmbedsInRayClassField is independent of which Frobenius-normalized realization is chosen. It does not assert uniqueness of the embedding itself.

Let L/K be finite abelian. Its conductor is the least modulus whose ray class field contains L. Since the public interface makes no global choice of ray class fields, the theorem asserts existence of this least modulus.

The conductor of a finite abelian extension is the least modulus whose ray class field contains that extension. The older theorem name embedsInRayClassFieldiffconductorle remains available for compatibility; its conclusi…

Reducing the modulus yields an embedding of ray class field realizations that intertwines their Artin maps.

Existence of a least ray-class-field modulus and uniqueness of any modulus with the same universal property combine into a unique-existence statement.

At a finite prime of the base, the exponent of the norm is the sum of the upstairs exponents, each weighted by its inertia degree. This is the calculation needed when passing from ideals to norm-defined ray subgroups.

A finite abelian extension has at most one modulus that characterizes exactly the ray class fields containing it.

A larger modulus has at least as strong a congruence condition at each finite prime and at least as many real positivity conditions.

At the modulus with no finite part and every real place selected, the ideal-theoretic ray class group is the narrow class group. The comparison preserves the class of each finite prime.

At the modulus with no finite or real conditions, the ideal-theoretic ray class group agrees with Mathlib's ideal class group. The comparison also preserves the class of each finite prime, fixing its arithmetic meaning.

An embedding between two realizations of ray class fields intertwines the Artin action with the canonical projection of ray class groups. The statement uses only Mathlib and public Definitions vocabulary; the idelic impl…

For any ray class field realization of m, its degree is the cardinality of the ideal-theoretic ray class group. The realization is explicit, so this module does not depend on an implementation-level choice of field.

The modulus projection produces an embedding of realizations. Normality upgrades that embedding to literal inclusion in the fixed separable closure.

For a prime away from the modulus, the Frobenius-normalized Artin isomorphism identifies complete splitting with triviality of the corresponding ray class.

For a modulus m, there exists a finite abelian extension whose Galois group is the ideal-theoretic ray class group modulo m, compatibly with finite global reciprocity. No global choice of ray class field is exposed.

The comparison with the idèlic ray class group identifies this group with a quotient by a finite-index congruence subgroup, so it is finite for every modulus.

Finite primes away from the modulus generate enough of the ideal-theoretic ray class group to determine any homomorphism into a commutative group.

The kernel in prime-to-modulus ideals is the product of the genuine ideal norm image and the principal ray-ideal subgroup.

An ideal prime to the larger modulus represents the same prime ideal after projection to the ray class group of the smaller modulus.

The direct ideal-quotient projection agrees with the natural idelic quotient projection because both preserve every prime class outside the larger modulus. The latter projection is directly surjective since both ray clas…

This is the ideal-theoretic norm-kernel form of finite abelian reciprocity. The ideal norms are norms of fractional ideals prime to the modulus; the principal ray ideals are absorbed by the ray quotient.

This is the forward direction of the ideal-theoretic norm-kernel formula. The subgroup is formed from actual fractional-ideal norms, not from idèle norms. Equality requires the separate reverse approximation theorem.

The degree of a finite abelian class field is the index of its defining subgroup in the ray class group.

For a fixed modulus, inclusion of ray-class subgroups reverses inclusion of their finite abelian class fields. The embedding between arbitrary Frobenius-normalized realizations intertwines both Artin actions.

Every subgroup of an ideal-theoretic ray class group is the kernel of the Frobenius-normalized Artin map of a finite abelian extension. The statement uses ideal classes; the proof transports the existing idelic reciproci…

The fields are intermediate fields of one fixed separable closure, so the conclusion is literal inclusion rather than merely an abstract embedding.

Away from the modulus, the residue degree is the order of the prime ray class modulo the subgroup defining the extension.

At a prime away from the modulus, complete splitting is equivalent to membership of the prime's ray class in the defining subgroup.

The quotient of a ray class group by the subgroup defining a class field is the Galois group of that field.

The quotient isomorphism retains the prescribed Artin normalization.

The class field is independent of the Frobenius-normalized realization as an actual intermediate field, not just up to abstract isomorphism. This does not assert uniqueness of the embedding or of the Artin map.

The field attached to a fixed modulus and subgroup is well-defined up to K-algebra equivalence. The equivalence is not claimed to be unique.

An element of the n-th higher-unit group is an integral unit congruent to 1 modulo the n-th power of the maximal ideal. This also applies at n = 0, where the condition reduces to being an integral unit.

At positive depth, every element of 1 + 𝔪ᵛⁿ is automatically a unit in the local integer ring. Consequently no integral-unit witness is needed in the membership criterion below.

For every depth, including zero, the higher-unit subgroup is open in the multiplicative group of the finite completion.

The ray-congruent generators already form a subgroup under the principal ideal map, so taking their subgroup closure adds no new ideals.

The local congruence condition makes the corresponding principal idèle integral-unit-valued at every finite prime in the modulus support.

This All module collects the Mathlib-native arithmetic Frobenius statements and the intrinsic existence, Artin isomorphism, degree, splitting, and principalization results for small and big Hilbert class fields.

An automorphism of an abelian extension may move a prime above a fixed base prime. At an unramified prime, the arithmetic Frobenius element is unchanged. The prime transport is Mathlib's equivalence of height-one spectra…

In a finite abelian extension, the Frobenius at an unramified prime is the identity exactly when the base prime splits completely. Complete splitting is expressed only with Mathlib's ramification indices and residue degr…

At an unramified prime of an abelian extension, all primes above the same finite base prime give the same canonical arithmetic Frobenius element. This is the equality, rather than merely conjugacy, needed to avoid choosi…

This statement exposes Mathlib's intrinsic arithmetic Frobenius, rather than an element named through a particular implementation of the global Artin map. It is therefore the precise bridge to IsArithFrobAt that downstre…

For a prime w of L above v of K, unramifiedness kills the inertia subgroup. The arithmetic Frobenius therefore has order equal to the residue degree at w.

At a prime unramified in the top field, restriction of arithmetic Frobenius to an intermediate field is arithmetic Frobenius at the prime below it.

The narrow ideal class group is isomorphic to the Galois group of the big Hilbert class field. The displayed compatibility with arithmetic Frobenius fixes the Artin normalization of the isomorphism.

The degree of any extension satisfying the intrinsic big-Hilbert-class-field property is the order of the narrow ray class group. The latter is the ray class group for the modulus containing every real place and no finit…

The big Hilbert class field is characterized intrinsically as a finite abelian extension unramified at every finite prime and containing every other finite abelian extension with that property. No particular field chosen…

Its narrow-class Artin isomorphism and unramifiedness at finite primes give a ray-class-field realization whose extension is the original field.

A finite prime splits completely in the big Hilbert class field precisely when its narrow ideal class is trivial. Real-place ramification does not affect this finite-prime criterion.

A finite prime splits completely in the big Hilbert class field exactly when its fractional ideal has a totally positive generator.

Maximality among finite-prime-unramified abelian extensions determines one intermediate field of the fixed separable closure.

The Frobenius-normalized realization of the narrow ray class group is maximal among finite abelian extensions unramified at finite places.

The Frobenius-normalized realization of the ordinary ray class group is maximal among finite abelian extensions unramified at all places.

When the base has no real places, no extension can ramify at an infinite place. Thus the small and big Hilbert class field conditions agree.

The ordinary ideal class group is isomorphic to the Galois group of the small Hilbert class field. The displayed compatibility with arithmetic Frobenius fixes the Artin normalization of the isomorphism.

Any extension satisfying the intrinsic small-Hilbert-class-field property has degree equal to the ordinary class number of the base field.

Everywhere-unramified extensions are unramified at finite places, so the maximality property of a big Hilbert class field supplies the embedding.

The small Hilbert class field is characterized as an everywhere-unramified finite abelian extension containing every other such extension. In particular, real places are required to remain unramified.

The extensions are intermediate fields of one separable closure, so the result is literal containment, not only an abstract embedding.

Its ordinary-class Artin isomorphism and everywhere-unramifiedness give a ray-class-field realization whose extension is the original field.

A finite prime splits completely in the Hilbert class field precisely when its fractional ideal class is trivial. Both sides use Mathlib's native ideal-theoretic objects.

The principal ideal theorem says that extension to the Hilbert class field makes every integral ideal of the base number field principal.

The maximality condition determines an actual intermediate field, not merely an isomorphism class. It does not distinguish a unique field automorphism.

The intrinsic maximality condition determines a small Hilbert class field up to an isomorphism over the base. This asserts existence of an isomorphism, not a distinguished or unique choice of one.

This module collects finite ideal-theoretic reciprocity and the topological maximal-abelian statements. The latter are proved via topological comparison with the existing restricted-product implementation.

For a finite abelian extension L/K, global reciprocity supplies a modulus and a surjective Artin map from its ray class group to Gal(L/K). The extension is unramified away from that modulus, and prime classes are sent to…

The kernel of a finite ray-class Artin map is exactly the relation that must be divided out to obtain the Galois group. The modulus and Frobenius normalization are carried by FiniteAbelianReciprocityData.

The induced isomorphism maps the class of a ray class to its Artin value.

The finite-place local Artin construction is made on an algebraic localization inside a completion. In finite degree that localization is the whole completion. This theorem transports the independent local Artin map to t…

This is a Mathlib-typed local--global compatibility statement. Restricting one global Artin map along Mathlib's one-place idèle-class homomorphism has the local tensor-norm group as its kernel. It specifies the kernel at…

The canonical one-place map into an ideal-theoretic ray class group has the actual local norm subgroup as its Artin kernel. Its Artin values preserve the absolute-value class of one extension of that place to the top fie…

The ray map comes from the one-place idèle class, while the local Artin map comes from local reciprocity on the completed extension. The transport from local automorphisms to the global Galois group is characterized on t…

The local-to-ray map is constructed from a one-place idèle class. This statement compares the kernel of the resulting ray-class Artin map with the determinant norm of the entire local tensor algebra, at every finite plac…

This map from Mathlib's idèle class group to Mathlib's abelianized absolute Galois group is continuous, surjective, and has the identity component as its kernel. It is induced by a topological reciprocity isomorphism. Th…

For a number field K, the idèle class group modulo its identity component is topologically isomorphic to the maximal abelian quotient of the absolute Galois group. The statement uses Mathlib's groups on both sides.

Public Hasse--Arf theorem and basic lower-filtration identities.

Let L/K be a finite abelian extension of nonarchimedean local fields, with the valuation of L extending that of K. If n is a jump in the lower ramification filtration, the corresponding upper index is the Herbrand value…

The sum starts at index one: the increment from n to n + 1 is the cardinality of the next lower group divided by that of the zeroth group.

The finite-sum Herbrand value is nonnegative at every integral lower index. For a finite Abelian extension of nonarchimedean local fields, Hasse--Arf therefore makes the value at each lower jump a natural number.

For a finite extension, each lower ramification group is finite and nonempty. Thus every increment of the rational Herbrand function is strictly positive. This does not assert integrality of its values.

The piecewise function defined from the public integral lower groups agrees with the existing Herbrand function of the local lower filtration. Its strict growth is consequently available without exposing that filtration…

The public upper filtration is transported to the existing local upper filtration in the implementation layer, including its right limit.

The definition uses powers of the maximal ideal of a valuation subring. The inclusion below holds without local-field or finiteness hypotheses.

For a finite field extension and a Noetherian valuation subring, each nonidentity automorphism moves an element of the valuation ring by a nonzero amount. Krull's intersection theorem then excludes that automorphism from…

Every level of the lower ramification filtration is normal in the decomposition group: conjugation preserves the maximal-ideal powers that define the filtration.

Mathlib defines inertia through the action on the residue field. The valuation-subring definition of G₀ uses the equivalent condition that every difference σ • x - x belongs to the maximal ideal.

Upper groups are real lower groups evaluated at inverse Herbrand indices, so their normality follows from normality of the real lower groups.

The real-index filtration is decreasing directly from the antitonicity of powers of the maximal ideal. No choice of a local extension is needed.

Conjugation preserves powers of the maximal ideal, so the real lower groups are normal in the decomposition group.

The public inverse Herbrand identity identifies the upper group at φ(s) with the public real lower group at s.

The public real lower group agrees with the original natural-index lower group at each integer. Eventual triviality then passes to upper numbering through the Herbrand-index identity and antitonicity.

This All module collects the power-class quotient theorem, existence and the norm-residue criterion for local Hilbert pairings, and existence of a coherent family satisfying the global product formula.

The set is defined by three explicit valuation conditions, independently of any choice of local Hilbert symbols or of a larger auxiliary support.

The norm-residue criterion determines exactly where a local symbol equals one, even though it does not determine the symbol's other values. Hence the finite support of one constructed family transfers to every family sat…

The norm-residue criterion determines the zero set of every such family, even though it does not determine all of its nontrivial values.

When the power-class group is finite and the field contains a primitive n-th root of unity, its full group of μₙ-valued characters has the same order. Hence a nondegenerate pairing gives an equivalence with that dual.

A Hilbert pairing is a homomorphism in each power-class argument. These formulas expose that structure directly on representatives in Kˣ.

The symbol is multiplicative in its second representative.

For a number field containing the n-th roots of unity, local class field theory supplies a Hilbert pairing on every finite completion. These pairings can be chosen coherently: their values on two nonzero elements of the…

When the n-th roots of unity lie in the base field, the finite field factors of the Kummer algebra are all isomorphic. We choose one factor and reindex the product by Fin (n / d), where d is that factor's degree.

The quotient by X ^ n - a is finite étale when the exponent is invertible in the base field. This includes reducible polynomials: the algebra need not be a field.

The polynomial X ^ n - a is monic for positive n. Its quotient algebra is finite free even when that polynomial is reducible, so no field assumption is placed on the Kummer algebra.

The rank of K[X] / (X ^ n - a) is n regardless of whether the polynomial is irreducible. This is distinct from the index of its norm subgroup.

The canonical algebra K[X] / (X^n - a) need not be a field. When K contains the n-th roots of unity and n is nonzero in K, its norm image on units nevertheless agrees with the norm image of a field generated by an n-th r…

The degree of K[X] / (X^n - a) is always n, but its norm image can have smaller index. Over a nonarchimedean local field containing the n-th roots of unity, the index is instead the degree of the simple field generated b…

The algebra norm of a possibly reducible Kummer algebra is the product of the norms of its finite separable field factors. The factors may have different degrees; no factorwise norm-image assertion is made.

Even when its rank is n, the algebra K[X]/(Xⁿ-1) has surjective norm under the local Kummer hypotheses. This is the simplest instance showing that norm index and algebra rank are different invariants.

When the exponent is invertible, the possibly reducible algebra K[X] / (X ^ n - a) is a finite product of finite separable simple field extensions. This applies in particular when a = 1.

When the n-th roots of unity lie in the base field, every field factor of the Kummer algebra has the same positive degree d. The total rank n is the number of factors times d.

If the base field contains the n-th roots of unity, every field factor of K[X] / (X ^ n - a) is a splitting field of the same polynomial. Thus all factors in the finite product decomposition are isomorphic over the base.

The order of the class of a is the degree of the field generated by an n-th root of a. The associated Kummer algebra need not be a field: in particular, the class of a = 1 has order one even when the algebra has rank n.

The pairing and the Artin maps in this theorem are chosen together. The algebraic pairing laws alone do not determine the values in μₙ(K).

Let K be a nonarchimedean local field containing the n-th roots of unity, with n nonzero in K. The local Hilbert symbol descends to a bimultiplicative pairing Kˣ / (Kˣ)^n × Kˣ / (Kˣ)^n → μₙ(K). The theorem below records…

Pairings constructed from the same arithmetic local Artin maps can be chosen compatibly when m ∣ n. Their values are compared in Kˣ, since they belong to different roots-of-unity subgroups. The public norm criterion plac…

The algebraic laws and norm-vanishing criterion are invariant under inversion of every value. Thus these conditions alone do not distinguish the value convention used by a normalized local Artin map. This theorem does no…

The vanishing of a local Hilbert symbol is equivalent to a concrete Kummer norm condition. The Kummer algebra is the canonical Mathlib quotient K[X] / (X^n - a), so the statement does not choose a root in an algebraic cl…

For a nonarchimedean local field in which n is nonzero and the n-th roots of unity are present, the Hilbert pairing identifies power classes with all μₙ-valued characters of the power-class group.

Two representatives have the same power class precisely when their ratio is an n-th power.

For a field K and a positive integer n, PowerClassGroup K n is the quotient of Kˣ by the subgroup of n-th powers. A class is the identity exactly when its representative belongs to the power subgroup.

The nonzero residue of the exponent in a nonarchimedean local field makes its multiplicative n-th-power quotient finite. This is the finiteness input for turning a nondegenerate Hilbert pairing into a perfect pairing.

The quotient map to power classes preserves inverses.

The quotient map to power classes preserves multiplication.

The quotient map to power classes preserves powers.

When the base field contains the n-th roots of unity, the quotient σ(u) / u depends only on u ^ n. In particular, the Artin root quotient used to normalize a local Hilbert symbol does not depend on the root chosen.

Let L be a number field that is finite abelian over ℚ. Kronecker--Weber asserts that L is contained in a cyclotomic extension: there is a positive integer n and a ℚ-algebra embedding of L into ℚ(ζₙ). The positivity condi…

This module gathers the public local reciprocity, local existence, and norm-subgroup statements. The theorem statements use Mathlib and the public definitions layer; their proofs may import implementation modules.

Finite local reciprocity implies that the subgroup of nonzero field norms has finite index in the multiplicative group of the base field.

For a finite abelian extension of a nonarchimedean local field, the subgroup of nonzero field norms is open in the multiplicative group of the base.

Transporting both fields of a finite extension through compatible ring equivalences preserves the actual field norms, not merely their index.

The norm from a larger field factors through the norm from every intermediate field. Thus enlarging a finite extension can only shrink its subgroup of norms in the base field. No local-field or Galois assumption is neede…

This module states the existence half of finite abelian local class field theory. Both sides of the correspondence are expressed directly with Mathlib objects: intermediate fields of SeparableClosure K and subgroups of K…

This module states the classification form of local existence for a nonarchimedean local field K. Finite abelian intermediate fields of SeparableClosure K are ordered by field inclusion, whereas open finite-index subgrou…

This module states local reciprocity for a finite abelian extension L / K of a nonarchimedean local field. The assumptions provide the finite abelian-Galois extension together with the valuative topology on K. The conclu…

The finite-level Artin maps can be chosen simultaneously for all finite abelian subextensions of a fixed separable closure. Their norm kernels and restriction compatibility refer to the same family, not to independently…

For an unramified member of one coherent finite local Artin family, the inverse of every uniformizer maps to the unique Galois automorphism whose reduction is the arithmetic q-power Frobenius. The uniqueness clause is es…

Norm kernels and tower compatibility alone leave an orientation ambiguity at finite levels. Arithmetic Frobenius on unramified extensions removes it for the entire coherent family, including ramified extensions.

The same family has norm kernels and restriction compatibility, and at each unramified valued realization sends an inverse uniformizer to arithmetic Frobenius on the residue field. The local-field structures on an interm…

The index of the norm subgroup equals the degree of the finite abelian local extension. This is the numerical form of the reciprocity isomorphism.

This module states the quotient formulation of local reciprocity for a finite abelian extension L / K of a nonarchimedean local field. Under the finite-dimensional, abelian-Galois, valuative, and topological assumptions,…

The existence statements for the finite Artin map and the norm-quotient isomorphism alone do not say that their witnesses agree. Here a single canonical Artin map is chosen, and its quotient isomorphism is characterized…

The first isomorphism theorem determines the quotient equivalence from any specified continuous surjective homomorphism with the field-norm kernel. This is distinct from uniqueness of the Artin map itself.

The canonical finite local Artin maps are compatible with restriction in a tower of finite abelian extensions. This is stronger than separately choosing the maps supplied by the finite-level existence theorem; the proof…

Two finite local reciprocity families with the norm kernels and arithmetic Frobenius residue normalization agree on every unramified valued member. This does not assert uniqueness on ramified members of the families.

For a fixed finite unramified abelian extension, the norm subgroup contains every integer unit. The decomposition of a field unit into an integer unit and a power of an inverse uniformizer therefore determines a homomorp…

For an unramified finite abelian extension, one and the same Artin map is surjective, has the field-norm kernel, and sends every inverse uniformizer to the arithmetic Frobenius on residues. The statement uses only Mathli…

This module gives the concrete meaning of the public predicate IsFieldNorm. For a finite-dimensional extension of fields L / K and a unit x of K, it states that x belongs to the range of the unit-valued field norm exactl…

For a nonarchimedean local field K, the profinite completion of Kˣ with respect to its open finite-index normal subgroups is continuously multiplicatively equivalent to the topological abelianization of Mathlib's absolut…

This module gathers the public local-global principles for field norms.

The tensor algebra Kv ⊗[K] L is a product of the completions of L at the absolute values above v. Its determinant norm is the product of the norms of those components. The theorem exposes the decomposition and norm formu…

The finite product decomposition sends a pure tensor to the product of its two canonical images in each completion. This specifies the same algebra equivalence that appears in the determinant-norm product formula.

The positivity condition is vacuous at a complex place. Consequently every nonzero base-field element is a determinant norm from the whole archimedean tensor algebra.

This module states the local-to-global norm principle for a finite cyclic Galois extension L / K of number fields. For a unit x of K, the conclusion identifies membership in the global field-norm subgroup with the condit…

This module states the elementary local consequence of being a global field norm. The assumptions give a finite extension L / K of number fields and a unit x of K. The conclusion says that if x lies in the global norm su…

At such a place the determinant norms from the full archimedean tensor algebra are exactly the positive real elements. In particular this does not incorrectly replace the tensor norm by a separate condition at every fact…

At a real place which becomes complex, the determinant norm from the whole archimedean tensor algebra cannot be negative. The tensor algebra, rather than a single chosen completion, is the object in the public statement.

For a finite field extension L / K, the norm of y : L is unchanged by base change, in the sense that the determinant norm of 1 ⊗ y over a commutative K-algebra A is the image of its field norm over K. This applies to the…

For a finite abelian extension, the determinant norm from the whole archimedean tensor algebra is surjective when the base place is unramified in the extension.