NYLL
Module

SeparableClosurePadicLift.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.LocalGlobalArtinCompatibility.SeparableClosurePadicLift
33 declarations indexed from sourceView source ↗

Module documentation

Separable-closure p-adic lifts for local-global Artin compatibility

This module constructs the finite-place decomposition restriction maps and the positive p-adic cyclotomic lifts used in the local-global comparison.

Imports4
Imported by4

Declarations

instance

(anonymous instance)

L38 ↗
Source context 9 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
Lean source · statement
instance (p : Nat.Primes) : Fact p.1.Prime
theorem

numberFieldTowerExtensionQuotientEquivGaloisGroup_mk_apply

L44 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerExtensionQuotientEquivGaloisGroup_mk_apply
Documentation

Evaluation of the compatible finite quotient on an arbitrary ambient representative is the action of that representative on the chosen embedded copy of the top field.

Source context 10 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
theorem numberFieldTowerExtensionQuotientEquivGaloisGroup_mk_apply
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (x : L) :
    numberFieldSeparableClosureEmbedding L
        (numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          ((numberFieldTowerFiniteGaloisSubextension K L).extensionQuotientMk
            τ) x) =
      τ.1 (numberFieldSeparableClosureEmbedding L x)
def

automorphismCyclicFixedField

L75 ↗
GlobalClassFieldTheory.Reciprocity.automorphismCyclicFixedField
Documentation

The fixed field of the cyclic subgroup generated by one automorphism of a finite abelian extension.

Passing from K to this field is the genuine cyclic reduction used in the proof of finite-place local--global compatibility: over this field the given automorphism generates the whole Galois group.

Source context 10 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
def automorphismCyclicFixedField
    (σ : Gal(L/K)) :
    IntermediateField K L
instance

automorphismCyclicFixedFieldNumberField

L81 ↗
GlobalClassFieldTheory.Reciprocity.automorphismCyclicFixedFieldNumberField
Source context 10 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ)
def

automorphismOverCyclicFixedField

L89 ↗
GlobalClassFieldTheory.Reciprocity.automorphismOverCyclicFixedField
Documentation

An automorphism, regarded over the fixed field of the cyclic subgroup it generates.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · statement
def automorphismOverCyclicFixedField
    (σ : Gal(L/K)) :
    Gal(L / automorphismCyclicFixedField σ)
theorem

automorphismOverCyclicFixedField_restrictScalars

L105 ↗
GlobalClassFieldTheory.Reciprocity.automorphismOverCyclicFixedField_restrictScalars
Documentation

Restricting the automorphism over its cyclic fixed field back to the base field recovers the original automorphism.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [NumberField K] [NumberField L] [IsAbelianGalois K L] in
Lean source · statement
theorem automorphismOverCyclicFixedField_restrictScalars
    (σ : Gal(L/K)) :
    (automorphismOverCyclicFixedField σ).restrictScalars K = σ
theorem

automorphismOverCyclicFixedField_generates

L114 ↗
GlobalClassFieldTheory.Reciprocity.automorphismOverCyclicFixedField_generates
Documentation

The automorphism over its cyclic fixed field genuinely generates the entire relative Galois group.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [NumberField K] [NumberField L] [IsAbelianGalois K L] in
Lean source · statement
theorem automorphismOverCyclicFixedField_generates
    (σ : Gal(L/K)) :
    Subgroup.closure
        ({automorphismOverCyclicFixedField σ} :
          Set
            (Gal(L / automorphismCyclicFixedField σ))) =
      ⊤
def

automorphismCyclicFixedPlace

L164 ↗
GlobalClassFieldTheory.Reciprocity.automorphismCyclicFixedPlace
Documentation

The finite place of the cyclic fixed field obtained by restricting the chosen extension of v to that field and taking its centre.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
def automorphismCyclicFixedPlace
    (v : HeightOneSpectrum (𝓞 K))
    (σ : Gal(L/K)) :
    let M := automorphismCyclicFixedField σ
    HeightOneSpectrum (𝓞 M) := by
  dsimp only
  let M := automorphismCyclicFixedField σ
  exact
    finitePlaceExtensionCentre
      (K := K) (L := M) v
      (restrictFinitePlaceExtension
        (K := K) (L := L) (E := M) v
        (chosenFinitePlaceExtension (L := L) v))
theorem

finitePlaceBelow_automorphismCyclicFixedPlace

L182 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceBelow_automorphismCyclicFixedPlace
Documentation

The finite place induced on the cyclic fixed field lies above the original base-field place.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [NumberField L] in
Lean source · statement
theorem finitePlaceBelow_automorphismCyclicFixedPlace
    (v : HeightOneSpectrum (𝓞 K))
    (σ : Gal(L/K)) :
    finitePlaceBelow (K := K)
        (automorphismCyclicFixedPlace v σ) =
      v
theorem

finitePlaceBelow_chosenExtensionCentre_eq_automorphismCyclicFixedPlace

L200 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceBelow_chosenExtensionCentre_eq_automorphismCyclicFixedPlace
Documentation

The centre in L of the originally chosen extension of v lies above the cyclic-reduction place. This identifies the exact upper place used in the norm--restriction square without making a new valuation choice.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
theorem finitePlaceBelow_chosenExtensionCentre_eq_automorphismCyclicFixedPlace
    (v : HeightOneSpectrum (𝓞 K))
    (σ : Gal(L/K)) :
    let M := automorphismCyclicFixedField σ
    finitePlaceBelow (K := M)
        (finitePlaceExtensionCentre
          (K := K) (L := L) v
          (chosenFinitePlaceExtension (L := L) v)) =
      automorphismCyclicFixedPlace v σ := by
  dsimp only
  let M := automorphismCyclicFixedField σ
  let w :=
    chosenFinitePlaceExtension (L := L) v
  let wM :=
    restrictFinitePlaceExtension
      (K := K) (L := L) (E := M) v w
  apply HeightOneSpectrum.ext
  ext x
  change
    algebraMap (𝓞 M) (𝓞 L) x ∈
        finitePlaceExtensionCentreIdeal
          (K := K) (L := L) v w ↔
      x ∈
        finitePlaceExtensionCentreIdeal
          (K := K) (L := M) v wM
  rw [
    mem_finitePlaceExtensionCentreIdeal_iff,
    mem_finitePlaceExtensionCentreIdeal_iff]
  rfl
def

automorphismCyclicFixedTopExtension

L233 ↗
GlobalClassFieldTheory.Reciprocity.automorphismCyclicFixedTopExtension
Documentation

The exact extension of the normalized finite absolute value at the cyclic-reduction place whose centre is the original chosen place of L.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
def automorphismCyclicFixedTopExtension
    (v : HeightOneSpectrum (𝓞 K))
    (σ : Gal(L/K)) :
    let M := automorphismCyclicFixedField σ
    AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv M
        (automorphismCyclicFixedPlace v σ)) L := by
  dsimp only
  let M := automorphismCyclicFixedField σ
  let W :=
    automorphismCyclicFixedPlace v σ
  let V :
      {V : HeightOneSpectrum (𝓞 L) //
        finitePlaceBelow (K := M) V = W} :=
    ⟨finitePlaceExtensionCentre
        (K := K) (L := L) v
        (chosenFinitePlaceExtension (L := L) v),
      finitePlaceBelow_chosenExtensionCentre_eq_automorphismCyclicFixedPlace
        (K := K) (L := L) v σ⟩
  exact
    (finitePlaceExtensionEquivAbove
      (K := M) (L := L) W).symm V
theorem

automorphismCyclicFixedTopExtension_centre

L259 ↗
GlobalClassFieldTheory.Reciprocity.automorphismCyclicFixedTopExtension_centre
Documentation

The chosen top extension above the cyclic fixed place has the same centre as the original chosen extension over the base field.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
theorem automorphismCyclicFixedTopExtension_centre
    (v : HeightOneSpectrum (𝓞 K))
    (σ : Gal(L/K)) :
    let M := automorphismCyclicFixedField σ
    finitePlaceExtensionCentre
        (K := M) (L := L)
        (automorphismCyclicFixedPlace v σ)
        (automorphismCyclicFixedTopExtension v σ) =
      finitePlaceExtensionCentre
        (K := K) (L := L) v
        (chosenFinitePlaceExtension (L := L) v) := by
  dsimp only
  let M := automorphismCyclicFixedField σ
  let W :=
    automorphismCyclicFixedPlace v σ
  let V :
      {V : HeightOneSpectrum (𝓞 L) //
        finitePlaceBelow (K := M) V = W} :=
    ⟨finitePlaceExtensionCentre
        (K := K) (L := L) v
        (chosenFinitePlaceExtension (L := L) v),
      finitePlaceBelow_chosenExtensionCentre_eq_automorphismCyclicFixedPlace
        (K := K) (L := L) v σ⟩
  have h :=
    congrArg Subtype.val
      ((finitePlaceExtensionEquivAbove
        (K := M) (L := L) W).apply_symm_apply V)
  simpa only [
    finitePlaceExtensionEquivAbove_coe,
    V, W, id_eq,
    automorphismCyclicFixedTopExtension
  ] using h
theorem

automorphismOverCyclicFixedField_mem_chosenFinitePlaceDecompositionGroup

L295 ↗
GlobalClassFieldTheory.Reciprocity.automorphismOverCyclicFixedField_mem_chosenFinitePlaceDecompositionGroup
Documentation

A decomposition automorphism remains in the decomposition group at the chosen place after the cyclic fixed-field reduction. This is the lightweight geometric statement underlying the corresponding local Artin range result.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
theorem automorphismOverCyclicFixedField_mem_chosenFinitePlaceDecompositionGroup
    (v : HeightOneSpectrum (𝓞 K))
    (σ :
      absoluteValueDecompositionGroup K
        (chosenFinitePlaceExtension (L := L) v).1) :
    let M := automorphismCyclicFixedField σ.1
    automorphismOverCyclicFixedField σ.1 ∈
      absoluteValueDecompositionGroup M
        (chosenFinitePlaceExtension
          (L := L) (automorphismCyclicFixedPlace v σ.1)).1 := by
  dsimp only
  let M :=
    automorphismCyclicFixedField σ.1
  let W :=
    automorphismCyclicFixedPlace v σ.1
  let wK :=
    chosenFinitePlaceExtension (L := L) v
  let wM :=
    automorphismCyclicFixedTopExtension v σ.1
  let σM : Gal(L / M) :=
    automorphismOverCyclicFixedField σ.1
  have hrestrict :
      RamificationTheory.HilbertRamification.ValuationSubring.restrictAutomorphismScalars
          (K := K) (M := M) σM =
        σ.1 := by
    apply AlgEquiv.ext
    intro x
    rfl
  have hσM_wK :
      σM ∈
        absoluteValueDecompositionGroup M wK.1 := by
    apply
      (decompositionGroupRestriction_mem_absoluteValueDecompositionGroup_restrictScalars_iff
        (K := K) (M := M) wK.1 σM).mp
    simpa only [hrestrict] using σ.2
  have hequiv :
      wK.1.IsEquiv wM.1 := by
    apply
      finitePlaceExtensions_isEquiv_of_centres_eq
        (F := K) (M := M) v W wK wM
    exact
      (automorphismCyclicFixedTopExtension_centre
        (K := K) (L := L) v σ.1).symm
  have hσM_wM :
      σM ∈
        absoluteValueDecompositionGroup M wM.1 := by
    rw [
      ←
        absoluteValueDecompositionGroup_eq_of_absoluteValue_isEquiv
          (F := M) wK.1 wM.1 hequiv]
    exact hσM_wK
  have hσM_chosen :
      σM ∈
        absoluteValueDecompositionGroup M
          (chosenFinitePlaceExtension (L := L) W).1 := by
    rw [
      ←
        absoluteValueDecompositionGroup_eq_of_exactExtensions_of_isMulCommutative
          (F := M)
          (NumberField.HeightOneSpectrum.adicAbv M W)
          (RayClass.adicAbv_isNontrivial W)
          wM
          (chosenFinitePlaceExtension (L := L) W)]
    exact hσM_wM
  exact hσM_chosen
theorem

automorphismOverCyclicFixedField_mem_chosenFinitePlaceArtin_range

L364 ↗
GlobalClassFieldTheory.Reciprocity.automorphismOverCyclicFixedField_mem_chosenFinitePlaceArtin_range
Documentation

A decomposition automorphism remains a decomposition automorphism after the cyclic fixed-field reduction, for the actual chosen local Artin factor over the reduced base.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
theorem automorphismOverCyclicFixedField_mem_chosenFinitePlaceArtin_range
    (v : HeightOneSpectrum (𝓞 K))
    (σ :
      absoluteValueDecompositionGroup K
        (chosenFinitePlaceExtension (L := L) v).1) :
    let M := automorphismCyclicFixedField σ.1
    automorphismOverCyclicFixedField σ.1 ∈
      (chosenFinitePlaceArtinMonoidHom
        (K := M) (L := L)
        (automorphismCyclicFixedPlace v σ.1)).range := by
  dsimp only
  rw [
    chosenFinitePlaceArtinMonoidHom_range
      (K := automorphismCyclicFixedField σ.1) (L := L)
      (automorphismCyclicFixedPlace v σ.1)]
  exact
    automorphismOverCyclicFixedField_mem_chosenFinitePlaceDecompositionGroup
      (K := K) (L := L) v σ
def

finitePlaceSeparableClosureDecompositionRestriction

L389 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureDecompositionRestriction
Documentation

Restriction from the decomposition group in the common compatible rational separable closure to the decomposition group at the chosen finite place of L.

The codomain is transported along the proved equality between the restricted ambient absolute value and the supplied exact extension.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
def finitePlaceSeparableClosureDecompositionRestriction
    (v : HeightOneSpectrum (𝓞 K)) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    let wL :=
      chosenFinitePlaceExtension (L := L) v
    let wΩ :=
      numberFieldTowerFinitePlaceExtensionToSeparableClosure
        K L v wL
    absoluteValueDecompositionGroup K wΩ.1 →*
      absoluteValueDecompositionGroup K wL.1 := by
  letI : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  letI : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  letI : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  dsimp only
  let wL :=
    chosenFinitePlaceExtension (L := L) v
  let wΩ :=
    numberFieldTowerFinitePlaceExtensionToSeparableClosure
      K L v wL
  exact
    { toFun := fun τ =>
        ⟨AlgEquiv.restrictNormalHom L τ.1,
          by
            intro x
            change
              wL.1
                  ((AlgEquiv.restrictNormalHom L τ.1) x) < 1 ↔
                wL.1 x < 1
            rw [
              ←
                numberFieldTowerFinitePlaceExtensionToSeparableClosure_algebraMap
                  K L v wL
                    ((AlgEquiv.restrictNormalHom L τ.1) x),
              ←
                numberFieldTowerFinitePlaceExtensionToSeparableClosure_algebraMap
                  K L v wL x]
            have hcomm :
                algebraMap L (SeparableClosure ℚ)
                    ((AlgEquiv.restrictNormalHom L τ.1) x) =
                  τ.1 (algebraMap L (SeparableClosure ℚ) x) := by
              exact AlgEquiv.restrictNormal_commutes τ.1 L x
            rw [hcomm]
            exact τ.2 (algebraMap L (SeparableClosure ℚ) x)⟩
      map_one' := by
        apply Subtype.ext
        exact
          map_one
            (AlgEquiv.restrictNormalHom
              (F := K) (K₁ := SeparableClosure ℚ) L)
      map_mul' := by
        intro τ η
        apply Subtype.ext
        exact
          map_mul
            (AlgEquiv.restrictNormalHom
              (F := K) (K₁ := SeparableClosure ℚ) L)
            τ.1 η.1 }
theorem

finitePlaceSeparableClosureDecompositionRestriction_coe

L459 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureDecompositionRestriction_coe
Documentation

On underlying automorphisms, the compatible finite-place restriction is the ordinary normal-field restriction.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem finitePlaceSeparableClosureDecompositionRestriction_coe
    (v : HeightOneSpectrum (𝓞 K)) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    ∀ (τ :
      let wΩ :=
        numberFieldTowerFinitePlaceExtensionToSeparableClosure
          K L v (chosenFinitePlaceExtension (L := L) v)
      absoluteValueDecompositionGroup K wΩ.1),
    ((finitePlaceSeparableClosureDecompositionRestriction
        (K := K) (L := L) v) τ :
      Gal(L / K)) =
      AlgEquiv.restrictNormalHom L τ.1 := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  intro τ
  rfl
theorem

finitePlaceSeparableClosureDecompositionRestriction_surjective

L488 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureDecompositionRestriction_surjective
Documentation

The compatible separable-closure restriction is onto the actual decomposition group at the chosen finite place.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem finitePlaceSeparableClosureDecompositionRestriction_surjective
    (v : HeightOneSpectrum (𝓞 K)) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    Function.Surjective
      (finitePlaceSeparableClosureDecompositionRestriction
        (K := K) (L := L) v) := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  dsimp only
  let separableClosurePadicLiftBaseIsGalois :
      IsGalois K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosure_isGalois K L
  let wL :=
    chosenFinitePlaceExtension (L := L) v
  let wΩ :=
    numberFieldTowerFinitePlaceExtensionToSeparableClosure
      K L v wL
  let r :=
    absoluteValueDecompositionGroupRestrictionHom
      (K := K) (L := L) (Ω := SeparableClosure ℚ) wΩ.1
  have hr : Function.Surjective r :=
    absoluteValueDecompositionGroupRestrictionHom_surjective
      (K := K) (L := L) (Ω := SeparableClosure ℚ)
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (RayClass.adicAbv_isNontrivial v) wΩ
  have hw :
      wΩ.1.comp
          (f := algebraMap L (SeparableClosure ℚ))
          (algebraMap L (SeparableClosure ℚ)).injective =
        wL.1 :=
    numberFieldTowerFinitePlaceExtensionToSeparableClosure_restrict
      K L v wL
  let σToRestricted :
      absoluteValueDecompositionGroup K wL.1 →
      absoluteValueDecompositionGroup K
        (wΩ.1.comp
          (f := algebraMap L (SeparableClosure ℚ))
          (algebraMap L (SeparableClosure ℚ)).injective) :=
    fun σ =>
      ⟨σ.1, by
        simpa only [hw] using σ.2⟩
  intro σ
  obtain ⟨τ, hτ⟩ := hr (σToRestricted σ)
  refine ⟨τ, ?_⟩
  apply Subtype.ext
  change (r τ).1 = (σToRestricted σ).1
  exact congrArg
    (fun ρ :
      absoluteValueDecompositionGroup K
        (wΩ.1.comp
          (f := algebraMap L (SeparableClosure ℚ))
          (algebraMap L (SeparableClosure ℚ)).injective) => ρ.1)
    hτ
def

finitePlaceSeparableClosureTopDecompositionInclusion

L553 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureTopDecompositionInclusion
Documentation

Scalar restriction embeds the decomposition group over L into the compatible decomposition group over K.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
def
    finitePlaceSeparableClosureTopDecompositionInclusion
    (v : HeightOneSpectrum (𝓞 K)) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    let wΩ :=
      numberFieldTowerFinitePlaceExtensionToSeparableClosure
        K L v (chosenFinitePlaceExtension (L := L) v)
    absoluteValueDecompositionGroup L wΩ.1 →*
      absoluteValueDecompositionGroup K wΩ.1 := by
  letI : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  letI : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  letI : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  dsimp only
  let wΩ :=
    numberFieldTowerFinitePlaceExtensionToSeparableClosure
      K L v (chosenFinitePlaceExtension (L := L) v)
  exact
    { toFun := fun τ =>
        ⟨RamificationTheory.HilbertRamification.ValuationSubring.restrictAutomorphismScalars
              (K := K) (M := L) τ.1,
          (decompositionGroupRestriction_mem_absoluteValueDecompositionGroup_restrictScalars_iff
            (K := K) (M := L) wΩ.1 τ.1).2 τ.2⟩
      map_one' := by
        apply Subtype.ext
        rfl
      map_mul' := by
        intro τ η
        apply Subtype.ext
        rfl }
theorem

finitePlaceSeparableClosureTopDecompositionInclusion_range

L595 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureTopDecompositionInclusion_range
Documentation

The image of the top-field decomposition group is exactly the kernel of restriction to the chosen finite-place decomposition group of L.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem
    finitePlaceSeparableClosureTopDecompositionInclusion_range
    (v : HeightOneSpectrum (𝓞 K)) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    (finitePlaceSeparableClosureTopDecompositionInclusion
        (K := K) (L := L) v).range =
      (finitePlaceSeparableClosureDecompositionRestriction
        (K := K) (L := L) v).ker := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let wL :=
    chosenFinitePlaceExtension (L := L) v
  let wΩ :=
    numberFieldTowerFinitePlaceExtensionToSeparableClosure
      K L v wL
  ext τ
  constructor
  · rintro ⟨η, rfl⟩
    rw [MonoidHom.mem_ker]
    apply Subtype.ext
    apply AlgEquiv.ext
    intro x
    simp only [
      finitePlaceSeparableClosureDecompositionRestriction_coe]
    apply (algebraMap L (SeparableClosure ℚ)).injective
    calc
      algebraMap L (SeparableClosure ℚ)
            ((AlgEquiv.restrictNormalHom L
              ((finitePlaceSeparableClosureTopDecompositionInclusion
                (K := K) (L := L) v) η).1) x) =
          ((finitePlaceSeparableClosureTopDecompositionInclusion
              (K := K) (L := L) v) η).1
            (algebraMap L (SeparableClosure ℚ) x) :=
        AlgEquiv.restrictNormal_commutes
          ((finitePlaceSeparableClosureTopDecompositionInclusion
            (K := K) (L := L) v) η).1 L x
      _ = η.1 (algebraMap L (SeparableClosure ℚ) x) := rfl
      _ = algebraMap L (SeparableClosure ℚ) x := η.1.commutes x
      _ = algebraMap L (SeparableClosure ℚ)
            ((1 : Gal(L / K)) x) := rfl
  · intro hτ
    have hrestriction :
        AlgEquiv.restrictNormalHom L τ.1 = 1 := by
      have hτOne := MonoidHom.mem_ker.mp hτ
      have hτVal := congrArg Subtype.val hτOne
      calc
        AlgEquiv.restrictNormalHom L τ.1 =
            ((1 : absoluteValueDecompositionGroup K wL.1).1 :
              Gal(L / K)) := by
          simpa only [
            finitePlaceSeparableClosureDecompositionRestriction_coe] using
              hτVal
        _ = 1 := rfl
    let η : SeparableClosure ℚ ≃ₐ[L] SeparableClosure ℚ :=
      { τ.1.toRingEquiv with
        commutes' := by
          intro x
          have hcomm :=
            AlgEquiv.restrictNormal_commutes τ.1 L x
          have hx :=
            congrArg (fun ρ : Gal(L / K) => ρ x) hrestriction
          change (τ.1.restrictNormal L) x = x at hx
          calc
            τ.1 (algebraMap L (SeparableClosure ℚ) x) =
                algebraMap L (SeparableClosure ℚ)
                  ((τ.1.restrictNormal L) x) := hcomm.symm
            _ = algebraMap L (SeparableClosure ℚ) x :=
              congrArg (algebraMap L (SeparableClosure ℚ)) hx }
    have hη :
        η ∈ absoluteValueDecompositionGroup L wΩ.1 := by
      intro x
      exact τ.2 x
    refine ⟨⟨η, hη⟩, ?_⟩
    apply Subtype.ext
    apply AlgEquiv.ext
    intro x
    rfl
def

finitePlaceSeparableClosureTopExtension

L685 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureTopExtension
Documentation

The compatible separable-closure absolute value, regarded as an exact extension of the chosen absolute value on the top number field.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
def finitePlaceSeparableClosureTopExtension
    (v : HeightOneSpectrum (𝓞 K)) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    let wL :=
      chosenFinitePlaceExtension (L := L) v
    AbsoluteValueExtension wL.1 (SeparableClosure ℚ) := by
  letI : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  letI : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  letI : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  dsimp only
  let wL :=
    chosenFinitePlaceExtension (L := L) v
  let wΩ :=
    numberFieldTowerFinitePlaceExtensionToSeparableClosure
      K L v wL
  refine ⟨wΩ.1, ?_⟩
  intro x
  exact
    numberFieldTowerFinitePlaceExtensionToSeparableClosure_algebraMap
      K L v wL x
def

finitePlaceCyclotomicCompositumExtension

L716 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceCyclotomicCompositumExtension
Documentation

Restriction of the compatible separable-closure valuation to the actual cyclotomic ZHat-compositum over the top number field.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
def finitePlaceCyclotomicCompositumExtension
    (v : HeightOneSpectrum (𝓞 K)) :
    let wL :=
      chosenFinitePlaceExtension (L := L) v
    AbsoluteValueExtension wL.1
      (numberFieldCyclotomicZHatCompositum L) := by
  letI : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  letI : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  letI : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  letI : IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) :=
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
  dsimp only
  let C :=
    numberFieldCyclotomicZHatCompositum L
  let wL :=
    chosenFinitePlaceExtension (L := L) v
  let wΩL :=
    finitePlaceSeparableClosureTopExtension
      (K := K) (L := L) v
  refine
    ⟨wΩL.1.comp
        (f := algebraMap C (SeparableClosure ℚ))
        (algebraMap C (SeparableClosure ℚ)).injective,
      ?_⟩
  intro x
  change
    wΩL.1
        (algebraMap C (SeparableClosure ℚ)
          (algebraMap L C x)) =
      wL.1 x
  rw [← IsScalarTower.algebraMap_apply L C (SeparableClosure ℚ)]
  exact wΩL.2 x
theorem

finitePlaceCyclotomicCompositumExtension_base_isEquiv

L758 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceCyclotomicCompositumExtension_base_isEquiv
Documentation

The restricted cyclotomic-compositum valuation has the same finite-place class as the normalized valuation at the centre of the chosen extension on the top field.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem finitePlaceCyclotomicCompositumExtension_base_isEquiv
    (v : HeightOneSpectrum (𝓞 K)) :
    let wL :=
      chosenFinitePlaceExtension (L := L) v
    let wC :=
      finitePlaceCyclotomicCompositumExtension
        (K := K) (L := L) v
    (wC.1.comp
        (f := algebraMap L
          (numberFieldCyclotomicZHatCompositum L))
        (algebraMap L
          (numberFieldCyclotomicZHatCompositum L)).injective).IsEquiv
      (NumberField.HeightOneSpectrum.adicAbv L
        (finitePlaceExtensionCentre
          (K := K) (L := L) v wL)) := by
  dsimp only
  let C :=
    numberFieldCyclotomicZHatCompositum L
  let wL :=
    chosenFinitePlaceExtension (L := L) v
  let wC :=
    finitePlaceCyclotomicCompositumExtension
      (K := K) (L := L) v
  have hrestrict :
      wC.1.comp
          (f := algebraMap L C)
          (algebraMap L C).injective =
        wL.1 := by
    ext x
    exact wC.2 x
  change
    (wC.1.comp
        (f := algebraMap L C)
        (algebraMap L C).injective).IsEquiv
      (NumberField.HeightOneSpectrum.adicAbv L
        (finitePlaceExtensionCentre
          (K := K) (L := L) v wL))
  rw [hrestrict]
  exact
    finitePlaceExtension_isEquiv_adicAbv
      (K := K) (L := L) v wL
def

finitePlaceSeparableClosureTopCyclotomicRestriction

L803 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureTopCyclotomicRestriction
Documentation

Restriction from the top-field decomposition group in the compatible separable closure to the decomposition group in the actual cyclotomic ZHat-compositum.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
def
    finitePlaceSeparableClosureTopCyclotomicRestriction
    (v : HeightOneSpectrum (𝓞 K)) :
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower L
        (numberFieldCyclotomicZHatCompositum L)
        (SeparableClosure ℚ) :=
      numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
    let wΩL :=
      finitePlaceSeparableClosureTopExtension
        (K := K) (L := L) v
    let wC :=
      finitePlaceCyclotomicCompositumExtension
        (K := K) (L := L) v
    absoluteValueDecompositionGroup L wΩL.1 →*
      absoluteValueDecompositionGroup L wC.1 := by
  letI : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  letI : IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) :=
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
  dsimp only
  let C :=
    numberFieldCyclotomicZHatCompositum L
  let wΩL :=
    finitePlaceSeparableClosureTopExtension
      (K := K) (L := L) v
  let wC :=
    finitePlaceCyclotomicCompositumExtension
      (K := K) (L := L) v
  have hwC :
      wΩL.1.comp
          (f := algebraMap C (SeparableClosure ℚ))
          (algebraMap C (SeparableClosure ℚ)).injective =
        wC.1 := by
    rfl
  let raw :=
    absoluteValueDecompositionGroupRestrictionHom
      (K := L) (L := C) (Ω := SeparableClosure ℚ)
      wΩL.1
  exact
    { toFun := fun τ =>
        ⟨(raw τ).1, by
          simpa only [hwC] using (raw τ).2⟩
      map_one' := by
        apply Subtype.ext
        exact congrArg Subtype.val (map_one raw)
      map_mul' := by
        intro τ η
        apply Subtype.ext
        exact congrArg Subtype.val (map_mul raw τ η) }
theorem

finitePlaceSeparableClosureTopCyclotomicRestriction_surjective

L861 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureTopCyclotomicRestriction_surjective
Documentation

The top-field decomposition group surjects onto the decomposition group of the actual cyclotomic ZHat-compositum at the restricted place.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem
    finitePlaceSeparableClosureTopCyclotomicRestriction_surjective
    (v : HeightOneSpectrum (𝓞 K)) :
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower L
        (numberFieldCyclotomicZHatCompositum L)
        (SeparableClosure ℚ) :=
      numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
    Function.Surjective
      (finitePlaceSeparableClosureTopCyclotomicRestriction
        (K := K) (L := L) v) := by
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) :=
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
  dsimp only
  let C :=
    numberFieldCyclotomicZHatCompositum L
  let separableClosurePadicLiftTopIsGalois :
      IsGalois L (SeparableClosure ℚ) :=
    numberFieldSeparableClosureTop_isGalois L
  let wL :=
    chosenFinitePlaceExtension (L := L) v
  let wΩL :=
    finitePlaceSeparableClosureTopExtension
      (K := K) (L := L) v
  let wC :=
    finitePlaceCyclotomicCompositumExtension
      (K := K) (L := L) v
  let raw :=
    absoluteValueDecompositionGroupRestrictionHom
      (K := L) (L := C) (Ω := SeparableClosure ℚ) wΩL.1
  have hraw : Function.Surjective raw :=
    absoluteValueDecompositionGroupRestrictionHom_surjective
      (K := L) (L := C) (Ω := SeparableClosure ℚ)
      wL.1
      (wL.isNontrivial
        (RayClass.adicAbv_isNontrivial v))
      wΩL
  have hwC :
      wΩL.1.comp
          (f := algebraMap C (SeparableClosure ℚ))
          (algebraMap C (SeparableClosure ℚ)).injective =
        wC.1 := by
    rfl
  intro σ
  let σRaw :
      absoluteValueDecompositionGroup L
        (wΩL.1.comp
          (f := algebraMap C (SeparableClosure ℚ))
          (algebraMap C (SeparableClosure ℚ)).injective) :=
    ⟨σ.1, by
      rw [hwC]
      exact σ.2⟩
  obtain ⟨τ, hτ⟩ := hraw σRaw
  refine ⟨τ, ?_⟩
  apply Subtype.ext
  change (raw τ).1 = σRaw.1
  exact congrArg
    (fun ρ :
      absoluteValueDecompositionGroup L
        (wΩL.1.comp
          (f := algebraMap C (SeparableClosure ℚ))
          (algebraMap C (SeparableClosure ℚ)).injective) => ρ.1)
    hτ
def

finitePlaceSeparableClosureCyclotomicRestriction

L932 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureCyclotomicRestriction
Documentation

Restriction of the compatible separable-closure decomposition group to the actual rational cyclotomic ZHat-field.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
def finitePlaceSeparableClosureCyclotomicRestriction
    (v : HeightOneSpectrum (𝓞 K)) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    let wΩ :=
      numberFieldTowerFinitePlaceExtensionToSeparableClosure
        K L v (chosenFinitePlaceExtension (L := L) v)
    absoluteValueDecompositionGroup K wΩ.1 →*
      Gal(rationalCyclotomicZHatField / ℚ) :=
  by
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    letI : Normal ℚ rationalCyclotomicZHatField :=
      rationalCyclotomicZHatField_normal
    exact
      (AlgEquiv.restrictNormalHom
          rationalCyclotomicZHatField).comp
        ((AlgEquiv.restrictScalarsHom ℚ).comp
          (absoluteValueDecompositionGroup K
            (numberFieldTowerFinitePlaceExtensionToSeparableClosure
              K L v
                (chosenFinitePlaceExtension (L := L) v)).1).subtype)
def

finitePlaceSeparableClosurePadicCyclotomicDegree

L969 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosurePadicCyclotomicDegree
Documentation

The genuine p-adic cyclotomic degree on the compatible separable-closure decomposition group.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · full declaration
def finitePlaceSeparableClosurePadicCyclotomicDegree
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    let wΩ :=
      numberFieldTowerFinitePlaceExtensionToSeparableClosure
        K L v (chosenFinitePlaceExtension (L := L) v)
    absoluteValueDecompositionGroup K wΩ.1 →*
      Multiplicative ℤ_[p.1] :=
  by
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    exact
      (rationalCyclotomicPadicCoordinate p).toMonoidHom.comp
        (finitePlaceSeparableClosureCyclotomicRestriction
          (K := K) (L := L) v)
theorem

finitePlaceSeparableClosureTopCyclotomicRestriction_padicDegree

L1003 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureTopCyclotomicRestriction_padicDegree
Documentation

Restricting first to the top cyclotomic compositum gives the same p-adic degree as restricting directly from the common separable closure to the rational cyclotomic field.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem
    finitePlaceSeparableClosureTopCyclotomicRestriction_padicDegree
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    letI : IsScalarTower L
        (numberFieldCyclotomicZHatCompositum L)
        (SeparableClosure ℚ) :=
      numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
    (finitePlaceSeparableClosurePadicCyclotomicDegree
        (K := K) (L := L) v p).comp
        (finitePlaceSeparableClosureTopDecompositionInclusion
          (K := K) (L := L) v) =
      (numberFieldCyclotomicPadicDecompositionCoordinate L
        (finitePlaceCyclotomicCompositumExtension
          (K := K) (L := L) v).1 p).toMonoidHom.comp
        (finitePlaceSeparableClosureTopCyclotomicRestriction
          (K := K) (L := L) v) := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let : IsScalarTower ℚ K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseScalarTower K L
  let : IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) :=
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
  let C :=
    numberFieldCyclotomicZHatCompositum L
  let T :=
    rationalCyclotomicZHatField
  let : Algebra T C :=
    rationalCyclotomicZHatCompositum_algebra L
  let : IsScalarTower ℚ T C :=
    rationalCyclotomicZHatCompositum_scalarTower L
  let : Normal ℚ T :=
    rationalCyclotomicZHatField_normal
  let : Normal L C :=
    IsGalois.to_normal
  apply MonoidHom.ext
  intro τ
  apply congrArg (rationalCyclotomicPadicCoordinate p)
  apply AlgEquiv.ext
  intro x
  let τK : SeparableClosure ℚ ≃ₐ[K] SeparableClosure ℚ :=
    RamificationTheory.HilbertRamification.ValuationSubring.restrictAutomorphismScalars
      (K := K) (M := L) τ.1
  let τQ : SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ :=
    τK.restrictScalars ℚ
  let τC : C ≃ₐ[L] C :=
    AlgEquiv.restrictNormalHom C τ.1
  change
    AlgEquiv.restrictNormalHom T τQ x =
      numberFieldCyclotomicZHatCompositumRestriction L τC x
  have hTC (z : T) :
      algebraMap C (SeparableClosure ℚ) (algebraMap T C z) =
        algebraMap T (SeparableClosure ℚ) z := by
    rfl
  have hC :
      algebraMap T C
          (numberFieldCyclotomicZHatCompositumRestriction L τC x) =
        τC (algebraMap T C x) := by
    change
      algebraMap T C
          ((AlgEquiv.restrictNormal
            (MulSemiringAction.toAlgEquiv ℚ C τC) T) x) =
        (MulSemiringAction.toAlgEquiv ℚ C τC)
          (algebraMap T C x)
    exact
      AlgEquiv.restrictNormal_commutes
        (MulSemiringAction.toAlgEquiv ℚ C τC) T x
  have hΩC :
      algebraMap C (SeparableClosure ℚ) (τC (algebraMap T C x)) =
        τ.1
          (algebraMap C (SeparableClosure ℚ)
            (algebraMap T C x)) := by
    exact
      AlgEquiv.restrictNormal_commutes τ.1 C
        (algebraMap T C x)
  apply (algebraMap T (SeparableClosure ℚ)).injective
  calc
    algebraMap T (SeparableClosure ℚ)
          (AlgEquiv.restrictNormalHom T τQ x) =
        τQ (algebraMap T (SeparableClosure ℚ) x) :=
      AlgEquiv.restrictNormal_commutes τQ T x
    _ = τ.1 (algebraMap T (SeparableClosure ℚ) x) := rfl
    _ = τ.1
          (algebraMap C (SeparableClosure ℚ)
            (algebraMap T C x)) :=
      congrArg τ.1 (hTC x).symm
    _ = algebraMap C (SeparableClosure ℚ)
          (τC (algebraMap T C x)) := hΩC.symm
    _ = algebraMap C (SeparableClosure ℚ)
          (algebraMap T C
            (numberFieldCyclotomicZHatCompositumRestriction L τC x)) :=
      congrArg (algebraMap C (SeparableClosure ℚ)) hC.symm
    _ = algebraMap T (SeparableClosure ℚ)
          (numberFieldCyclotomicZHatCompositumRestriction L τC x) :=
      hTC _
theorem

finitePlaceSeparableClosureTop_padicDegree_range

L1117 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureTop_padicDegree_range
Documentation

The p-adic degrees contributed by the top-field decomposition group are exactly those visible in the actual cyclotomic compositum at the restricted place.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem
    finitePlaceSeparableClosureTop_padicDegree_range
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    letI : IsScalarTower L
        (numberFieldCyclotomicZHatCompositum L)
        (SeparableClosure ℚ) :=
      numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
    ((finitePlaceSeparableClosurePadicCyclotomicDegree
        (K := K) (L := L) v p).comp
        (finitePlaceSeparableClosureTopDecompositionInclusion
          (K := K) (L := L) v)).range =
      (numberFieldCyclotomicPadicDecompositionCoordinate L
        (finitePlaceCyclotomicCompositumExtension
          (K := K) (L := L) v).1 p).toMonoidHom.range := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let : IsScalarTower ℚ K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseScalarTower K L
  let : IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) :=
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
  rw [
    finitePlaceSeparableClosureTopCyclotomicRestriction_padicDegree
      (K := K) (L := L) v p]
  apply le_antisymm
  · rintro y ⟨τ, rfl⟩
    exact
      ⟨finitePlaceSeparableClosureTopCyclotomicRestriction
          (K := K) (L := L) v τ,
        rfl⟩
  · rintro y ⟨σ, rfl⟩
    obtain ⟨τ, hτ⟩ :=
      finitePlaceSeparableClosureTopCyclotomicRestriction_surjective
        (K := K) (L := L) v σ
    refine ⟨τ, ?_⟩
    exact congrArg
      (numberFieldCyclotomicPadicDecompositionCoordinate L
        (finitePlaceCyclotomicCompositumExtension
          (K := K) (L := L) v).1 p)
      hτ
theorem

finitePlaceSeparableClosureRestrictionKernel_padicDegree_range

L1176 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureRestrictionKernel_padicDegree_range
Documentation

The p-adic degrees contributed by the kernel of finite-place restriction are exactly the degrees coming from the decomposition group over the top field.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem
    finitePlaceSeparableClosureRestrictionKernel_padicDegree_range
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    letI : IsScalarTower L
        (numberFieldCyclotomicZHatCompositum L)
        (SeparableClosure ℚ) :=
      numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
    let restriction :=
      finitePlaceSeparableClosureDecompositionRestriction
        (K := K) (L := L) v
    let inclusion :=
      finitePlaceSeparableClosureTopDecompositionInclusion
        (K := K) (L := L) v
    let degree :=
      finitePlaceSeparableClosurePadicCyclotomicDegree
        (K := K) (L := L) v p
    (restriction.ker.map degree).toAddSubgroup' =
      (degree.comp inclusion).range.toAddSubgroup' := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let : IsScalarTower ℚ K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseScalarTower K L
  let : IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) :=
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
  dsimp only
  let restriction :=
    finitePlaceSeparableClosureDecompositionRestriction
      (K := K) (L := L) v
  let inclusion :=
    finitePlaceSeparableClosureTopDecompositionInclusion
      (K := K) (L := L) v
  let degree :=
    finitePlaceSeparableClosurePadicCyclotomicDegree
      (K := K) (L := L) v p
  rw [
    ←
      finitePlaceSeparableClosureTopDecompositionInclusion_range
        (K := K) (L := L) v,
    MonoidHom.range_comp]
theorem

finitePlaceSeparableClosureRestrictionKernel_padicDegree_isClosed

L1235 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureRestrictionKernel_padicDegree_isClosed
Documentation

The p-adic cyclotomic degrees contributed by the genuine kernel of finite-place restriction form a closed additive subgroup of ℤ_p.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem
    finitePlaceSeparableClosureRestrictionKernel_padicDegree_isClosed
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    letI : IsScalarTower L
        (numberFieldCyclotomicZHatCompositum L)
        (SeparableClosure ℚ) :=
      numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
    let restriction :=
      finitePlaceSeparableClosureDecompositionRestriction
        (K := K) (L := L) v
    let degree :=
      finitePlaceSeparableClosurePadicCyclotomicDegree
        (K := K) (L := L) v p
    IsClosed
      ((((restriction.ker.map degree).toAddSubgroup' :
          AddSubgroup ℤ_[p.1]) :
        Set ℤ_[p.1])) := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let : IsScalarTower ℚ K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseScalarTower K L
  let : IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) :=
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
  dsimp only
  rw [
    finitePlaceSeparableClosureRestrictionKernel_padicDegree_range
      (K := K) (L := L) v p,
    finitePlaceSeparableClosureTop_padicDegree_range
      (K := K) (L := L) v p]
  change
    IsClosed
      ((fun z : ℤ_[p.1] => Multiplicative.ofAdd z) ⁻¹'
        ((numberFieldCyclotomicPadicDecompositionCoordinate L
          (finitePlaceCyclotomicCompositumExtension
            (K := K) (L := L) v).1 p).range :
          Set (Multiplicative ℤ_[p.1])))
  exact
    (numberFieldCyclotomicPadicDecompositionCoordinate_range_isClosed
      L
      (finitePlaceCyclotomicCompositumExtension
        (K := K) (L := L) v).1 p).preimage
      continuous_ofAdd
theorem

finitePlaceSeparableClosureRestrictionKernel_padicDegree_isOpen

L1301 ↗
GlobalClassFieldTheory.Reciprocity.finitePlaceSeparableClosureRestrictionKernel_padicDegree_isOpen
Documentation

The p-adic cyclotomic degrees contributed by the genuine kernel of finite-place restriction form an open subgroup of ℤ_p.

The point is that the valuation on the actual cyclotomic compositum need only represent the normalized finite-place class. The finite-index theorem for that valuation class and closedness of the kernel image give openness.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem
    finitePlaceSeparableClosureRestrictionKernel_padicDegree_isOpen
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    letI : IsScalarTower L
        (numberFieldCyclotomicZHatCompositum L)
        (SeparableClosure ℚ) :=
      numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
    let restriction :=
      finitePlaceSeparableClosureDecompositionRestriction
        (K := K) (L := L) v
    let degree :=
      finitePlaceSeparableClosurePadicCyclotomicDegree
        (K := K) (L := L) v p
    IsOpen
      ((((restriction.ker.map degree).toAddSubgroup' :
          AddSubgroup ℤ_[p.1]) :
        Set ℤ_[p.1])) := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let : IsScalarTower ℚ K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseScalarTower K L
  let : IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) :=
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
  dsimp only
  have hclosed :=
    finitePlaceSeparableClosureRestrictionKernel_padicDegree_isClosed
      (K := K) (L := L) v p
  dsimp only at hclosed
  rw [
    finitePlaceSeparableClosureRestrictionKernel_padicDegree_range
      (K := K) (L := L) v p,
    finitePlaceSeparableClosureTop_padicDegree_range
      (K := K) (L := L) v p] at hclosed ⊢
  let H : AddSubgroup ℤ_[p.1] :=
    (numberFieldCyclotomicPadicDecompositionCoordinate L
      (finitePlaceCyclotomicCompositumExtension
        (K := K) (L := L) v).1 p).range.toAddSubgroup'
  change IsClosed (H : Set ℤ_[p.1]) at hclosed
  have hindex : H.index ≠ 0 := by
    exact
      numberFieldCyclotomicPadicDecompositionCoordinate_range_index_ne_zero_of_base_isEquiv
        L
        (finitePlaceExtensionCentre
          (K := K) (L := L) v
          (chosenFinitePlaceExtension (L := L) v))
        (finitePlaceCyclotomicCompositumExtension
          (K := K) (L := L) v).1
        (finitePlaceCyclotomicCompositumExtension_base_isEquiv
          (K := K) (L := L) v)
        p
  let finiteIndexH : H.FiniteIndex := ⟨hindex⟩
  exact AddSubgroup.isOpen_of_isClosed_of_finiteIndex H hclosed
theorem

exists_positivePadicDegree_lift_of_surjective

L1376 ↗
GlobalClassFieldTheory.Reciprocity.exists_positivePadicDegree_lift_of_surjective
Documentation

A surjective restriction map admits a lift with positive integral p-adic degree whenever the degrees contributed by its kernel form an open subgroup of ℤ_[p].

The initial lift is corrected inside the genuine restriction kernel. Density of the positive natural numbers in ℤ_[p] supplies the required correction without changing its prescribed restriction.

Source context 11 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
Lean source · statement
theorem exists_positivePadicDegree_lift_of_surjective
    {D A : Type} [Group D] [Group A]
    (p : ℕ) [Fact p.Prime]
    (restriction : D →* A)
    (hrestriction : Function.Surjective restriction)
    (degree : D →* Multiplicative ℤ_[p])
    (hdegree :
      IsOpen
        ((((restriction.ker.map degree).toAddSubgroup' :
            AddSubgroup ℤ_[p]) :
          Set ℤ_[p])))
    (σ : A) :
    ∃ τ : D,
      restriction τ = σ ∧
        ∃ n : ℕ, 0 < n ∧
          degree τ =
            (Multiplicative.ofAdd (1 : ℤ_[p])) ^ n
theorem

exists_finitePlaceSeparableClosureLift_with_positivePadicCyclotomicDegree

L1437 ↗
GlobalClassFieldTheory.Reciprocity.exists_finitePlaceSeparableClosureLift_with_positivePadicCyclotomicDegree
Documentation

Every actual finite-place decomposition automorphism has a lift to the compatible separable closure whose genuine cyclotomic p-adic degree is a positive integer.

The lift is corrected only inside the decomposition group over L, so its prescribed restriction to L is unchanged.

Source context 12 commands

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

open scoped NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
noncomputable local instance automorphismCyclicFixedFieldNumberField
    (σ : Gal(L/K)) :
    NumberField (automorphismCyclicFixedField σ) :=
  NumberField.of_module_finite K
    (automorphismCyclicFixedField σ)
omit [FiniteDimensional K L] in
Lean source · full declaration
theorem
    exists_finitePlaceSeparableClosureLift_with_positivePadicCyclotomicDegree
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (σ :
      absoluteValueDecompositionGroup K
        (chosenFinitePlaceExtension (L := L) v).1) :
    letI : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    letI : IsScalarTower ℚ K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseScalarTower K L
    letI : IsScalarTower L
        (numberFieldCyclotomicZHatCompositum L)
        (SeparableClosure ℚ) :=
      numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
    let wΩ :=
      numberFieldTowerFinitePlaceExtensionToSeparableClosure
        K L v (chosenFinitePlaceExtension (L := L) v)
    ∃ τ : absoluteValueDecompositionGroup K wΩ.1,
      finitePlaceSeparableClosureDecompositionRestriction
          (K := K) (L := L) v τ =
        σ ∧
      ∃ n : ℕ, 0 < n ∧
        finitePlaceSeparableClosurePadicCyclotomicDegree
            (K := K) (L := L) v p τ =
          (Multiplicative.ofAdd (1 : ℤ_[p.1])) ^ n := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  let : Algebra L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureTopAlgebra L
  let : IsScalarTower K L (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureScalarTower K L
  let : IsScalarTower ℚ K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseScalarTower K L
  let : IsScalarTower L
      (numberFieldCyclotomicZHatCompositum L)
      (SeparableClosure ℚ) :=
    numberFieldCyclotomicZHatCompositumSeparableClosureScalarTower L
  dsimp only
  exact
    exists_positivePadicDegree_lift_of_surjective
      p
      (finitePlaceSeparableClosureDecompositionRestriction
        (K := K) (L := L) v)
      (finitePlaceSeparableClosureDecompositionRestriction_surjective
        (K := K) (L := L) v)
      (finitePlaceSeparableClosurePadicCyclotomicDegree
        (K := K) (L := L) v p)
      (finitePlaceSeparableClosureRestrictionKernel_padicDegree_isOpen
        (K := K) (L := L) v p)
      σ

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