Module

MaximalAbelianFiniteProjection.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.MaximalAbelianFiniteProjection

2 declarations indexed from sourceView source ↗

Module documentation

Finite projections detect maximal-abelian Artin values

The existing infinite-Galois inverse-limit equivalence detects equality of maximal-abelian automorphisms on finite Galois intermediate fields. On the Artin side, projection at a finite one-place idele is the actual chosen finite-place Artin symbol. These two interfaces close the finite part of local-global Artin comparison without a new comparison assumption.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.MaximalAbelianGlobalArtin

Imported by3

theorem

maximalAbelianGalois_ext_of_finite_restrictions

L30 ↗

ClassFieldTower.Martinet.Shafarevich.maximalAbelianGalois_ext_of_finite_restrictions

Documentation

Equality in the maximal-abelian Galois group is detected by all finite Galois restriction maps, by the existing inverse-limit equivalence.

Source context 7 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]
omit [NumberField F] in

Lean source · statement

theorem maximalAbelianGalois_ext_of_finite_restrictions
    (sigma tau : Gal(_root_.maximalAbelianExtension F/F))
    (h : ∀ E : FiniteGaloisIntermediateField F (_root_.maximalAbelianExtension F),
      AlgEquiv.restrictNormalHom E sigma = AlgEquiv.restrictNormalHom E tau) :
    sigma = tau

theorem

maximalAbelianGlobalArtin_finitePlace_finiteProjection

L42 ↗

ClassFieldTower.Martinet.Shafarevich.maximalAbelianGlobalArtin_finitePlace_finiteProjection

Documentation

The finite projection of a maximal-abelian Artin value at a one-place idele is the actual chosen finite-place Artin symbol.

Source context 6 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open GlobalClassFieldTheory.Reciprocity
variable (F : Type) [Field F] [NumberField F]

Lean source · full declaration

theorem maximalAbelianGlobalArtin_finitePlace_finiteProjection
    (v : HeightOneSpectrum (𝓞 F)) (a : (v.adicCompletion F)ˣ)
    (E : FiniteGaloisIntermediateField F (_root_.maximalAbelianExtension F)) :
    let : NumberField E := NumberField.of_module_finite F E
    AlgEquiv.restrictNormalHom E
      (maximalAbelianGlobalArtin F (IdeleGroup.finitePlaceIdeleClass v a)) =
      chosenFinitePlaceArtinMonoidHom (K := F) (L := E) v a := by
  let : NumberField E := NumberField.of_module_finite F E
  exact (maximalAbelianGlobalArtin_finiteProjection F (IdeleGroup.finitePlaceIdele v a) E).trans
    (globalArtinMonoidHom_finitePlaceIdele (K := F) (L := E) v a)

Module documentation

Finite projections detect maximal-abelian Artin values

Declarations

maximalAbelianGalois_ext_of_finite_restrictions

maximalAbelianGlobalArtin_finitePlace_finiteProjection