ModuleArithmeticFrobenius.lean
Nyll.ValuedFieldTheory.LocalField.Padic.Cyclotomic.Unramified.ArithmeticFrobenius
37 declarations indexed from sourceView source ↗ Module documentation
Arithmetic Frobenius on the unramified cyclotomic extension
Let K be a complete discretely valued field with finite residue field k = F_q, let ζ be a primitive n-th root of unity, and suppose that n is prime to the residue characteristic. the unramified cyclotomic theorem states that K(ζ) / K is unramified of degree the order of q modulo n, identifies its Galois group with the residue Galois group and arithmetic Frobenius, and proves O_{K(ζ)} = O_K[ζ].
The proof follows the arithmetic construction directly and uses no comparison certificate:
- the exact least-positive-exponent characterization of the order of
q
modulo n;
- the cyclotomic polynomial as the primitive separable integral model in the
the unramified base-change theorem Hensel core, giving unramifiedness and the degree formula;
- the canonical reduction homomorphism from field automorphisms to residue
automorphisms, with injectivity from uniqueness of simple Hensel lifts and surjectivity from the genuine Galois cardinalities;
- arithmetic Frobenius, its formula
ζ ↦ ζ^q, and generation of the Galois
group;
- the reverse integral-ring inclusion by residue generation, ramification
index one, and Nakayama, yielding O_{K(ζ)} = O_K[ζ].
Declarations
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedResidueDegree
DocumentationThe integer f in the unramified cyclotomic theorem: the multiplicative order of the residue cardinality q modulo n.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedResidueDegree_pos
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedResidueDegree_modEq_one
DocumentationThe defining exponent satisfies q^f = 1 mod n.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedResidueDegree_le_of_modEq_one
DocumentationMinimality of the exponent in the unramified cyclotomic theorem.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedResidueDegree_isLeast
DocumentationLiteral least-positive-natural-number formulation of the degree in the unramified cyclotomic theorem(i).
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_primitiveRoot_isIntegral
DocumentationA root of unity is integral over any coefficient ring acting on its ambient field. This is the element-level source for the unramified cyclotomic theorem(iii).
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_isIntegralClosure_of_subring_eq
DocumentationTurn a literal equality with the integral closure into the standard IsIntegralClosure instance.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_eq_of_roots_of_residue_eq_of_derivative_isUnit
DocumentationTwo simple roots over a local domain which have the same residue class are equal. This is the uniqueness half of Hensel's lemma, in the small generality needed for the residue-action comparisons below and in the generic unramified support lemma for the unramified cyclotomic theorem.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_galIntegerRingEquiv
DocumentationRestriction of a K-automorphism to the target valuation ring. The target ring is the integral closure of the Henselian base valuation ring, so this restriction is canonical.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_galIntegerRingEquiv_apply
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedResidueField
DocumentationThe residue field attached to an exponential valuation.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedResidueAlgebra
DocumentationThe canonical residue-field algebra structure of a valuation extension.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_residueFiniteDimensional
DocumentationFinite-dimensionality of the residue extension, transported to the module structure induced by padicCyclotomicUnramifiedResidueAlgebra.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_exponentialResidueDegree_eq_finrank
DocumentationThe residue degree uses the quotient-induced module structure; this identifies it with the finrank for padicCyclotomicUnramifiedResidueAlgebra.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
omit [FiniteDimensional K L] in
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_residueMapEquiv_commutes
DocumentationA ring equivalence of a local extension which fixes the base ring induces an algebra equivalence of residue fields.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_galResidueAlgEquiv
DocumentationThe canonical action of Gal(L/K) on the residue extension.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_galResidueAlgEquiv_residue
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_galToResidueGal
DocumentationThe canonical residue action as a group homomorphism.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section CanonicalResidueAction
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_isGalois_of_primitiveRoot_adjoin_eq_top
DocumentationA field generated by a primitive root of unity is normal; together with separability this gives the Galois input used in the unramified cyclotomic theorem(ii).
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_order_pos
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section FiniteResidueCyclotomic
variable {k : Type u} {Ω : Type v}
variable [Field k] [Fintype k] [Field Ω] [Algebra k Ω]
variable {p r n : ℕ} [hp : Fact p.Prime]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_residue_adjoin_finrank
DocumentationFinite-field degree calculation underlying the unramified cyclotomic theorem(i).
If k has cardinality p^r and ζ is a primitive n-th root in an extension field, then the simple residue extension k(ζ) has degree equal to the order of p^r modulo n. This is the irreducible-factor calculation used after reducing the cyclotomic polynomial.
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section FiniteResidueCyclotomic
variable {k : Type u} {Ω : Type v}
variable [Field k] [Fintype k] [Field Ω] [Algebra k Ω]
variable {p r n : ℕ} [hp : Fact p.Prime]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_residue_frobenius_apply
DocumentationArithmetic Frobenius on a finite residue extension acts by the q-th power, with q = p^r. This is the action asserted in the unramified cyclotomic theorem(ii).
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section FiniteResidueCyclotomic
variable {k : Type u} {Ω : Type v}
variable [Field k] [Fintype k] [Field Ω] [Algebra k Ω]
variable {p r n : ℕ} [hp : Fact p.Prime]
omit hp in
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_residue_adjoin_galois_generated_by_frobenius
DocumentationFor the residue cyclotomic field k(ζ), arithmetic Frobenius generates the full Galois group, and the number of powers needed is the least f from the unramified cyclotomic theorem(i).
Source context 9 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section FiniteResidueCyclotomic
variable {k : Type u} {Ω : Type v}
variable [Field k] [Fintype k] [Field Ω] [Algebra k Ω]
variable {p r n : ℕ} [hp : Fact p.Prime]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_finiteUnramifiedExtension
Documentationthe unramified cyclotomic theorem(i), local Hensel step.
For a Henselian exponential valuation with finite residue field of cardinality p^r, adjoining a primitive n-th root of unity, with p prime to n, is a finite unramified extension in the literal sense of the finite unramified-extension definition. The primitive integral model used here is the cyclotomic polynomial itself; its reduction is separable because n is nonzero in the residue field.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_finrank_eq_residueDegree
Documentationthe unramified cyclotomic theorem(i), degree calculation upstairs.
The integral minimal polynomial of ζ has irreducible reduction by the Hensel step of the factor-lifting criterion. That reduction is an irreducible factor of the n-th cyclotomic polynomial over the finite residue field, so all of its irreducible factors have degree ord_n(p^r).
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_galToResidueGal_injective
DocumentationThe canonical reduction homomorphism on Galois groups is injective for the prime-to-residue-characteristic cyclotomic extension. If two automorphisms have the same residue action, their images of ζ are simple roots of the cyclotomic polynomial with the same residue, hence are equal by Hensel uniqueness; ζ generates the field.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_galToResidueGal_bijective
Documentationthe unramified cyclotomic theorem(ii), canonical Galois comparison: the reduction homomorphism is bijective. Injectivity is the Hensel-uniqueness argument above; surjectivity follows by comparing the two genuine Galois group cardinalities with the equal field and residue degrees from part (i).
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_galEquivResidueGal
Documentationthe unramified cyclotomic theorem(ii): the canonical multiplicative equivalence obtained from reduction of valuation-ring automorphisms.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedArithmeticFrobenius
DocumentationThe arithmetic Frobenius in Gal(K(ζ)/K), defined canonically as the inverse image of finite-field Frobenius under the reduction equivalence.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_galEquivResidueGal_arithmeticFrobenius
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedArithmeticFrobenius_apply_primitiveRoot
Documentationthe unramified cyclotomic theorem(ii): arithmetic Frobenius sends the chosen primitive root to its q = p^r power. Both sides are simple cyclotomic roots and their residues agree by construction of Frobenius, so Hensel uniqueness identifies them upstairs.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramifiedArithmeticFrobenius_generates
Documentationthe unramified cyclotomic theorem(ii): arithmetic Frobenius generates the whole Galois group, with exponents bounded by the degree f = ord_n(p^r).
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_valuationSubring_adjoin_eq_top
Documentationthe unramified cyclotomic theorem(iii), valuation-ring generation by the specified root.
The residue of ζ is again primitive of order n; its residue-field degree equals the full residue degree by part (i). Thus it generates the residue extension. Since the extension is unramified, the source maximal ideal maps onto the target maximal ideal, and Nakayama applied to the finite integral closure proves O_L = O_K[ζ].
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_of_finiteDimensional
DocumentationFinite-dimensional core of the complete the unramified cyclotomic theorem endpoint. The public endpoint below derives finite-dimensionality from L = K(ζ).
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicUnramified
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [FiniteDimensional K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_finiteDimensional_of_primitiveRoot_adjoin_eq_top
DocumentationA field generated by one integral element is finite-dimensional. This removes the redundant finite-dimensionality assumption from the literal the unramified cyclotomic theorem endpoint.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicEndpoint
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified
DocumentationComplete arithmetic-Frobenius endpoint for the unramified cyclotomic extension.
For the extension generated by a primitive prime-to-p root of unity, this packages: finite unramifiedness and the least-exponent degree formula; the canonical Galois/residue-Galois comparison and its arithmetic Frobenius generator; and O_L = O_K[ζ] for the specified ζ. No separate finite-dimensionality hypothesis is needed: it follows from L = K(ζ).
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section LocalCyclotomicEndpoint
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
AlgebraicNumberTheory.Valuations.padicCyclotomicUnramified_adjoin_le_integralClosure
DocumentationThe easy inclusion in the unramified cyclotomic theorem(iii): every root of unity is integral, hence the algebra generated by a primitive root lies in the integral closure. The reverse inclusion for the local cyclotomic setting is proved by padicCyclotomicUnramified_valuationSubring_adjoin_eq_top above.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
namespace AlgebraicNumberTheory
namespace Valuations
open Polynomial ZMod
section IntegralInclusion
variable {R : Type u} {L : Type v}
variable [CommRing R] [Field L] [Algebra R L]