Module

FinitePlaceDecomposition.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.SUnitKummerPrimeSelection.FinitePlaceDecomposition

2 declarations indexed from sourceView source ↗

Module documentation

Finite-place decomposition groups in Galois towers

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

Imports4

Imported by3

theorem

restrictAutomorphismScalars_mem_finitePlaceDecompositionGroup_of_relative_eq_top

L34 ↗

GlobalClassFieldTheory.ClassFieldAxiom.restrictAutomorphismScalars_mem_finitePlaceDecompositionGroup_of_relative_eq_top

Documentation

Full relative decomposition above q puts every M-automorphism inside the global chosen decomposition group below q.

Source context 5 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
open _root_.HilbertRamification
  (decompositionGroupRestriction_mem_absoluteValueDecompositionGroup_restrictScalars_iff) in

Lean source · statement

theorem
    restrictAutomorphismScalars_mem_finitePlaceDecompositionGroup_of_relative_eq_top
    {F M L : Type}
    [Field F] [NumberField F]
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra F M] [Algebra M L] [Algebra F L]
    [IsScalarTower F M L]
    [FiniteDimensional F L]
    [FiniteDimensional M L]
    [IsGalois F L] [IsGalois M L]
    [IsMulCommutative (L ≃ₐ[F] L)]
    (p : HeightOneSpectrum (𝓞 F))
    (q : HeightOneSpectrum (𝓞 M))
    (hq :
      _root_.finitePlaceBelow (K := F) q = p)
    (hfull :
      _root_.finitePlaceDecompositionGroup
          (K := M) (L := L) q =
        ⊤)
    (tau : L ≃ₐ[M] L) :
    RamificationTheory.HilbertRamification.ValuationSubring.restrictAutomorphismScalars
          (K := F) (M := M) tau ∈
      _root_.finitePlaceDecompositionGroup
        (K := F) (L := L) p

theorem

finitePlaceDecompositionGroup_isCyclic_of_chosenUnramified

L152 ↗

GlobalClassFieldTheory.ClassFieldAxiom.finitePlaceDecompositionGroup_isCyclic_of_chosenUnramified