NYLL
Module

CyclicPrimePowerFullDecomposition.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Cohomology.CyclicPrimePowerFullDecomposition
8 declarations indexed from sourceView source ↗

Module documentation

Full decomposition places in cyclic prime-power extensions

This file proves the infinitude of full-decomposition places in cyclic prime-power extensions. For a cyclic group of prime-power order, every proper subgroup is contained in the chosen subgroup of index p. Consequently every finite place whose decomposition group is proper splits completely in the chosen degree-p subextension.

The second part records the idelic approximation argument: if all finite places outside a finite set split completely, then the idele class norm is surjective.

Imports4
Imported by3

Declarations

theorem

cyclicPrimeSubextensionDecompositionGroup_eq_bot_of_ne_top

L53 ↗
GlobalClassFieldTheory.Cohomology.cyclicPrimeSubextensionDecompositionGroup_eq_bot_of_ne_top
Documentation

A proper decomposition group in the original cyclic prime-power extension becomes trivial in the chosen degree-p subextension.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
namespace GlobalClassFieldTheory
namespace Cohomology
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField L] in
Lean source · statement
theorem
    cyclicPrimeSubextensionDecompositionGroup_eq_bot_of_ne_top
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard : Nat.card (L ≃ₐ[K] L) = p ^ exponent)
    (v : HeightOneSpectrum (𝓞 K))
    (hproper :
      finitePlaceDecompositionGroup
          (K := K) (L := L) v ≠ ⊤) :
    cyclicPrimeSubextensionDecompositionGroup
        (K := K) (L := L)
        hp hexponent hcard v = ⊥
theorem

finitePlaceSplitsCompletely_in_cyclicPrimeSubextension_of_decompositionGroup_ne_top

L100 ↗
GlobalClassFieldTheory.Cohomology.finitePlaceSplitsCompletely_in_cyclicPrimeSubextension_of_decompositionGroup_ne_top
Documentation

Every place with proper decomposition group in L / K splits completely, in the standard chosen-extension sense, in the actual degree-p fixed subextension.

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
namespace GlobalClassFieldTheory
namespace Cohomology
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
omit [NumberField L] in
Lean source · statement
theorem
    finitePlaceSplitsCompletely_in_cyclicPrimeSubextension_of_decompositionGroup_ne_top
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard : Nat.card (L ≃ₐ[K] L) = p ^ exponent)
    (v : HeightOneSpectrum (𝓞 K))
    (hproper :
      finitePlaceDecompositionGroup
          (K := K) (L := L) v ≠ ⊤) :
    FinitePlaceSplitsCompletely
      (K := K)
      (L := cyclicPrimeSubextension
        (K := K) (L := L)
        hp hexponent hcard) v
theorem

ideleClassNorm_range_eq_top_of_splitsCompletely_outside

L160 ↗
GlobalClassFieldTheory.Cohomology.ideleClassNorm_range_eq_top_of_splitsCompletely_outside
Documentation

If every finite place outside a finite set splits completely, then idelic approximation shows that every idele class is a norm.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
namespace GlobalClassFieldTheory
namespace Cohomology
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
Lean source · statement
theorem ideleClassNorm_range_eq_top_of_splitsCompletely_outside
    {E : Type}
    [Field E] [NumberField E] [Algebra K E]
    [FiniteDimensional K E] [IsGalois K E]
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (hsplit :
      ∀ v : HeightOneSpectrum (𝓞 K), v ∉ S →
        FinitePlaceSplitsCompletely
          (K := K) (L := E) v) :
    (RelativeIdeleGroup.Cohomology.ideleClassNorm K E).range = ⊤
theorem

ideleClassNorm_index_eq_one_of_splitsCompletely_outside

L237 ↗
GlobalClassFieldTheory.Cohomology.ideleClassNorm_index_eq_one_of_splitsCompletely_outside
Documentation

The preceding surjectivity says that the idele-class norm index is one.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
namespace GlobalClassFieldTheory
namespace Cohomology
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
Lean source · statement
theorem ideleClassNorm_index_eq_one_of_splitsCompletely_outside
    {E : Type}
    [Field E] [NumberField E] [Algebra K E]
    [FiniteDimensional K E] [IsGalois K E]
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (hsplit :
      ∀ v : HeightOneSpectrum (𝓞 K), v ∉ S →
        FinitePlaceSplitsCompletely
          (K := K) (L := E) v) :
    (RelativeIdeleGroup.Cohomology.ideleClassNorm K E).range.index = 1
theorem

cyclic_prime_power_fullDecompositionPlaces_infinite_of_primeSubextension_normIndex

L255 ↗
GlobalClassFieldTheory.Cohomology.cyclic_prime_power_fullDecompositionPlaces_infinite_of_primeSubextension_normIndex
Documentation

Assuming the norm-index lower bound for the chosen prime-degree subextension, the set of finite places whose decomposition group is the whole Galois group is infinite.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
namespace GlobalClassFieldTheory
namespace Cohomology
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
Lean source · statement
theorem
    cyclic_prime_power_fullDecompositionPlaces_infinite_of_primeSubextension_normIndex
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard : Nat.card (L ≃ₐ[K] L) = p ^ exponent)
    (hLower :
      p ≤
        (RelativeIdeleGroup.Cohomology.ideleClassNorm K
          (cyclicPrimeSubextension
            (K := K) (L := L)
            hp hexponent hcard)).range.index) :
    Set.Infinite
      {v : HeightOneSpectrum (𝓞 K) |
        finitePlaceDecompositionGroup
            (K := K) (L := L) v = ⊤}
theorem

cyclic_prime_power_infinite_fullDecompositionPlaces

L308 ↗
GlobalClassFieldTheory.Cohomology.cyclic_prime_power_infinite_fullDecompositionPlaces
Documentation

In a cyclic extension of prime-power degree, infinitely many finite places have full decomposition group. The norm-index input in the preceding theorem is supplied by the unconditional lower bound for the chosen degree-p subextension.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
namespace GlobalClassFieldTheory
namespace Cohomology
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
Lean source · statement
theorem cyclic_prime_power_infinite_fullDecompositionPlaces
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard : Nat.card (L ≃ₐ[K] L) = p ^ exponent) :
    Set.Infinite
      {v : HeightOneSpectrum (𝓞 K) |
        finitePlaceDecompositionGroup
            (K := K) (L := L) v = ⊤}
theorem

exists_fullDecompositionPlace_outside_finset_of_primeSubextension_normIndex

L350 ↗
GlobalClassFieldTheory.Cohomology.exists_fullDecompositionPlace_outside_finset_of_primeSubextension_normIndex
Documentation

Finset-avoidance form of the conditional full-decomposition infinitude result, convenient for recursively choosing new places.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
namespace GlobalClassFieldTheory
namespace Cohomology
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
Lean source · statement
theorem
    exists_fullDecompositionPlace_outside_finset_of_primeSubextension_normIndex
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard : Nat.card (L ≃ₐ[K] L) = p ^ exponent)
    (hLower :
      p ≤
        (RelativeIdeleGroup.Cohomology.ideleClassNorm K
          (cyclicPrimeSubextension
            (K := K) (L := L)
            hp hexponent hcard)).range.index)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    ∃ v : HeightOneSpectrum (𝓞 K),
      v ∉ S ∧
      finitePlaceDecompositionGroup
          (K := K) (L := L) v = ⊤
theorem

exists_fullDecompositionPlace_outside_finset

L381 ↗
GlobalClassFieldTheory.Cohomology.exists_fullDecompositionPlace_outside_finset
Documentation

Finset-avoidance form of the unconditional full-decomposition infinitude theorem.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open RelativeIdeleGroup.Cohomology
namespace GlobalClassFieldTheory
namespace Cohomology
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
Lean source · statement
theorem exists_fullDecompositionPlace_outside_finset
    {p exponent : ℕ}
    (hp : p.Prime)
    (hexponent : 0 < exponent)
    (hcard : Nat.card (L ≃ₐ[K] L) = p ^ exponent)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    ∃ v : HeightOneSpectrum (𝓞 K),
      v ∉ S ∧
      finitePlaceDecompositionGroup
          (K := K) (L := L) v = ⊤

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.