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 needed for that construction. For a normal intermediate field, restriction maps the decomposition group upstairs onto the decomposition group of the restricted valuation. The proof uses the actual valuation-conjugacy correction in absoluteValueDecompositionGroup_map_restrictNormalHom.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocityinstance (p : Nat.Primes) : Fact p.1.PrimeSurrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩)Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩)Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩)Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m)Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional minstance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m)Restriction along a normal intermediate field, as a homomorphism between the decomposition groups of a valuation and its restriction.
Unlike an unrestricted Galois restriction, the codomain records the valuation-stabilizer condition, which is the condition needed to transport local Artin symbols through a global field tower.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def absoluteValueDecompositionGroupRestrictionHom
(wΩ : AbsoluteValue Ω ℝ) :
absoluteValueDecompositionGroup K wΩ →*
absoluteValueDecompositionGroup K
(wΩ.comp (f := algebraMap L Ω)
(algebraMap L Ω).injective) where
toFun τ :=
⟨AlgEquiv.restrictNormalHom
(F := K) (K₁ := Ω) L τ.1,
by
intro x
change
wΩ
(algebraMap L Ω
((AlgEquiv.restrictNormalHom
(F := K) (K₁ := Ω) L τ.1) x)) < 1 ↔
wΩ (algebraMap L Ω x) < 1
change
wΩ
(algebraMap L Ω
((AlgEquiv.restrictNormal τ.1 L) x)) < 1 ↔
wΩ (algebraMap L Ω x) < 1
rw [AlgEquiv.restrictNormal_commutes]
exact τ.2 (algebraMap L Ω x)⟩
map_one' := by
apply Subtype.ext
exact
map_one
(AlgEquiv.restrictNormalHom
(F := K) (K₁ := Ω) L)
map_mul' τ η := by
apply Subtype.ext
exact
map_mul
(AlgEquiv.restrictNormalHom
(F := K) (K₁ := Ω) L) τ.1 η.1Restriction from a Galois overfield is surjective on the actual decomposition groups of a nontrivial valuation.
The preimage is obtained by first extending the requested automorphism and then correcting it by an automorphism fixing the normal intermediate field. Thus the resulting lift genuinely stabilizes the specified valuation upstairs.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem absoluteValueDecompositionGroupRestrictionHom_surjective
[IsGalois K Ω]
(vK : AbsoluteValue K ℝ)
(hvK : vK.IsNontrivial)
(wΩ : AbsoluteValueExtension vK Ω) :
Function.Surjective
(absoluteValueDecompositionGroupRestrictionHom
(K := K) (L := L) (Ω := Ω) wΩ.1)The infinite global Artin symbol of a finite one-place idèle stabilizes every chosen extension of that finite place to an abelian Galois overfield.
The proof is genuinely inverse-limit in nature. For each element of the overfield, we pass to the finite Galois closure it generates. The restriction of the infinite Artin symbol is then the finite chosen local Artin symbol, whose image is the finite decomposition group. Independence of the exact extension in the abelian finite layer returns the valuation stabilizer statement upstairs.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
infiniteGlobalArtinMonoidHom_finitePlaceIdele_mem_absoluteValueDecompositionGroup
{F A : Type}
[Field F] [NumberField F]
[Field A] [Algebra F A] [IsAbelianGalois F A]
(v : HeightOneSpectrum (𝓞 F))
(wA : AbsoluteValueExtension
(NumberField.HeightOneSpectrum.adicAbv F v) A)
(x : (v.adicCompletion F)ˣ) :
infiniteGlobalArtinMonoidHom F A
(IdeleGroup.finitePlaceIdele v x) ∈
absoluteValueDecompositionGroup F wA.1Restriction from a finite cyclotomic compositum over a number field to its rational cyclotomic layer.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]
section FiniteCyclotomicBaseChange
variable
{F : Type*} [Field F] [NumberField F]def
numberFieldCyclotomicZHatFiniteCompositumRestriction
(E :
FiniteGaloisIntermediateField
ℚ rationalCyclotomicZHatField) :
Gal(numberFieldCyclotomicZHatFiniteCompositum F E / F) →*
Gal(E / ℚ)Restriction to the rational factor is injective on the actual finite compositum: an automorphism fixing both generating fields fixes their supremum.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]
section FiniteCyclotomicBaseChange
variable
{F : Type*} [Field F] [NumberField F]theorem
numberFieldCyclotomicZHatFiniteCompositumRestriction_injective
(E :
FiniteGaloisIntermediateField
ℚ rationalCyclotomicZHatField) :
Function.Injective
(numberFieldCyclotomicZHatFiniteCompositumRestriction
(F := F) E)The Galois group of the finite compositum is canonically the subgroup of the rational finite-layer Galois group fixing the actual intersection with the number field.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]
section FiniteCyclotomicBaseChange
variable
{F : Type*} [Field F] [NumberField F]def
numberFieldCyclotomicZHatFiniteCompositumGalEquivFixingSubgroup
(E :
FiniteGaloisIntermediateField
ℚ rationalCyclotomicZHatField) :
Gal(numberFieldCyclotomicZHatFiniteCompositum F E / F) ≃*
(numberFieldCyclotomicZHatFiniteIntersection F E).fixingSubgroupThe finite compositum Galois group and the intersection-fixing subgroup have the same cardinality.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]
section FiniteCyclotomicBaseChange
variable
{F : Type*} [Field F] [NumberField F]theorem
numberFieldCyclotomicZHatFiniteCompositum_galois_card
(E :
FiniteGaloisIntermediateField
ℚ rationalCyclotomicZHatField) :
Nat.card
(Gal(numberFieldCyclotomicZHatFiniteCompositum F E / F)) =
Nat.card
(numberFieldCyclotomicZHatFiniteIntersection F E).fixingSubgroupRestriction from the full actual cyclotomic ZHat-compositum over a number field has image exactly the subgroup fixing the genuine intersection with the rational cyclotomic ZHat-field.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem numberFieldCyclotomicZHatCompositumRestriction_range
(F : Type*) [Field F] [NumberField F] :
(numberFieldCyclotomicZHatCompositumRestriction F).range =
((numberFieldCyclotomicZHatIntersection F).restrict
(show
numberFieldCyclotomicZHatIntersection F ≤
rationalCyclotomicZHatField from
by
dsimp only [numberFieldCyclotomicZHatIntersection]
exact inf_le_right)).fixingSubgroup := by
let C := numberFieldCyclotomicZHatCompositum F
let : Algebra ℚ C := C.algebra'
let : Algebra F C :=
numberFieldCyclotomicZHatCompositum_algebra F
let : IsScalarTower ℚ F C :=
numberFieldCyclotomicZHatCompositum_scalarTower F
let : Algebra rationalCyclotomicZHatField C :=
rationalCyclotomicZHatCompositum_algebra F
let : IsScalarTower ℚ rationalCyclotomicZHatField C :=
rationalCyclotomicZHatCompositum_scalarTower F
let : Normal ℚ rationalCyclotomicZHatField :=
rationalCyclotomicZHatField_normal
let eF : F →ₐ[ℚ] C :=
numberFieldCyclotomicZHatCompositumEmbedding F
let eT : rationalCyclotomicZHatField →ₐ[ℚ] C :=
rationalCyclotomicZHatCompositumEmbedding F
let r := numberFieldCyclotomicZHatCompositumRestriction F
have hIntersection_le :
numberFieldCyclotomicZHatIntersection F ≤
rationalCyclotomicZHatField := by
change
numberFieldInRationalSeparableClosure F ⊓
rationalCyclotomicZHatField ≤
rationalCyclotomicZHatField
exact inf_le_right
let J : IntermediateField ℚ rationalCyclotomicZHatField :=
(numberFieldCyclotomicZHatIntersection F).restrict
hIntersection_le
have eF_eq_algebraMap (y : F) :
eF y = algebraMap F C y := by
rfl
have restriction_commutes
(τ : C ≃ₐ[F] C) (z : rationalCyclotomicZHatField) :
eT (r τ z) = τ (eT z) := by
change
algebraMap rationalCyclotomicZHatField C (r τ z) =
τ (algebraMap rationalCyclotomicZHatField C z)
change
algebraMap rationalCyclotomicZHatField C
((AlgEquiv.restrictNormal
(MulSemiringAction.toAlgEquiv ℚ C τ)
rationalCyclotomicZHatField) z) =
(MulSemiringAction.toAlgEquiv ℚ C τ)
(algebraMap rationalCyclotomicZHatField C z)
exact
AlgEquiv.restrictNormal_commutes
(MulSemiringAction.toAlgEquiv ℚ C τ)
rationalCyclotomicZHatField z
have hJ (x : rationalCyclotomicZHatField) :
x ∈ J ↔ eT x ∈ eF.fieldRange := by
change
x ∈ (numberFieldCyclotomicZHatIntersection F).restrict
hIntersection_le ↔
eT x ∈ eF.fieldRange
rw [IntermediateField.mem_restrict]
change
x.1 ∈
numberFieldInRationalSeparableClosure F ⊓
rationalCyclotomicZHatField ↔
eT x ∈ eF.fieldRange
rw [IntermediateField.mem_inf]
simp only [x.2, and_true]
change
x.1 ∈ (numberFieldSeparableClosureEmbedding F).fieldRange ↔
eT x ∈ eF.fieldRange
rw [AlgHom.mem_fieldRange, AlgHom.mem_fieldRange]
constructor
· rintro ⟨y, hy⟩
refine ⟨y, ?_⟩
apply Subtype.ext
change numberFieldSeparableClosureEmbedding F y = x.1
exact hy
· rintro ⟨y, hy⟩
refine ⟨y, ?_⟩
change numberFieldSeparableClosureEmbedding F y = x.1
exact congrArg Subtype.val hy
have hfixedField :
IntermediateField.fixedField r.range = J := by
ext x
rw [IntermediateField.mem_fixedField_iff]
rw [hJ]
constructor
· intro hx
have hfixed :
∀ τ : C ≃ₐ[F] C, τ (eT x) = eT x := by
intro τ
have hxτ : r τ x = x :=
hx (r τ) ⟨τ, rfl⟩
have hrestrict :
eT (r τ x) = τ (eT x) := by
exact restriction_commutes τ x
exact hrestrict.symm.trans (congrArg eT hxτ)
have hmem :
eT x ∈ Set.range (algebraMap F C) :=
(InfiniteGalois.mem_range_algebraMap_iff_fixed
(eT x)).2 hfixed
rw [AlgHom.mem_fieldRange]
obtain ⟨y, hy⟩ := hmem
exact ⟨y, (eF_eq_algebraMap y).trans hy⟩
· intro hx σ hσ
obtain ⟨τ, rfl⟩ := hσ
rw [AlgHom.mem_fieldRange] at hx
obtain ⟨y, hy⟩ := hx
apply eT.injective
have hrestrict :
eT (r τ x) = τ (eT x) := by
exact restriction_commutes τ x
calc
eT (r τ x) = τ (eT x) := hrestrict
_ = τ (eF y) := congrArg τ hy.symm
_ = eF y := by
rw [eF_eq_algebraMap]
exact τ.commutes y
_ = eT x := hy
let H : ClosedSubgroup
(rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField) :=
{ toSubgroup := r.range
isClosed' := by
change IsClosed (Set.range r)
have hrClosed :
IsClosed
(Set.range
(numberFieldCyclotomicZHatCompositumRestriction F)) :=
(isCompact_range
(numberFieldCyclotomicZHatCompositumRestriction_continuous F)).isClosed
simpa only [r] using hrClosed }
change r.range = J.fixingSubgroup
calc
r.range =
(IntermediateField.fixedField r.range).fixingSubgroup :=
(by
have hH := InfiniteGalois.fixingSubgroup_fixedField H
change
(IntermediateField.fixedField r.range).fixingSubgroup =
r.range at hH
exact hH.symm)
_ = J.fixingSubgroup :=
congrArg
(fun E : IntermediateField ℚ rationalCyclotomicZHatField =>
E.fixingSubgroup)
hfixedFieldThe genuine cyclotomic ZHat coordinate on the full compositum over a number field.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def numberFieldCyclotomicZHatCompositumCoordinate
(F : Type*) [Field F] [NumberField F] :
Gal(numberFieldCyclotomicZHatCompositum F / F) →*
Multiplicative ZHatThe genuine cyclotomic coordinate on the full compositum is injective.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem numberFieldCyclotomicZHatCompositumCoordinate_injective
(F : Type*) [Field F] [NumberField F] :
Function.Injective
(numberFieldCyclotomicZHatCompositumCoordinate F)The actual cyclotomic ZHat-compositum over every number field has torsion-free Galois group.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]instance
numberFieldCyclotomicZHatCompositumGal_isMulTorsionFree
(F : Type*) [Field F] [NumberField F] :
IsMulTorsionFree
(Gal(numberFieldCyclotomicZHatCompositum F / F))The image of the actual cyclotomic compositum over F is precisely f_F ZHat, where f_F is the degree of the genuine intersection F ∩ ℚ̃.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
numberFieldCyclotomicZHatCompositumCoordinate_range_toAddSubgroup
(F : Type*) [Field F] [NumberField F] :
(numberFieldCyclotomicZHatCompositumCoordinate F).range.toAddSubgroup' =
(zHatMulNat
(cyclotomicZHatIntersectionDegree F)).toAddMonoidHom.rangeA surjective restriction map admits positive cyclotomic-degree lifts as soon as the degrees contributed by its kernel have finite index in ZHat.
This is the group-theoretic core of the decomposition-compatible Frobenius lift: the initial preimage is corrected inside the genuine restriction kernel, so its prescribed image is unchanged.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem exists_positiveZHatDegree_lift_of_surjective
{D A : Type*} [Group D] [Group A]
(restriction : D →* A)
(hrestriction : Function.Surjective restriction)
(degree : D →* Multiplicative ZHat)
(hdegree :
((restriction.ker.map degree).toAddSubgroup').index ≠ 0)
(σ : A) :
∃ τ : D,
restriction τ = σ ∧
∃ n : ℕ, 0 < n ∧
degree τ =
(Multiplicative.ofAdd (1 : ZHat)) ^ nTwo homomorphisms out of a finite commutative group agree once they agree on every primary component.
This is the precise prime-power reduction used in the finite-place argument. It is proved from the actual direct-product decomposition by the Sylow subgroups; no cyclicity hypothesis on the whole group is introduced.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem MonoidHom.ext_of_eq_on_finitePrimaryComponents
{G A : Type*}
[CommGroup G] [Finite G]
[CommGroup A]
(f g : G →* A)
(hprimary :
∀ (p : ℕ) (_hp : Fact p.Prime)
(x : CommGroup.primaryComponent G p),
f x = g x) :
f = gEvery individual p-adic coordinate of the profinite integers is surjective. This is extracted from the genuine Chinese-remainder equivalence ZHat ≃ ∏ p, ℤ_p.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem zHatToPadicInt_surjective
(p : Nat.Primes) :
Function.Surjective (zHatToPadicInt p)The genuine p-adic cyclotomic coordinate on the actual Galois group of the rational cyclotomic ZHat-extension.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def rationalCyclotomicPadicCoordinate
(p : Nat.Primes) :
(rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField) →ₜ*
Multiplicative ℤ_[p.1]The rational cyclotomic p-adic coordinate is obtained by applying the canonical ZHat-to-ℤ_p coordinate to the cyclotomic character.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem rationalCyclotomicPadicCoordinate_apply
(p : Nat.Primes)
(σ :
rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField) :
Multiplicative.toAdd
(rationalCyclotomicPadicCoordinate p σ) =
zHatToPadicInt p
(Multiplicative.toAdd
(rationalCyclotomicZHatFieldGalEquivZHat σ))The p-adic cyclotomic coordinate on the actual decomposition group of an arbitrary absolute value of the number-field cyclotomic ZHat-compositum.
This is the restriction of the genuine compositum Galois group to the rational cyclotomic factor, followed by its actual ℤ_p coordinate. The source is the valuation stabilizer itself, rather than an abstract copy of a local Galois group.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def
numberFieldCyclotomicPadicDecompositionCoordinate
(F : Type) [Field F] [NumberField F]
(wC : AbsoluteValue
(numberFieldCyclotomicZHatCompositum F) ℝ)
(p : Nat.Primes) :
absoluteValueDecompositionGroup F wC →ₜ*
Multiplicative ℤ_[p.1] where
toMonoidHom :=
(rationalCyclotomicPadicCoordinate p).toMonoidHom.comp
((numberFieldCyclotomicZHatCompositumRestriction F).comp
(absoluteValueDecompositionGroup F wC).subtype)
continuous_toFun :=
(rationalCyclotomicPadicCoordinate p).continuous_toFun.comp
((numberFieldCyclotomicZHatCompositumRestriction_continuous
(K := F)).comp continuous_subtype_val)The decomposition-group coordinate is the rational cyclotomic coordinate of the restricted global automorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem numberFieldCyclotomicPadicDecompositionCoordinate_apply
(F : Type) [Field F] [NumberField F]
(wC : AbsoluteValue
(numberFieldCyclotomicZHatCompositum F) ℝ)
(p : Nat.Primes)
(σ : absoluteValueDecompositionGroup F wC) :
numberFieldCyclotomicPadicDecompositionCoordinate
F wC p σ =
rationalCyclotomicPadicCoordinate p
(numberFieldCyclotomicZHatCompositumRestriction F σ.1)On an actual global Artin symbol lying in a decomposition group, the decomposition coordinate is the p-adic coordinate of the rational cyclotomic idèle value of the ordinary field norm.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
numberFieldCyclotomicPadicDecompositionCoordinate_infiniteGlobalArtin
(F : Type) [Field F] [NumberField F]
(wC : AbsoluteValue
(numberFieldCyclotomicZHatCompositum F) ℝ)
(p : Nat.Primes) (a : IdeleGroup F)
(ha :
infiniteGlobalArtinMonoidHom F
(numberFieldCyclotomicZHatCompositum F) a ∈
absoluteValueDecompositionGroup F wC) :
numberFieldCyclotomicPadicDecompositionCoordinate
F wC p
⟨infiniteGlobalArtinMonoidHom F
(numberFieldCyclotomicZHatCompositum F) a, ha⟩ =
Multiplicative.ofAdd
(zHatToPadicInt p
(Multiplicative.toAdd
(rationalCyclotomicZHatIdeleValue
(IdeleGroup.norm ℚ F a))))The image of a cyclotomic p-adic decomposition coordinate is closed. This is the compact image of the actual closed decomposition group in the Krull topology.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
numberFieldCyclotomicPadicDecompositionCoordinate_range_isClosed
(F : Type) [Field F] [NumberField F]
(wC : AbsoluteValue
(numberFieldCyclotomicZHatCompositum F) ℝ)
(p : Nat.Primes) :
IsClosed
((numberFieldCyclotomicPadicDecompositionCoordinate
F wC p).range :
Set (Multiplicative ℤ_[p.1]))Reduction of the full cyclotomic character of a rational one-place idèle whose component is a power of a principal local component. The result is the same power of the genuine chosen local Artin character.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
rationalCyclotomicCharacterPrimeProduct_finitePlaceIdele_principalComponent_toZModPow
(p q : Nat.Primes) (k d : ℕ) (x : ℚˣ) :
Units.map (PadicInt.toZModPow k).toMonoidHom
(KummerTheory.rationalCyclotomicCharacterPrimeProduct
(infiniteGlobalArtinMonoidHom
ℚ KummerTheory.rationalCyclotomicField
(IdeleGroup.finitePlaceIdele
(RayClass.rationalPrime q)
((IdeleGroup.finiteComponent
(RayClass.rationalPrime q)
(IdeleGroup.principalIdele ℚ x)) ^ d))) p) =
(rationalCyclotomicPrincipalFinitePlaceCharacter
p k x q) ^ dAt the place p, the full p-adic cyclotomic character of the one-place idèle obtained from the rational unit p + 1 is the direct unit p + 1, with the prescribed local-degree power.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
rationalCyclotomicCharacterPrimeProduct_finitePlaceIdele_primeSucc
(p : Nat.Primes) (d : ℕ) :
KummerTheory.rationalCyclotomicCharacterPrimeProduct
(infiniteGlobalArtinMonoidHom
ℚ KummerTheory.rationalCyclotomicField
(IdeleGroup.finitePlaceIdele
(RayClass.rationalPrime p)
((IdeleGroup.finiteComponent
(RayClass.rationalPrime p)
(IdeleGroup.principalIdele ℚ
(Units.mk0
((p.1 + 1 : ℕ) : ℚ)
(by positivity)))) ^ d))) p =
(padicNatUnit p (p.1 + 1)
(Nat.coprime_self_add_right.mpr
(Nat.coprime_one_right p.1))) ^ d := by
let x : ℚˣ :=
Units.mk0
((p.1 + 1 : ℕ) : ℚ)
(by positivity)
have hx :
(x : ℚ) =
((p.1 + 1 : ℕ) : ℚ) :=
rfl
have hprimeUnit :
(rationalPrimeUnit x p : ℚ) =
((p.1 + 1 : ℕ) : ℚ) := by
rw [rationalPrimeUnit_val,
hx,
padicValRat_rationalPrime_succ,
neg_zero,
zpow_zero,
one_mul]
have hunit :
padicIntUnitOfRat p
(rationalPrimeUnit x p : ℚ)
(rationalPrimeUnit x p).ne_zero
(padicValRat_rationalPrimeUnit x p) =
padicNatUnit p (p.1 + 1)
(Nat.coprime_self_add_right.mpr
(Nat.coprime_one_right p.1)) := by
apply Units.ext
apply Subtype.ext
rw [padicIntUnitOfRat_coe,
padicNatUnit_val,
hprimeUnit]
exact PadicInt.coe_natCast (p.1 + 1)
apply Units.ext
apply PadicInt.ext_of_toZModPow.mp
intro k
let hpFact : Fact (Nat.Prime p.1) := ⟨p.2⟩
have hred :=
rationalCyclotomicCharacterPrimeProduct_finitePlaceIdele_principalComponent_toZModPow
p p k d x
rw [
rationalCyclotomicPrincipalFinitePlaceCharacter_at_prime p k x,
hunit] at hred
have hredVal := congrArg Units.val hred
simp only [Units.coe_map, Units.val_pow_eq_pow_val] at hredVal
have htoZModPow (z : ℤ_[p.1]) :
(PadicInt.toZModPow
(p := p.1) (k : ℕ)).toMonoidHom z =
PadicInt.toZModPow (p := p.1) (k : ℕ) z :=
rfl
simp only [htoZModPow] at hredVal
simpa only [x, Units.val_pow_eq_pow_val, map_pow] using hredValAway from p, the full p-adic cyclotomic character of the rational-prime one-place idèle is inverse arithmetic Frobenius, again with the prescribed local-degree power.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
rationalCyclotomicCharacterPrimeProduct_finitePlaceIdele_primeAway
(p q : Nat.Primes) (hqp : q ≠ p) (d : ℕ) :
KummerTheory.rationalCyclotomicCharacterPrimeProduct
(infiniteGlobalArtinMonoidHom
ℚ KummerTheory.rationalCyclotomicField
(IdeleGroup.finitePlaceIdele
(RayClass.rationalPrime q)
((IdeleGroup.finiteComponent
(RayClass.rationalPrime q)
(IdeleGroup.principalIdele ℚ
(Units.mk0 (q.1 : ℚ)
(by exact_mod_cast q.2.ne_zero)))) ^ d))) p =
((padicNatUnit p q.1
((Nat.coprime_primes p.2 q.2).2
(fun hpq =>
hqp (Subtype.ext hpq.symm))))⁻¹) ^ d := by
let x : ℚˣ :=
Units.mk0 (q.1 : ℚ)
(by exact_mod_cast q.2.ne_zero)
let hcoprime : p.1.Coprime q.1 :=
(Nat.coprime_primes p.2 q.2).2
(fun hpq =>
hqp (Subtype.ext hpq.symm))
have hx : (x : ℚ) = q.1 := rfl
apply Units.ext
apply PadicInt.ext_of_toZModPow.mp
intro k
let hpFact : Fact (Nat.Prime p.1) := ⟨p.2⟩
have hlocal :
rationalCyclotomicPrincipalFinitePlaceCharacter
p k x q =
(ZMod.unitOfCoprime q.1
(q.2.coprime_iff_not_dvd.mpr
(rationalPrime_not_dvd_pow_of_ne
q p hqp k)))⁻¹ := by
rw [
rationalCyclotomicPrincipalFinitePlaceCharacter_of_ne
p q hqp k x,
hx,
padicValRat.self q.2.one_lt,
zpow_neg,
zpow_one]
have hred :=
rationalCyclotomicCharacterPrimeProduct_finitePlaceIdele_principalComponent_toZModPow
p q k d x
rw [hlocal] at hred
have htarget :
Units.map
(PadicInt.toZModPow
(p := p.1) (k : ℕ)).toMonoidHom
(((padicNatUnit p q.1 hcoprime)⁻¹) ^ d) =
((ZMod.unitOfCoprime q.1
(hcoprime.symm.pow_right k))⁻¹) ^ d := by
rw [map_pow, map_inv,
padicNatUnit_toZModPow]
have hredVal :=
congrArg Units.val (hred.trans htarget.symm)
simp only [Units.coe_map, Units.val_pow_eq_pow_val] at hredVal
have htoZModPow (z : ℤ_[p.1]) :
(PadicInt.toZModPow
(p := p.1) (k : ℕ)).toMonoidHom z =
PadicInt.toZModPow (p := p.1) (k : ℕ) z :=
rfl
simp only [htoZModPow] at hredVal
simpa only [x, hcoprime, Units.val_pow_eq_pow_val,
Units.val_inv_eq_inv_val] using hredValThe image of the actual decomposition group has a nonzero p-adic cyclotomic coordinate.
The witness is a genuine one-place idèle over F. Its component is obtained by extending a rational completion unit to the chosen place: at residue characteristic p we use p + 1, and away from p we use the rational residue prime. The ordinary idèle norm is the corresponding positive local-degree power. The direct-unit and inverse-Frobenius local formulas show that its full p-adic cyclotomic character is non-torsion, so its torsion-free coordinate cannot vanish.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
numberFieldCyclotomicPadicDecompositionCoordinate_range_toAddSubgroup_ne_bot
(F : Type) [Field F] [NumberField F]
(v : HeightOneSpectrum (𝓞 F))
(wC : AbsoluteValueExtension
(NumberField.HeightOneSpectrum.adicAbv F v)
(numberFieldCyclotomicZHatCompositum F))
(p : Nat.Primes) :
(numberFieldCyclotomicPadicDecompositionCoordinate
F wC.1 p).range.toAddSubgroup' ≠
(⊥ : AddSubgroup ℤ_[p.1])The actual p-adic coordinate of a finite-place decomposition group has finite index in ℤ_[p]. This is the precise nonvanishing input used to correct a Frobenius lift inside the restriction kernel.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
numberFieldCyclotomicPadicDecompositionCoordinate_range_index_ne_zero
(F : Type) [Field F] [NumberField F]
(v : HeightOneSpectrum (𝓞 F))
(wC : AbsoluteValueExtension
(NumberField.HeightOneSpectrum.adicAbv F v)
(numberFieldCyclotomicZHatCompositum F))
(p : Nat.Primes) :
((numberFieldCyclotomicPadicDecompositionCoordinate
F wC.1 p).range.toAddSubgroup').index ≠ 0The finite-index conclusion depends only on the valuation class of the chosen absolute value on the cyclotomic compositum.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
numberFieldCyclotomicPadicDecompositionCoordinate_range_index_ne_zero_of_isEquiv
(F : Type) [Field F] [NumberField F]
(v : HeightOneSpectrum (𝓞 F))
(wC : AbsoluteValue
(numberFieldCyclotomicZHatCompositum F) ℝ)
(wC' : AbsoluteValueExtension
(NumberField.HeightOneSpectrum.adicAbv F v)
(numberFieldCyclotomicZHatCompositum F))
(hww' : wC.IsEquiv wC'.1)
(p : Nat.Primes) :
((numberFieldCyclotomicPadicDecompositionCoordinate
F wC p).range.toAddSubgroup').index ≠ 0The finite-index conclusion for an arbitrary representative of the valuation class above v.
The hypothesis only compares the restriction of the chosen absolute value with the normalized v-adic absolute value. We raise the chosen nonarchimedean absolute value to the unique positive normalizing exponent, obtaining an exact extension without changing its decomposition group.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
numberFieldCyclotomicPadicDecompositionCoordinate_range_index_ne_zero_of_base_isEquiv
(F : Type) [Field F] [NumberField F]
(v : HeightOneSpectrum (𝓞 F))
(wC : AbsoluteValue
(numberFieldCyclotomicZHatCompositum F) ℝ)
(hbase :
(wC.comp
(f := algebraMap F
(numberFieldCyclotomicZHatCompositum F))
(algebraMap F
(numberFieldCyclotomicZHatCompositum F)).injective).IsEquiv
(NumberField.HeightOneSpectrum.adicAbv F v))
(p : Nat.Primes) :
((numberFieldCyclotomicPadicDecompositionCoordinate
F wC p).range.toAddSubgroup').index ≠ 0The actual cyclotomic p-adic coordinate is onto.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem rationalCyclotomicPadicCoordinate_surjective
(p : Nat.Primes) :
Function.Surjective
(rationalCyclotomicPadicCoordinate p)The closed subgroup fixing the p-primary cyclotomic direction.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def rationalCyclotomicPadicKernel
(p : Nat.Primes) :
ClosedSubgroup
(rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField) where
toSubgroup :=
(rationalCyclotomicPadicCoordinate p).toMonoidHom.ker
isClosed' := by
change
IsClosed
((rationalCyclotomicPadicCoordinate p) ⁻¹'
({1} : Set (Multiplicative ℤ_[p.1])))
exact
isClosed_singleton.preimage
(rationalCyclotomicPadicCoordinate p).continuous_toFunThe closed p-adic coordinate kernel is normal because it is the kernel of a group homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]instance rationalCyclotomicPadicKernel_normal
(p : Nat.Primes) :
(rationalCyclotomicPadicKernel p).toSubgroup.NormalThe p-primary cyclotomic field inside the rational cyclotomic ZHat-extension. Its defining subgroup is the kernel of the actual coordinate to ℤ_p.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]abbrev rationalCyclotomicPadicFieldWithinZHat
(p : Nat.Primes) :
IntermediateField ℚ rationalCyclotomicZHatFieldThe internal p-primary fixed field is Galois over ℚ.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]instance
rationalCyclotomicPadicFieldWithinZHat_isGalois
(p : Nat.Primes) :
IsGalois ℚ (rationalCyclotomicPadicFieldWithinZHat p)The canonical algebra maps through the internal p-primary fixed field form a scalar tower.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]instance rationalCyclotomicPadicFieldWithinZHat_scalarTower
(p : Nat.Primes) :
IsScalarTower ℚ (rationalCyclotomicPadicFieldWithinZHat p)
rationalCyclotomicZHatFieldThe actual p-primary cyclotomic field in the fixed rational separable closure.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def rationalCyclotomicPadicField
(p : Nat.Primes) :
IntermediateField ℚ (SeparableClosure ℚ)The actual p-primary field is contained in the cyclotomic ZHat-extension.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem rationalCyclotomicPadicField_le_cyclotomicZHatField
(p : Nat.Primes) :
rationalCyclotomicPadicField p ≤
rationalCyclotomicZHatFieldThe fixing subgroup of the internal p-primary field is exactly the kernel of the p-adic cyclotomic coordinate.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem rationalCyclotomicPadicFieldWithinZHat_fixingSubgroup
(p : Nat.Primes) :
(rationalCyclotomicPadicFieldWithinZHat p).fixingSubgroup =
(rationalCyclotomicPadicKernel p).toSubgroupThe Galois group of the internal p-primary cyclotomic field is the actual additive group of p-adic integers, written multiplicatively.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def
rationalCyclotomicPadicFieldWithinZHatGalEquivPadicInt
(p : Nat.Primes) :
(rationalCyclotomicPadicFieldWithinZHat p ≃ₐ[ℚ]
rationalCyclotomicPadicFieldWithinZHat p) ≃*
Multiplicative ℤ_[p.1]Under the ℤ_p coordinate, restriction to the internal p-primary field is exactly the original cyclotomic coordinate.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
rationalCyclotomicPadicFieldWithinZHatGalEquivPadicInt_restrict
(p : Nat.Primes)
(σ :
rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField) :
rationalCyclotomicPadicFieldWithinZHatGalEquivPadicInt p
(AlgEquiv.restrictNormalHom
(rationalCyclotomicPadicFieldWithinZHat p) σ) =
rationalCyclotomicPadicCoordinate p σThe actual p-primary cyclotomic field is an abelian Galois extension of ℚ.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]instance
rationalCyclotomicPadicField_isAbelianGalois
(p : Nat.Primes) :
IsAbelianGalois ℚ (rationalCyclotomicPadicField p)Reduction from p-adic integers to a finite p-power quotient is surjective.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem padicIntToZModPow_surjective
(p : Nat.Primes) (n : ℕ) :
Function.Surjective
(PadicInt.toZModPow
(p := p.1) n)The finite p^n cyclotomic coordinate on the genuine cyclotomic ZHat Galois group.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def rationalCyclotomicPadicReduction
(p : Nat.Primes) (n : ℕ) :
(rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField) →*
Multiplicative (ZMod (p.1 ^ n))Finite cyclotomic reduction is obtained by reducing the p-adic cyclotomic coordinate modulo p^n.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem rationalCyclotomicPadicReduction_apply
(p : Nat.Primes) (n : ℕ)
(σ :
rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField) :
Multiplicative.toAdd
(rationalCyclotomicPadicReduction p n σ) =
PadicInt.toZModPow n
(Multiplicative.toAdd
(rationalCyclotomicPadicCoordinate p σ))Every finite p^n cyclotomic coordinate is onto.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem rationalCyclotomicPadicReduction_surjective
(p : Nat.Primes) (n : ℕ) :
Function.Surjective
(rationalCyclotomicPadicReduction p n)The closed subgroup cutting out the finite p^n cyclotomic layer.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def rationalCyclotomicPadicLevelKernel
(p : Nat.Primes) (n : ℕ) :
ClosedSubgroup
(rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField) where
toSubgroup :=
(rationalCyclotomicPadicReduction p n).ker
isClosed' := by
let c :=
fun σ :
rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField =>
Multiplicative.toAdd
(rationalCyclotomicPadicCoordinate p σ)
have hc : Continuous c :=
continuous_toAdd.comp
(rationalCyclotomicPadicCoordinate p).continuous_toFun
have hspan :
IsClosed
((Ideal.span
({(p.1 : ℤ_[p.1]) ^ n} :
Set ℤ_[p.1]) :
Ideal ℤ_[p.1]) :
Set ℤ_[p.1]) := by
have hset :
((Ideal.span
({(p.1 : ℤ_[p.1]) ^ n} :
Set ℤ_[p.1]) :
Ideal ℤ_[p.1]) :
Set ℤ_[p.1]) =
Metric.closedBall 0
((p.1 : ℝ) ^ (-n : ℤ)) := by
ext x
change
x ∈
(Ideal.span
({(p.1 : ℤ_[p.1]) ^ n} : Set ℤ_[p.1]) :
Ideal ℤ_[p.1]) ↔
dist x 0 ≤ (p.1 : ℝ) ^ (-n : ℤ)
rw [dist_zero_right,
PadicInt.norm_le_pow_iff_mem_span_pow]
rw [hset]
exact Metric.isClosed_closedBall
change
IsClosed
{σ |
rationalCyclotomicPadicReduction p n σ = 1}
rw [show
{σ |
rationalCyclotomicPadicReduction p n σ = 1} =
c ⁻¹'
((Ideal.span
({(p.1 : ℤ_[p.1]) ^ n} :
Set ℤ_[p.1]) :
Ideal ℤ_[p.1]) :
Set ℤ_[p.1]) by
ext σ
change
PadicInt.toZModPow n (c σ) = 0 ↔
c σ ∈
(Ideal.span
({(p.1 : ℤ_[p.1]) ^ n} :
Set ℤ_[p.1]) :
Ideal ℤ_[p.1])
rw [← PadicInt.ker_toZModPow n,
RingHom.mem_ker]]
exact hspan.preimage hcThe finite-coordinate kernel is normal because it is the kernel of a group homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]instance rationalCyclotomicPadicLevelKernel_normal
(p : Nat.Primes) (n : ℕ) :
(rationalCyclotomicPadicLevelKernel p n).toSubgroup.NormalThe finite-coordinate kernel is open in the cyclotomic Galois group.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem rationalCyclotomicPadicLevelKernel_isOpen
(p : Nat.Primes) (n : ℕ) :
IsOpen
((rationalCyclotomicPadicLevelKernel p n :
Subgroup
(rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField)) :
Set
(rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField))The genuine finite cyclotomic p^n layer inside the actual cyclotomic ZHat-extension.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]abbrev rationalCyclotomicPadicFiniteLevel
(p : Nat.Primes) (n : ℕ) :
FiniteGaloisIntermediateField
ℚ rationalCyclotomicZHatField where
toIntermediateField :=
IntermediateField.fixedField
(rationalCyclotomicPadicLevelKernel p n).toSubgroup
finiteDimensional := by
apply
(InfiniteGalois.isOpen_iff_finite
(IntermediateField.fixedField
(rationalCyclotomicPadicLevelKernel p n).toSubgroup)).mp
rw [
InfiniteGalois.fixingSubgroup_fixedField
(rationalCyclotomicPadicLevelKernel p n)]
exact
rationalCyclotomicPadicLevelKernel_isOpen p n
isGalois := by infer_instanceThe bundled finite p^n layer exposes its constructed Galois instance across the opaque field definition.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]instance rationalCyclotomicPadicFiniteLevel_isGalois
(p : Nat.Primes) (n : ℕ) :
IsGalois ℚ (rationalCyclotomicPadicFiniteLevel p n)The canonical algebra maps through the finite p^n layer form a scalar tower.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]instance rationalCyclotomicPadicFiniteLevel_scalarTower
(p : Nat.Primes) (n : ℕ) :
IsScalarTower ℚ (rationalCyclotomicPadicFiniteLevel p n)
rationalCyclotomicZHatFieldThe Galois group of the finite p^n cyclotomic level is the actual cyclic group ZMod (p^n).
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def
rationalCyclotomicPadicFiniteLevelGalEquivZMod
(p : Nat.Primes) (n : ℕ) :
(rationalCyclotomicPadicFiniteLevel p n ≃ₐ[ℚ]
rationalCyclotomicPadicFiniteLevel p n) ≃*
Multiplicative (ZMod (p.1 ^ n))Restriction to a finite p^n level is exactly reduction of the genuine p-adic cyclotomic coordinate modulo p^n.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
rationalCyclotomicPadicFiniteLevelGalEquivZMod_restrict
(p : Nat.Primes) (n : ℕ)
(σ :
rationalCyclotomicZHatField ≃ₐ[ℚ]
rationalCyclotomicZHatField) :
rationalCyclotomicPadicFiniteLevelGalEquivZMod p n
(AlgEquiv.restrictNormalHom
(rationalCyclotomicPadicFiniteLevel p n) σ) =
rationalCyclotomicPadicReduction p n σThe Galois group of the base-changed finite p-primary cyclotomic layer, embedded in its genuine ZMod (p^n) coordinate.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]def
numberFieldCyclotomicPadicFiniteCompositumCoordinate
(F : Type*) [Field F] [NumberField F]
(p : Nat.Primes) (n : ℕ) :
Gal(numberFieldCyclotomicZHatFiniteCompositum F
(rationalCyclotomicPadicFiniteLevel p n) / F) →*
Multiplicative (ZMod (p.1 ^ n))The finite base-changed cyclotomic coordinate is injective. Thus the actual compositum Galois group is realized as a subgroup of the cyclic p-power coordinate, with no abstract replacement field.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
numberFieldCyclotomicPadicFiniteCompositumCoordinate_injective
(F : Type*) [Field F] [NumberField F]
(p : Nat.Primes) (n : ℕ) :
Function.Injective
(numberFieldCyclotomicPadicFiniteCompositumCoordinate
F p n)Every actual finite base-changed p-primary cyclotomic layer has cyclic Galois group. The statement is about the genuine compositum over F: cyclicity follows by embedding its Galois group into the standard cyclic ZMod (p^n) coordinate.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem
numberFieldCyclotomicPadicFiniteCompositum_isCyclic
(F : Type*) [Field F] [NumberField F]
(p : Nat.Primes) (n : ℕ) :
IsCyclic
(Gal(numberFieldCyclotomicZHatFiniteCompositum F
(rationalCyclotomicPadicFiniteLevel p n) / F))The degree of the genuine finite p^n cyclotomic level is exactly p^n.
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicNumberTheory.Valuations
open AlgebraicNumberTheory
open HilbertRamification
open ClassFormation
open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerNumberField
(p : Nat.Primes) (k : ℕ) :
NumberField (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
KummerTheory.rationalCyclotomicLevel_numberField
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerFiniteDimensional
(p : Nat.Primes) (k : ℕ) :
FiniteDimensional ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional
⟨p.1 ^ k, pow_pos p.2.pos k⟩
local instance rationalCyclotomicFrobeniusLiftPrimePowerIsAbelianGalois
(p : Nat.Primes) (k : ℕ) :
IsAbelianGalois ℚ (KummerTheory.rationalCyclotomicLevel
⟨p.1 ^ k, pow_pos p.2.pos k⟩) :=
rationalCyclotomicLevelIsAbelianGalois
⟨p.1 ^ k, pow_pos p.2.pos k⟩
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelFiniteDimensional
(m : ℕ+) :
FiniteDimensional ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicPrincipalPrimeLevelFiniteDimensional m
noncomputable local instance
rationalCyclotomicFrobeniusLiftLevelIsAbelianGalois
(m : ℕ+) :
IsAbelianGalois ℚ
(KummerTheory.rationalCyclotomicLevel m) :=
rationalCyclotomicLevelIsAbelianGalois m
variable
{K L Ω : Type}
[Field K] [Field L] [Field Ω]
[Algebra K L] [Algebra L Ω] [Algebra K Ω]
[IsScalarTower K L Ω] [Normal K L]theorem rationalCyclotomicPadicFiniteLevel_finrank
(p : Nat.Primes) (n : ℕ) :
Module.finrank ℚ
(rationalCyclotomicPadicFiniteLevel p n) =
p.1 ^ n