NYLL
Module

RealProPFrobeniusFixedFieldSplitting.lean

Nyll.SawinTotallyRealTowers.RealProPFrobeniusFixedFieldSplitting
5 declarations indexed from sourceView source ↗

Module documentation

Complete splitting in every finite layer of the actual cut field

The actual quotient kills the absolute decomposition groups at selected unramified primes. Thus those groups fix the cut field elementwise. The proved restriction-image theorem for decomposition groups then gives complete splitting in every finite Galois layer inside that field.

Imports12
Imported by2

Declarations

instance

finiteCutLayerIsGalois

L36 ↗
ClassFieldTower.Sawin.finiteCutLayerIsGalois
Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich AlgebraicNumberTheory.Valuations
Lean source · statement
instance finiteCutLayerIsGalois
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) :
    IsGalois ℚ E.toIntermediateField
theorem

finitePlaceSplitsCompletely_of_absoluteDecomposition_trivial

L42 ↗
ClassFieldTower.Sawin.finitePlaceSplitsCompletely_of_absoluteDecomposition_trivial
Documentation

Trivial absolute decomposition action on an actual finite Galois layer implies complete splitting there.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich AlgebraicNumberTheory.Valuations
private local instance finiteCutLayerIsGalois
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) :
    IsGalois ℚ E.toIntermediateField := E.isGalois
Lean source · statement
theorem finitePlaceSplitsCompletely_of_absoluteDecomposition_trivial
    (F : Type) [Field F] [NumberField F]
    (E : FiniteGaloisIntermediateField F (AlgebraicClosure F))
    (w : HeightOneSpectrum (𝓞 F))
    (h : ∀ σ : finitePlaceAbsoluteDecompositionGroup F w,
      AlgEquiv.restrictNormalHom E σ.1 = 1) :
    FinitePlaceSplitsCompletely (K := F) (L := E) w
theorem

realProPFrobeniusFixedField_absoluteDecomposition_fixes

L68 ↗
ClassFieldTower.Sawin.realProPFrobeniusFixedField_absoluteDecomposition_fixes
Documentation

At a selected place outside the original support, the actual absolute decomposition group fixes every element of the cut field.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich AlgebraicNumberTheory.Valuations
private local instance finiteCutLayerIsGalois
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) :
    IsGalois ℚ E.toIntermediateField := E.isGalois
Lean source · statement
theorem realProPFrobeniusFixedField_absoluteDecomposition_fixes
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (v : ℕ → HeightOneSpectrum (𝓞 ℚ)) (n : ℕ) (hv : v n ∉ T)
    (σ : finitePlaceAbsoluteDecompositionGroup ℚ (v n))
    (x : AlgebraicClosure ℚ) (hx : x ∈ realProPFrobeniusFixedField p T v) :
    σ.1 x = x
theorem

realProPFrobeniusFixedField_finiteLayer_splits

L87 ↗
ClassFieldTower.Sawin.realProPFrobeniusFixedField_finiteLayer_splits
Documentation

Every finite Galois layer in the actual cut field splits at every selected place outside the original ramification support.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich AlgebraicNumberTheory.Valuations
private local instance finiteCutLayerIsGalois
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) :
    IsGalois ℚ E.toIntermediateField := E.isGalois
Lean source · statement
theorem realProPFrobeniusFixedField_finiteLayer_splits
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (v : ℕ → HeightOneSpectrum (𝓞 ℚ))
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ))
    (hE : E.toIntermediateField ≤ realProPFrobeniusFixedField p T v)
    (n : ℕ) (hv : v n ∉ T) :
    FinitePlaceSplitsCompletely (K := ℚ) (L := E) (v n)
theorem

exists_sawinInfinite_totallyReal_split_field

L106 ↗
ClassFieldTower.Sawin.exists_sawinInfinite_totallyReal_split_field
Documentation

The unconditional S3 quotient gives an actual infinite Galois, totally real field and infinitely many completely split primes in all its finite Galois layers.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich AlgebraicNumberTheory.Valuations
private local instance finiteCutLayerIsGalois
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) :
    IsGalois ℚ E.toIntermediateField := E.isGalois
Lean source · statement
theorem exists_sawinInfinite_totallyReal_split_field :
    ∃ primes : ℕ → Nat.Primes, ∃ L : IntermediateField ℚ (AlgebraicClosure ℚ),
      IsGalois ℚ L ∧ IsTotallyReal L ∧ Infinite (L ≃ₐ[ℚ] L) ∧
      L ≤ maximalRealProPOutside 2 sawinRationalPrimeSupport ∧
      (∀ n : ℕ, n < (primes n).val ∧
        (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n) ∉
          sawinRationalPrimeSupport ∧ (primes n).val % 4 = 1) ∧
      (Set.range primes).Infinite ∧
      ∀ E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ),
        E.toIntermediateField ≤ L → ∀ n : ℕ,
          FinitePlaceSplitsCompletely (K := ℚ) (L := E)
            ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n))

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