Module

FinitePadicAuxiliaryField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.LocalGlobalArtinCompatibility.FinitePadicAuxiliaryField

41 declarations indexed from sourceView source ↗

Module documentation

The finite p-adic auxiliary field

This module realizes the simultaneous finite/cyclotomic lift as an actual number field and proves the subgroup and intermediate-field identities needed by the auxiliary-field argument.

Imports4

Imported by4

instance

(anonymous instance)

L43 ↗

Source context 12 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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

instance

finitePadicAuxiliaryExtensionNormal

L49 ↗

GlobalClassFieldTheory.Reciprocity.finitePadicAuxiliaryExtensionNormal

Source context 14 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra

Lean source · statement

instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal

instance

finitePadicAuxiliaryExtensionQuotientFinite

L56 ↗

GlobalClassFieldTheory.Reciprocity.finitePadicAuxiliaryExtensionQuotientFinite

Source context 15 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L

Lean source · statement

instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L))

instance

finitePadicAuxiliaryExtensionQuotientIsMulCommutative

L65 ↗

GlobalClassFieldTheory.Reciprocity.finitePadicAuxiliaryExtensionQuotientIsMulCommutative

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L

Lean source · statement

instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L))

def

numberFieldTowerFinitePadicCyclicFixedField

L92 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedField

Documentation

The concrete auxiliary fixed field attached to a simultaneous finite/cyclotomic lift.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

def numberFieldTowerFinitePadicCyclicFixedField
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    IntermediateField ℚ (SeparableClosure ℚ)

theorem

numberFieldTowerFinitePadicCyclicFixedField_finiteDimensional

L103 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedField_finiteDimensional

Documentation

A nonzero-degree lift produces a genuine number field: its concrete fixed field is finite over ℚ.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem numberFieldTowerFinitePadicCyclicFixedField_finiteDimensional
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hτ :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠
        1) :
    FiniteDimensional ℚ
      (numberFieldTowerFinitePadicCyclicFixedField
        (K := K) (L := L) p τ)

theorem

numberFieldTowerBaseField_le_finitePadicCyclicFixedField

L131 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseField_le_finitePadicCyclicFixedField

Documentation

The compatible embedded copy of K lies in every auxiliary cyclic fixed field.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem numberFieldTowerBaseField_le_finitePadicCyclicFixedField
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    numberFieldTowerBaseField K L ≤
      numberFieldTowerFinitePadicCyclicFixedField
        (K := K) (L := L) p τ

def

numberFieldTowerFinitePadicAuxiliaryBaseEmbedding

L154 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryBaseEmbedding

Documentation

The compatible embedding of the original base field into the genuine auxiliary fixed field.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

def numberFieldTowerFinitePadicAuxiliaryBaseEmbedding
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    K →ₐ[ℚ]
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ)

theorem

numberFieldTowerFinitePadicAuxiliaryBaseEmbedding_coe

L176 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryBaseEmbedding_coe

Documentation

Coercing the auxiliary base embedding recovers the fixed lower embedding into the rational separable closure.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem numberFieldTowerFinitePadicAuxiliaryBaseEmbedding_coe
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (x : K) :
    ((numberFieldTowerFinitePadicAuxiliaryBaseEmbedding
        (K := K) (L := L) p τ x :
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ)) :
      SeparableClosure ℚ) =
        numberFieldTowerLowerEmbedding K L x

theorem

numberFieldTowerTopField_mem_finitePadicAuxiliaryTopField

L192 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerTopField_mem_finitePadicAuxiliaryTopField

Documentation

The compatible copy of the original top field lies in the auxiliary compositum fixed field.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem numberFieldTowerTopField_mem_finitePadicAuxiliaryTopField
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    {x : SeparableClosure ℚ}
    (hx : x ∈ numberFieldInRationalSeparableClosure L) :
    x ∈
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below

def

numberFieldTowerFinitePadicAuxiliaryTopEmbedding

L224 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryTopEmbedding

Documentation

The compatible embedding of the original top field into the auxiliary compositum fixed field.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

def numberFieldTowerFinitePadicAuxiliaryTopEmbedding
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    L →ₐ[ℚ]
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below

theorem

numberFieldTowerFinitePadicAuxiliaryTopEmbedding_coe

L247 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryTopEmbedding_coe

Documentation

Coercing the auxiliary top embedding recovers the chosen top-field embedding into the rational separable closure.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem numberFieldTowerFinitePadicAuxiliaryTopEmbedding_coe
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (x : L) :
    ((numberFieldTowerFinitePadicAuxiliaryTopEmbedding
        (K := K) (L := L) p τ x :
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below) :
      SeparableClosure ℚ) =
        numberFieldSeparableClosureEmbedding L x

theorem

numberFieldTowerFinitePadicAuxiliaryEmbedding_algebraMap

L263 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryEmbedding_algebraMap

Documentation

The compatible base and top embeddings form the actual base-change square inside the rational separable closure.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem numberFieldTowerFinitePadicAuxiliaryEmbedding_algebraMap
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (x : K) :
    ((numberFieldTowerFinitePadicAuxiliaryTopEmbedding
        (K := K) (L := L) p τ (algebraMap K L x) :
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below) :
      SeparableClosure ℚ) =
    ((numberFieldTowerFinitePadicAuxiliaryBaseEmbedding
        (K := K) (L := L) p τ x :
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ)) :
      SeparableClosure ℚ)

instance

numberFieldTowerFinitePadicAuxiliary_baseAlgebra

L283 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliary_baseAlgebra

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

instance
    numberFieldTowerFinitePadicAuxiliary_baseAlgebra
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    Algebra K
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ))

instance

numberFieldTowerFinitePadicAuxiliary_baseRatScalarTower

L296 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliary_baseRatScalarTower

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

instance
    numberFieldTowerFinitePadicAuxiliary_baseRatScalarTower
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    IsScalarTower ℚ K
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ))

instance

numberFieldTowerFinitePadicAuxiliary_topAlgebra

L310 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliary_topAlgebra

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

instance
    numberFieldTowerFinitePadicAuxiliary_topAlgebra
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    Algebra L
      (LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below)

instance

numberFieldTowerFinitePadicAuxiliary_topRatScalarTower

L323 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliary_topRatScalarTower

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

instance
    numberFieldTowerFinitePadicAuxiliary_topRatScalarTower
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    IsScalarTower ℚ L
      (LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below)

instance

numberFieldTowerFinitePadicAuxiliary_originalBaseTopAlgebra

L337 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliary_originalBaseTopAlgebra

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

instance
    numberFieldTowerFinitePadicAuxiliary_originalBaseTopAlgebra
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    Algebra K
      (LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below)

instance

numberFieldTowerFinitePadicAuxiliary_originalTopScalarTower

L351 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliary_originalTopScalarTower

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

instance
    numberFieldTowerFinitePadicAuxiliary_originalTopScalarTower
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    IsScalarTower K L
      (LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below)

instance

numberFieldTowerFinitePadicAuxiliary_baseTopScalarTower

L362 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliary_baseTopScalarTower

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

instance
    numberFieldTowerFinitePadicAuxiliary_baseTopScalarTower
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    IsScalarTower K
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ))
      (LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below)

theorem

numberFieldTowerFinitePadicAuxiliaryBase_isGalois

L385 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryBase_isGalois

Documentation

The genuine auxiliary fixed field is Galois over the original base field through the compatible embedding above.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem numberFieldTowerFinitePadicAuxiliaryBase_isGalois
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    IsGalois K
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ))

def

numberFieldTowerFinitePadicAuxiliarySubgroupLift

L439 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliarySubgroupLift

Documentation

The distinguished absolute lift, regarded as an element of the auxiliary base subgroup.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

def numberFieldTowerFinitePadicAuxiliarySubgroupLift
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    (numberFieldTowerFinitePadicCyclicFixedSubgroup
      (K := K) (L := L) p τ).toSubgroup

def

numberFieldTowerFinitePadicAuxiliaryAutomorphism

L450 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryAutomorphism

Documentation

The actual automorphism of the auxiliary compositum induced by the distinguished simultaneous finite/cyclotomic lift.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · full declaration

def numberFieldTowerFinitePadicAuxiliaryAutomorphism
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    let P :=
      numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
        (K := K) (L := L) p τ
    let S :=
      numberFieldTowerFinitePadicCyclicFixedSubgroup
        (K := K) (L := L) p τ
    Gal(
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below /
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) S) := by
  dsimp only
  let P :=
    numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
      (K := K) (L := L) p τ
  let S :=
    numberFieldTowerFinitePadicCyclicFixedSubgroup
      (K := K) (L := L) p τ
  let σS :=
    numberFieldTowerFinitePadicAuxiliarySubgroupLift
      (K := K) (L := L) p τ
  exact
    LocalClassFieldTheory.abstractExtensionQuotientEquivGaloisGroup
      ℚ (SeparableClosure ℚ)
      S P.field P.below
      P.toFiniteGaloisExtension.normal
      (QuotientGroup.mk'
        (extensionSubgroup
          S P.field P.below)
        σS)

theorem

numberFieldTowerFinitePadicAuxiliaryAutomorphism_apply_val

L486 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryAutomorphism_apply_val

Documentation

On the common separable closure, the auxiliary automorphism acts by the original distinguished ambient lift.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem numberFieldTowerFinitePadicAuxiliaryAutomorphism_apply_val
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (x :
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below) :
    ((numberFieldTowerFinitePadicAuxiliaryAutomorphism
        (K := K) (L := L) p τ x :
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below) :
      SeparableClosure ℚ) =
        τ.1 (x : SeparableClosure ℚ)

theorem

numberFieldTowerFinitePadicAuxiliaryAutomorphism_restriction

L520 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryAutomorphism_restriction

Documentation

Restricting the auxiliary automorphism through the actual base-change square recovers the finite quotient coordinate of the distinguished lift.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem numberFieldTowerFinitePadicAuxiliaryAutomorphism_restriction
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K))
        (numberFieldTowerFinitePadicAuxiliaryAutomorphism
          (K := K) (L := L) p τ) =
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
        (numberFieldTowerFiniteQuotientCoordinate
          (K := K) (L := L) τ)

def

numberFieldTowerFinitePadicAuxiliaryBasePlaceExtension

L567 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryBasePlaceExtension

Documentation

Restriction of the chosen separable-closure place to the genuine auxiliary base field. This is an exact extension of the original finite place of K, not merely an equivalent valuation.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

def
    numberFieldTowerFinitePadicAuxiliaryBasePlaceExtension
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ))

def

numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension

L597 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension

Documentation

Restriction of the same separable-closure place to the genuine auxiliary compositum. Its restriction to K agrees exactly with the original normalized finite absolute value.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

def
    numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv K v)
      (LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ)
        (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
          (K := K) (L := L) p τ).below)

theorem

numberFieldTowerFinitePadicAuxiliaryTopPlace_below

L626 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryTopPlace_below

Documentation

The centre of the restricted place on the auxiliary compositum lies above the centre of the same place on the auxiliary base field.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · full declaration

theorem
    numberFieldTowerFinitePadicAuxiliaryTopPlace_below
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hτ :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠
        1) :
    let S :=
      numberFieldTowerFinitePadicCyclicFixedSubgroup
        (K := K) (L := L) p τ
    let P :=
      numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
        (K := K) (L := L) p τ
    let F :=
      LocalClassFieldTheory.abstractFixedField
        ℚ (SeparableClosure ℚ) S
    let E :=
      LocalClassFieldTheory.abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) P.below
    letI hHfinite : Finite
        ((baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
          extensionSubgroup
            (baseField
              (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
            S (le_baseField S)) :=
      (numberFieldTowerFinitePadicAuxiliaryAbstractField
        (K := K) (L := L) p τ hτ).finite
    letI hPfinite : Finite
        (S.toSubgroup ⧸
          extensionSubgroup S P.field P.below) :=
      P.finite
    letI _ : FiniteDimensional ℚ F :=
      LocalClassFieldTheory.abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) S hHfinite
    letI _ : FiniteDimensional F E :=
      LocalClassFieldTheory.abstractRelativeFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ)
        S P.field P.below hHfinite hPfinite
    letI _ : IsScalarTower ℚ F E :=
      IsScalarTower.of_algebraMap_eq' rfl
    letI _ : FiniteDimensional ℚ E :=
      FiniteDimensional.trans ℚ F E
    letI _ : NumberField F :=
      NumberField.of_module_finite ℚ F
    letI _ : NumberField E :=
      NumberField.of_module_finite ℚ E
    letI _ : Algebra K F :=
      numberFieldTowerFinitePadicAuxiliary_baseAlgebra
        (K := K) (L := L) p τ
    finitePlaceBelow (K := F)
        (finitePlaceExtensionCentre
          (K := K) (L := E) v
          (numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension
            (K := K) (L := L) v p τ)) =
      finitePlaceExtensionCentre
        (K := K) (L := F) v
        (numberFieldTowerFinitePadicAuxiliaryBasePlaceExtension
          (K := K) (L := L) v p τ) := by
  dsimp only
  let S :=
    numberFieldTowerFinitePadicCyclicFixedSubgroup
      (K := K) (L := L) p τ
  let P :=
    numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
      (K := K) (L := L) p τ
  let F :=
    LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) S
  let E :=
    LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below
  let hHfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          S (le_baseField S)) :=
    (numberFieldTowerFinitePadicAuxiliaryAbstractField
      (K := K) (L := L) p τ hτ).finite
  let hPfinite : Finite
      (S.toSubgroup ⧸
        extensionSubgroup S P.field P.below) :=
    P.finite
  let auxiliaryBaseFiniteDimensional : FiniteDimensional ℚ F :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) S hHfinite
  let auxiliaryTopFiniteDimensional : FiniteDimensional F E :=
    LocalClassFieldTheory.abstractRelativeFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ)
      S P.field P.below hHfinite hPfinite
  let auxiliaryScalarTower : IsScalarTower ℚ F E :=
    IsScalarTower.of_algebraMap_eq' rfl
  let auxiliaryAbsoluteFiniteDimensional : FiniteDimensional ℚ E :=
    FiniteDimensional.trans ℚ F E
  let auxiliaryBaseNumberField : NumberField F :=
    NumberField.of_module_finite ℚ F
  let auxiliaryTopNumberField : NumberField E :=
    NumberField.of_module_finite ℚ E
  let auxiliaryOriginalBaseAlgebra : Algebra K F :=
    numberFieldTowerFinitePadicAuxiliary_baseAlgebra
      (K := K) (L := L) p τ
  let wF :=
    numberFieldTowerFinitePadicAuxiliaryBasePlaceExtension
      (K := K) (L := L) v p τ
  let wE :=
    numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension
      (K := K) (L := L) v p τ
  apply HeightOneSpectrum.ext
  ext x
  change
    algebraMap (𝓞 F) (𝓞 E) x ∈
        finitePlaceExtensionCentreIdeal
          (K := K) (L := E) v wE ↔
      x ∈
        finitePlaceExtensionCentreIdeal
          (K := K) (L := F) v wF
  rw [
    mem_finitePlaceExtensionCentreIdeal_iff,
    mem_finitePlaceExtensionCentreIdeal_iff]
  rfl

opaque

numberFieldTowerFinitePadicAuxiliaryTopPlace_automorphism_apply

L754 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryTopPlace_automorphism_apply

Documentation

Evaluation of the distinguished auxiliary automorphism through the restricted top-field place. Isolating this coercion calculation prevents the whole decomposition-group proof from normalizing the fixed-field tower.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · full declaration

opaque
    numberFieldTowerFinitePadicAuxiliaryTopPlace_automorphism_apply
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    let P := numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
      (K := K) (L := L) p τ
    let E := LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below
    let wE := numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension
      (K := K) (L := L) v p τ
    let σE := numberFieldTowerFinitePadicAuxiliaryAutomorphism
      (K := K) (L := L) p τ
    ∀ x : E,
      wE.1 (σE x) =
        (numberFieldTowerFinitePlaceExtensionToSeparableClosure
          K L v (chosenFinitePlaceExtension (L := L) v)).1
            (τ.1 (x : SeparableClosure ℚ)) := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  dsimp only
  intro x
  change
    (numberFieldTowerFinitePlaceExtensionToSeparableClosure
      K L v (chosenFinitePlaceExtension (L := L) v)).1
        ((numberFieldTowerFinitePadicAuxiliaryAutomorphism
          (K := K) (L := L) p τ x :
            LocalClassFieldTheory.abstractRelativeFixedField
              ℚ (SeparableClosure ℚ)
              (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
                (K := K) (L := L) p τ).below) : SeparableClosure ℚ) = _
  rw [
    numberFieldTowerFinitePadicAuxiliaryAutomorphism_apply_val
      (K := K) (L := L) p τ]

opaque

numberFieldTowerFinitePadicAuxiliaryAutomorphism_mem_topPlaceDecomposition

L791 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryAutomorphism_mem_topPlaceDecomposition

Documentation

The distinguished auxiliary automorphism preserves the top-field place obtained by restricting the original separable-closure place.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · full declaration

opaque numberFieldTowerFinitePadicAuxiliaryAutomorphism_mem_topPlaceDecomposition
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hdecomposition :
      letI : Algebra K (SeparableClosure ℚ) :=
        numberFieldTowerSeparableClosureBaseAlgebra K L
      (numberFieldTowerSeparableClosureEquivBaseSubgroup K L).symm τ ∈
        absoluteValueDecompositionGroup K
          (numberFieldTowerFinitePlaceExtensionToSeparableClosure
            K L v (chosenFinitePlaceExtension (L := L) v)).1) :
    let S := numberFieldTowerFinitePadicCyclicFixedSubgroup
      (K := K) (L := L) p τ
    let F := LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) S
    let wE := numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension
      (K := K) (L := L) v p τ
    let σE := numberFieldTowerFinitePadicAuxiliaryAutomorphism
      (K := K) (L := L) p τ
    σE ∈ absoluteValueDecompositionGroup F wE.1 := by
  let : Algebra K (SeparableClosure ℚ) :=
    numberFieldTowerSeparableClosureBaseAlgebra K L
  dsimp only at hdecomposition ⊢
  let S :=
    numberFieldTowerFinitePadicCyclicFixedSubgroup
      (K := K) (L := L) p τ
  let F :=
    LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) S
  let wE :=
    numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension
      (K := K) (L := L) v p τ
  let σE :=
    numberFieldTowerFinitePadicAuxiliaryAutomorphism
      (K := K) (L := L) p τ
  intro x
  change
    wE.1 (σE x) < 1 ↔
      wE.1 x < 1
  rw [
    numberFieldTowerFinitePadicAuxiliaryTopPlace_automorphism_apply
      (K := K) (L := L) v p τ x,
    show
      wE.1 x =
        (numberFieldTowerFinitePlaceExtensionToSeparableClosure
          K L v
          (chosenFinitePlaceExtension (L := L) v)).1
            (x : SeparableClosure ℚ) from rfl]
  exact hdecomposition (x : SeparableClosure ℚ)

opaque

numberFieldTowerFinitePadicAuxiliaryTopDecompositionGroup_eq_chosen

L843 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryTopDecompositionGroup_eq_chosen

Documentation

The restricted top-field place and the chosen extension above its centre have the same decomposition group.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · full declaration

opaque numberFieldTowerFinitePadicAuxiliaryTopDecompositionGroup_eq_chosen
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hτ :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠ 1) :
    let S := numberFieldTowerFinitePadicCyclicFixedSubgroup
      (K := K) (L := L) p τ
    let P := numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
      (K := K) (L := L) p τ
    let F := LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) S
    let E := LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below
    letI hHfinite : Finite
        ((baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
          extensionSubgroup
            (baseField
              (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
            S (le_baseField S)) :=
      (numberFieldTowerFinitePadicAuxiliaryAbstractField
        (K := K) (L := L) p τ hτ).finite
    letI hPfinite : Finite
        (S.toSubgroup ⧸ extensionSubgroup S P.field P.below) := P.finite
    letI : FiniteDimensional ℚ F :=
      LocalClassFieldTheory.abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) S hHfinite
    letI : FiniteDimensional F E :=
      LocalClassFieldTheory.abstractRelativeFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) S P.field P.below hHfinite hPfinite
    letI : IsScalarTower ℚ F E := IsScalarTower.of_algebraMap_eq' rfl
    letI : FiniteDimensional ℚ E := FiniteDimensional.trans ℚ F E
    letI : NumberField F := NumberField.of_module_finite ℚ F
    letI : NumberField E := NumberField.of_module_finite ℚ E
    letI : IsAbelianGalois F E :=
      GlobalClassFields.finiteAbelianSubextensionAbstractRelativeFixedFieldIsAbelianGalois P
    letI : Algebra K F :=
      numberFieldTowerFinitePadicAuxiliary_baseAlgebra
        (K := K) (L := L) p τ
    let wF := numberFieldTowerFinitePadicAuxiliaryBasePlaceExtension
      (K := K) (L := L) v p τ
    let wE := numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension
      (K := K) (L := L) v p τ
    let V := finitePlaceExtensionCentre (K := K) (L := F) v wF
    absoluteValueDecompositionGroup F wE.1 =
      absoluteValueDecompositionGroup F
        (chosenFinitePlaceExtension (L := E) V).1 := by
  dsimp only
  let H :=
    numberFieldTowerFinitePadicAuxiliaryAbstractField
      (K := K) (L := L) p τ hτ
  let S :=
    numberFieldTowerFinitePadicCyclicFixedSubgroup
      (K := K) (L := L) p τ
  let P :=
    numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
      (K := K) (L := L) p τ
  let F :=
    LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) S
  let E :=
    LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below
  let hHfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          S (le_baseField S)) :=
    H.finite
  let hPfinite : Finite
      (S.toSubgroup ⧸ extensionSubgroup S P.field P.below) :=
    P.finite
  let : FiniteDimensional ℚ F :=
    LocalClassFieldTheory.abstractFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) S hHfinite
  let : FiniteDimensional F E :=
    LocalClassFieldTheory.abstractRelativeFixedField_finiteDimensional
      ℚ (SeparableClosure ℚ) S P.field P.below hHfinite hPfinite
  let : IsScalarTower ℚ F E := IsScalarTower.of_algebraMap_eq' rfl
  let : FiniteDimensional ℚ E := FiniteDimensional.trans ℚ F E
  let : NumberField F := NumberField.of_module_finite ℚ F
  let : NumberField E := NumberField.of_module_finite ℚ E
  let : IsAbelianGalois F E :=
    GlobalClassFields.finiteAbelianSubextensionAbstractRelativeFixedFieldIsAbelianGalois P
  let : Algebra K F :=
    numberFieldTowerFinitePadicAuxiliary_baseAlgebra
      (K := K) (L := L) p τ
  let wF :=
    numberFieldTowerFinitePadicAuxiliaryBasePlaceExtension
      (K := K) (L := L) v p τ
  let wE :=
    numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension
      (K := K) (L := L) v p τ
  let V := finitePlaceExtensionCentre (K := K) (L := F) v wF
  let W := finitePlaceExtensionCentre (K := K) (L := E) v wE
  let Wover :
      {W' : HeightOneSpectrum (𝓞 E) //
        finitePlaceBelow (K := F) W' = V} :=
    ⟨W,
      numberFieldTowerFinitePadicAuxiliaryTopPlace_below
        (K := K) (L := L) v p τ hτ⟩
  let wFE :
      AbsoluteValueExtension
        (NumberField.HeightOneSpectrum.adicAbv F V) E :=
    (finitePlaceExtensionEquivAbove
      (K := F) (L := E) V).symm Wover
  have hwFEcentre :
      finitePlaceExtensionCentre
          (K := F) (L := E) V wFE =
        W := by
    exact
      congrArg Subtype.val
        ((finitePlaceExtensionEquivAbove
          (K := F) (L := E) V).apply_symm_apply Wover)
  have hwEquiv : wE.1.IsEquiv wFE.1 := by
    apply
      finitePlaceExtensions_isEquiv_of_centres_eq
        (F := K) (M := F) v V wE wFE
    exact hwFEcentre.symm
  calc
    absoluteValueDecompositionGroup F wE.1 =
        absoluteValueDecompositionGroup F wFE.1 :=
      absoluteValueDecompositionGroup_eq_of_absoluteValue_isEquiv
        (F := F) wE.1 wFE.1 hwEquiv
    _ =
      absoluteValueDecompositionGroup F
          (chosenFinitePlaceExtension (L := E) V).1 :=
      absoluteValueDecompositionGroup_eq_of_exactExtensions_of_isMulCommutative
        (F := F)
        (NumberField.HeightOneSpectrum.adicAbv F V)
        (RayClass.adicAbv_isNontrivial V)
        wFE
        (chosenFinitePlaceExtension (L := E) V)

theorem

globalNormResidueMonoidHomOfEmbedding_norm_restriction_apply

L985 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueMonoidHomOfEmbedding_norm_restriction_apply

Documentation

Pointwise form of norm/restriction naturality. Keeping the function equality and its coercion normalization in this small declaration prevents the auxiliary-field witness construction below from repeatedly elaborating the full pair of composite homomorphisms.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem globalNormResidueMonoidHomOfEmbedding_norm_restriction_apply
    (K K' L L' : Type)
    [Field K] [NumberField K]
    [Field K'] [NumberField K']
    [Field L] [NumberField L]
    [Field L'] [NumberField L']
    [Algebra K K'] [Algebra K L] [Algebra K L']
    [Algebra K' L'] [Algebra L L']
    [IsScalarTower K K' L'] [IsScalarTower K L L']
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [FiniteDimensional K' L'] [IsAbelianGalois K' L']
    [FiniteDimensional K K'] [IsGalois K K']
    (j : L' →ₐ[ℚ] SeparableClosure ℚ)
    (c : IdeleClassGroup K') :
    ((AlgEquiv.restrictNormalHom L).comp
        (AlgEquiv.restrictScalarsHom K))
          (globalNormResidueMonoidHomOfEmbedding K' L' j c) =
      globalNormResidueMonoidHomOfEmbedding K L
        (j.comp (IsScalarTower.toAlgHom ℚ L L'))
        (_root_.ideleClassNorm K K' c)

opaque

numberFieldTowerFinitePadicAuxiliaryLocalGlobalRepresentative

L1015 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryLocalGlobalRepresentative

Documentation

The auxiliary-field construction produces a lower local unit whose chosen local Artin value and global norm-residue value are both the finite quotient coordinate of the distinguished lift.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · full declaration

opaque numberFieldTowerFinitePadicAuxiliaryLocalGlobalRepresentative
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hτ :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠ 1)
    (hdecomposition :
      letI : Algebra K (SeparableClosure ℚ) :=
        numberFieldTowerSeparableClosureBaseAlgebra K L
      (numberFieldTowerSeparableClosureEquivBaseSubgroup K L).symm τ ∈
        absoluteValueDecompositionGroup K
          (numberFieldTowerFinitePlaceExtensionToSeparableClosure
            K L v (chosenFinitePlaceExtension (L := L) v)).1)
    (n : ℕ) (hn : 0 < n)
    (hdegree :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ =
        (Multiplicative.ofAdd (1 : ℤ_[p.1])) ^ n)
    (hprimaryQuotient :
      numberFieldTowerFiniteQuotientCoordinate
          (K := K) (L := L) τ ∈
        CommGroup.primaryComponent
          ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
            extensionSubgroup
              (numberFieldTowerBaseSubgroup K L)
              (numberFieldTowerTopSubgroup L)
              (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
          p.1) :
    {z : (v.adicCompletion K)ˣ //
      chosenFinitePlaceArtinMonoidHom (K := K) (L := L) v z =
          numberFieldTowerExtensionQuotientEquivGaloisGroup K L
            (numberFieldTowerFiniteQuotientCoordinate
              (K := K) (L := L) τ) ∧
      globalNormResidueMonoidHom K L
          (IdeleGroup.finitePlaceIdeleClass v z) =
          numberFieldTowerExtensionQuotientEquivGaloisGroup K L
            (numberFieldTowerFiniteQuotientCoordinate
              (K := K) (L := L) τ)} := by
  let H :=
    numberFieldTowerFinitePadicAuxiliaryAbstractField
      (K := K) (L := L) p τ hτ
  let S :=
    numberFieldTowerFinitePadicCyclicFixedSubgroup
      (K := K) (L := L) p τ
  let P :=
    numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
      (K := K) (L := L) p τ
  let F :=
    LocalClassFieldTheory.abstractFixedField
      ℚ (SeparableClosure ℚ) S
  let E :=
    LocalClassFieldTheory.abstractRelativeFixedField
      ℚ (SeparableClosure ℚ) P.below
  letI hHfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          S (le_baseField S)) :=
    H.finite
  letI hPfinite : Finite
      (S.toSubgroup ⧸ extensionSubgroup S P.field P.below) :=
    P.finite
  letI auxiliaryBaseNumberField : NumberField F := by
    let : FiniteDimensional ℚ F :=
      LocalClassFieldTheory.abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) S hHfinite
    exact NumberField.of_module_finite ℚ F
  letI auxiliaryTopNumberField : NumberField E := by
    let : FiniteDimensional F E :=
      LocalClassFieldTheory.abstractRelativeFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ)
        S P.field P.below hHfinite hPfinite
    exact NumberField.of_module_finite F E
  letI auxiliaryAbelianGalois : IsAbelianGalois F E :=
    GlobalClassFields.finiteAbelianSubextensionAbstractRelativeFixedFieldIsAbelianGalois P
  letI auxiliaryOriginalBaseAlgebra : Algebra K F :=
    numberFieldTowerFinitePadicAuxiliary_baseAlgebra
      (K := K) (L := L) p τ
  letI auxiliaryOriginalTopAlgebra : Algebra L E :=
    numberFieldTowerFinitePadicAuxiliary_topAlgebra
      (K := K) (L := L) p τ
  letI auxiliaryOriginalBaseTopAlgebra : Algebra K E :=
    numberFieldTowerFinitePadicAuxiliary_originalBaseTopAlgebra
      (K := K) (L := L) p τ
  letI auxiliaryOriginalTopScalarTower : IsScalarTower K L E :=
    numberFieldTowerFinitePadicAuxiliary_originalTopScalarTower
      (K := K) (L := L) p τ
  letI auxiliaryBaseTopScalarTower : IsScalarTower K F E :=
    numberFieldTowerFinitePadicAuxiliary_baseTopScalarTower
      (K := K) (L := L) p τ
  letI auxiliaryOriginalBaseGalois : IsGalois K F :=
    numberFieldTowerFinitePadicAuxiliaryBase_isGalois
      (K := K) (L := L) p τ
  let auxiliaryOriginalTopAlgHom : L →ₐ[ℚ] E :=
    numberFieldTowerFinitePadicAuxiliaryTopEmbedding
      (K := K) (L := L) p τ
  let wF :=
    numberFieldTowerFinitePadicAuxiliaryBasePlaceExtension
      (K := K) (L := L) v p τ
  let wE :=
    numberFieldTowerFinitePadicAuxiliaryTopPlaceExtension
      (K := K) (L := L) v p τ
  let V :=
    finitePlaceExtensionCentre
      (K := K) (L := F) v wF
  have hVbelow : finitePlaceBelow (K := K) V = v :=
    finitePlaceBelow_finitePlaceExtensionCentre
      (K := K) (L := F) v wF
  let Vover :
      {V' : HeightOneSpectrum (𝓞 F) //
        finitePlaceBelow (K := K) V' = v} :=
    ⟨V, hVbelow⟩
  letI auxiliaryCompletionAlgebra :
      Algebra (v.adicCompletion K) (V.adicCompletion F) :=
    (finitePlaceAdicCompletionMap K F v Vover).toAlgebra
  let σE : Gal(E / F) :=
    numberFieldTowerFinitePadicAuxiliaryAutomorphism
      (K := K) (L := L) p τ
  have hσtop :
      σE ∈ absoluteValueDecompositionGroup F wE.1 :=
    numberFieldTowerFinitePadicAuxiliaryAutomorphism_mem_topPlaceDecomposition
      (K := K) (L := L) v p τ hdecomposition
  have hgroup :=
    numberFieldTowerFinitePadicAuxiliaryTopDecompositionGroup_eq_chosen
      (K := K) (L := L) v p τ hτ
  have hσchosen :
      σE ∈ absoluteValueDecompositionGroup F
        (chosenFinitePlaceExtension (L := E) V).1 := by
    rw [← hgroup]
    exact hσtop
  have hRange :
      σE ∈ (chosenFinitePlaceArtinMonoidHom
        (K := F) (L := E) V).range := by
    rw [chosenFinitePlaceArtinMonoidHom_range (K := F) (L := E) V]
    exact hσchosen
  let y : (V.adicCompletion F)ˣ := Classical.choose hRange
  have hy :
      chosenFinitePlaceArtinMonoidHom (K := F) (L := E) V y =
        numberFieldTowerFinitePadicAuxiliaryAutomorphism
          (K := K) (L := L) p τ :=
    Classical.choose_spec hRange
  let z : (v.adicCompletion K)ˣ :=
    LocalFieldTheory.normUnits
      (v.adicCompletion K) (V.adicCompletion F) y
  have hz :
      z = LocalFieldTheory.normUnits
        (v.adicCompletion K) (V.adicCompletion F) y := by
    rfl
  let σK : Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
      (numberFieldTowerFiniteQuotientCoordinate
        (K := K) (L := L) τ)
  let restriction : Gal(E / F) →* Gal(L / K) :=
    (AlgEquiv.restrictNormalHom L).comp
      (AlgEquiv.restrictScalarsHom K)
  have hrestrict : restriction σE = σK :=
    numberFieldTowerFinitePadicAuxiliaryAutomorphism_restriction
      (K := K) (L := L) p τ
  have hlocal :
      chosenFinitePlaceArtinMonoidHom (K := K) (L := L) v z =
        σK := by
    rw [hz]
    have hnat :=
      DFunLike.congr_fun
        (chosenFinitePlaceArtinMonoidHom_norm_restriction_of_below_eq
          (K := K) (L := L) (K' := F) (L' := E)
          v V hVbelow) y
    calc
      chosenFinitePlaceArtinMonoidHom (K := K) (L := L) v
          (LocalFieldTheory.normUnits
            (v.adicCompletion K) (V.adicCompletion F) y) =
        restriction
          (chosenFinitePlaceArtinMonoidHom (K := F) (L := E) V y) := by
            simpa only [
              MonoidHom.coe_comp, Function.comp_apply, restriction]
              using hnat.symm
      _ = restriction σE := congrArg restriction hy
      _ = σK := hrestrict
  let j : E →ₐ[ℚ] SeparableClosure ℚ :=
    E.val.restrictScalars ℚ
  have hjLower :
      j.comp auxiliaryOriginalTopAlgHom =
        AlgebraicNumberTheory.numberFieldSeparableClosureEmbedding L := by
    apply AlgHom.ext
    intro a
    exact
      numberFieldTowerFinitePadicAuxiliaryTopEmbedding_coe
        (K := K) (L := L) p τ a
  have hPUnramified :
      P.toFiniteGaloisExtension.IsUnramified
        rationalCyclotomicDegreeData :=
    numberFieldTowerFinitePadicAuxiliaryCompositumSubextension_isUnramified
      (K := K) (L := L) p τ n hn hdegree hprimaryQuotient
  have hcompat :
      (globalNormResidueMonoidHomOfEmbedding F E j).comp
          (IdeleGroup.finitePlaceIdeleClass V) =
        chosenFinitePlaceArtinMonoidHom (K := F) (L := E) V :=
    globalNormResidueMonoidHomOfEmbedding_comp_finitePlaceIdeleClass_of_abstractFixedFieldUnramified
      H P hPUnramified V
  have hupper :
      globalNormResidueMonoidHomOfEmbedding F E j
          (IdeleGroup.finitePlaceIdeleClass V y) =
        σE :=
    (congrArg
      (fun φ : (V.adicCompletion F)ˣ →* Gal(E / F) => φ y)
      hcompat).trans hy
  have hnormClass :
      _root_.ideleClassNorm K F
          (IdeleGroup.finitePlaceIdeleClass V y) =
        IdeleGroup.finitePlaceIdeleClass v z := by
    rw [hz]
    simpa only [Vover] using
      (IdeleGroup.ideleClassNorm_finitePlaceIdeleClass_eq_normUnits
        (K := K) (L := F) v Vover y)
  have hglobal :
      globalNormResidueMonoidHom K L
          (IdeleGroup.finitePlaceIdeleClass v z) =
        σK := by
    calc
      globalNormResidueMonoidHom K L
          (IdeleGroup.finitePlaceIdeleClass v z) =
          globalNormResidueMonoidHom K L
            (_root_.ideleClassNorm K F
              (IdeleGroup.finitePlaceIdeleClass V y)) :=
        congrArg (globalNormResidueMonoidHom K L) hnormClass.symm
      _ = globalNormResidueMonoidHomOfEmbedding K L
          (j.comp auxiliaryOriginalTopAlgHom)
          (_root_.ideleClassNorm K F
            (IdeleGroup.finitePlaceIdeleClass V y)) := by
        rw [hjLower,
          ← globalNormResidueMonoidHom_eq_ofEmbedding_standard]
      _ = ((AlgEquiv.restrictNormalHom L).comp
          (AlgEquiv.restrictScalarsHom K))
          (globalNormResidueMonoidHomOfEmbedding F E j
            (IdeleGroup.finitePlaceIdeleClass V y)) := by
        apply Eq.symm
        apply
          globalNormResidueMonoidHomOfEmbedding_norm_restriction_apply
      _ = ((AlgEquiv.restrictNormalHom L).comp
          (AlgEquiv.restrictScalarsHom K)) σE :=
        congrArg
          ((AlgEquiv.restrictNormalHom L).comp
            (AlgEquiv.restrictScalarsHom K)) hupper
      _ = restriction σE := rfl
      _ = σK := hrestrict
  exact ⟨z, hlocal, hglobal⟩

theorem

exists_numberFieldTowerFinitePadicLift_of_finitePlace

L1269 ↗

GlobalClassFieldTheory.Reciprocity.exists_numberFieldTowerFinitePadicLift_of_finitePlace

Documentation

Every genuine finite-place decomposition automorphism has a compatible embedded absolute lift with the same finite quotient class and positive integral cyclotomic p-adic degree.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · full declaration

theorem exists_numberFieldTowerFinitePadicLift_of_finitePlace
    (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
    ∃ τ : (numberFieldTowerBaseSubgroup K L).toSubgroup,
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          (numberFieldTowerFiniteQuotientCoordinate
            (K := K) (L := L) τ) =
        σ.1 ∧
      (numberFieldTowerSeparableClosureEquivBaseSubgroup K L).symm τ ∈
        absoluteValueDecompositionGroup K
          (numberFieldTowerFinitePlaceExtensionToSeparableClosure
            K L v
            (chosenFinitePlaceExtension (L := L) v)).1 ∧
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠
        1 ∧
      ∃ n : ℕ, 0 < n ∧
        numberFieldTowerBaseSubgroupPadicCyclotomicDegree
            (K := K) (L := L) 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
  obtain ⟨τΩ, hτΩrestrict, n, hn, hτΩdegree⟩ :=
    exists_finitePlaceSeparableClosureLift_with_positivePadicCyclotomicDegree
      (K := K) (L := L) v p σ
  let τ :
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
    numberFieldTowerSeparableClosureEquivBaseSubgroup
      K L τΩ.1
  have hfinite :
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          (numberFieldTowerFiniteQuotientCoordinate
            (K := K) (L := L) τ) =
        σ.1 := by
    change
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          (QuotientGroup.mk
            (numberFieldTowerSeparableClosureEquivBaseSubgroup
              K L τΩ.1)) =
        σ.1
    rw [
      numberFieldTowerExtensionQuotientEquivGaloisGroup_mk_baseSubgroupEquiv]
    exact congrArg Subtype.val hτΩrestrict
  have hdegree :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ =
        (Multiplicative.ofAdd (1 : ℤ_[p.1])) ^ n := by
    exact hτΩdegree
  have hdecomposition :
      (numberFieldTowerSeparableClosureEquivBaseSubgroup K L).symm τ ∈
        absoluteValueDecompositionGroup K
          (numberFieldTowerFinitePlaceExtensionToSeparableClosure
            K L v
            (chosenFinitePlaceExtension (L := L) v)).1 := by
    simpa only [τ, MulEquiv.symm_apply_apply] using τΩ.2
  refine
    ⟨τ, hfinite, hdecomposition, ?_, n, hn, hdegree⟩
  rw [hdegree]
  exact
    PadicInt.multiplicative_positiveNatDegree_ne_one
      p.1 n hn

theorem

numberFieldTowerFiniteQuotientCoordinate_generates_of_galoisGenerator

L1346 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteQuotientCoordinate_generates_of_galoisGenerator

Documentation

Generation of the actual finite Galois group transports back through the compatible finite quotient coordinate.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem
    numberFieldTowerFiniteQuotientCoordinate_generates_of_galoisGenerator
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (σ : Gal(L/K))
    (hτσ :
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          (numberFieldTowerFiniteQuotientCoordinate
            (K := K) (L := L) τ) =
        σ)
    (hσ : Subgroup.closure ({σ} : Set (Gal(L/K))) = ⊤) :
    Subgroup.closure
        ({numberFieldTowerFiniteQuotientCoordinate
            (K := K) (L := L) τ} :
          Set
            ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
              extensionSubgroup
                (numberFieldTowerBaseSubgroup K L)
                (numberFieldTowerTopSubgroup L)
                (numberFieldTowerTopSubgroup_le_baseSubgroup K L))) =
      ⊤

theorem

numberFieldTowerFinitePadicCyclicPreimage_sup_extensionSubgroup_eq_top

L1391 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicPreimage_sup_extensionSubgroup_eq_top

Documentation

If the finite quotient coordinate of a lift generates the whole finite Galois quotient, then its cyclic preimage together with the top-field subgroup generates the whole embedded absolute Galois group.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem
    numberFieldTowerFinitePadicCyclicPreimage_sup_extensionSubgroup_eq_top
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hgenerate :
      Subgroup.closure
          ({numberFieldTowerFiniteQuotientCoordinate
              (K := K) (L := L) τ} :
            Set
              ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
                extensionSubgroup
                  (numberFieldTowerBaseSubgroup K L)
                  (numberFieldTowerTopSubgroup L)
                  (numberFieldTowerTopSubgroup_le_baseSubgroup K L))) =
        ⊤) :
    (numberFieldTowerFinitePadicCyclicPreimage
          (K := K) (L := L) p τ).toSubgroup ⊔
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L) =
      ⊤

theorem

numberFieldTowerFinitePadicCyclicFixedSubgroup_sup_topSubgroup

L1527 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedSubgroup_sup_topSubgroup

Documentation

Ambient form of the generation statement: the auxiliary cyclic fixed subgroup together with the subgroup fixing L generates the subgroup fixing K.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem
    numberFieldTowerFinitePadicCyclicFixedSubgroup_sup_topSubgroup
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hgenerate :
      Subgroup.closure
          ({numberFieldTowerFiniteQuotientCoordinate
              (K := K) (L := L) τ} :
            Set
              ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
                extensionSubgroup
                  (numberFieldTowerBaseSubgroup K L)
                  (numberFieldTowerTopSubgroup L)
                  (numberFieldTowerTopSubgroup_le_baseSubgroup K L))) =
        ⊤) :
    (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ).toSubgroup ⊔
        (numberFieldTowerTopSubgroup L).toSubgroup =
      (numberFieldTowerBaseSubgroup K L).toSubgroup

theorem

numberFieldTowerFinitePadicCyclicFixedField_inf_topField

L1577 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedField_inf_topField

Documentation

The concrete auxiliary fixed field is linearly disjoint from L over the compatible embedded copy of K.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem
    numberFieldTowerFinitePadicCyclicFixedField_inf_topField
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hgenerate :
      Subgroup.closure
          ({numberFieldTowerFiniteQuotientCoordinate
              (K := K) (L := L) τ} :
            Set
              ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
                extensionSubgroup
                  (numberFieldTowerBaseSubgroup K L)
                  (numberFieldTowerTopSubgroup L)
                  (numberFieldTowerTopSubgroup_le_baseSubgroup K L))) =
        ⊤) :
    numberFieldTowerFinitePadicCyclicFixedField
          (K := K) (L := L) p τ ⊓
        numberFieldInRationalSeparableClosure L =
      numberFieldTowerBaseField K L

theorem

numberFieldTowerTopField_le_finitePadicCyclicFixedField_sup_padicCyclotomicField

L1628 ↗

GlobalClassFieldTheory.Reciprocity.numberFieldTowerTopField_le_finitePadicCyclicFixedField_sup_padicCyclotomicField

Documentation

If the finite quotient coordinate is p-primary, adjoining the actual rational p-primary cyclotomic field to the auxiliary fixed field contains the compatible copy of L.

This is the field-theoretic conclusion of the simultaneous finite/cyclotomic lift: the intersection of the two fixing subgroups already fixes L, hence their fixed-field compositum contains L.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · statement

theorem
    numberFieldTowerTopField_le_finitePadicCyclicFixedField_sup_padicCyclotomicField
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (n : ℕ) (hn : 0 < n)
    (hdegree :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ =
        (Multiplicative.ofAdd (1 : ℤ_[p.1])) ^ n)
    (hprimary :
      numberFieldTowerFiniteQuotientCoordinate
          (K := K) (L := L) τ ∈
        CommGroup.primaryComponent
          ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
            extensionSubgroup
              (numberFieldTowerBaseSubgroup K L)
              (numberFieldTowerTopSubgroup L)
              (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
          p.1) :
    numberFieldInRationalSeparableClosure L ≤
      numberFieldTowerFinitePadicCyclicFixedField
            (K := K) (L := L) p τ ⊔
        rationalCyclotomicPadicField p

theorem

exists_finitePlaceCyclotomicAuxiliaryFixedField

L1723 ↗

GlobalClassFieldTheory.Reciprocity.exists_finitePlaceCyclotomicAuxiliaryFixedField

Documentation

For a finite-place automorphism generating Gal(L/K), construct the genuine auxiliary number field used in the cyclotomic reduction.

The field is finite over ℚ, contains the compatible copy of K, and has intersection with the compatible copy of L exactly equal to that copy of K. Its defining lift has the prescribed local restriction and positive integral cyclotomic p-adic degree.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · full declaration

theorem exists_finitePlaceCyclotomicAuxiliaryFixedField
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (σ :
      absoluteValueDecompositionGroup K
        (chosenFinitePlaceExtension (L := L) v).1)
    (hσ :
      Subgroup.closure
          ({σ.1} : Set (Gal(L/K))) =
        ⊤) :
    letI _ : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI _ : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI _ : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    ∃ τ : (numberFieldTowerBaseSubgroup K L).toSubgroup,
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          (numberFieldTowerFiniteQuotientCoordinate
            (K := K) (L := L) τ) =
        σ.1 ∧
      (numberFieldTowerSeparableClosureEquivBaseSubgroup K L).symm τ ∈
        absoluteValueDecompositionGroup K
          (numberFieldTowerFinitePlaceExtensionToSeparableClosure
            K L v
            (chosenFinitePlaceExtension (L := L) v)).1 ∧
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠
        1 ∧
      FiniteDimensional ℚ
        (numberFieldTowerFinitePadicCyclicFixedField
          (K := K) (L := L) p τ) ∧
      numberFieldTowerBaseField K L ≤
        numberFieldTowerFinitePadicCyclicFixedField
          (K := K) (L := L) p τ ∧
      numberFieldTowerFinitePadicCyclicFixedField
            (K := K) (L := L) p τ ⊓
          numberFieldInRationalSeparableClosure L =
        numberFieldTowerBaseField K L ∧
      ∃ n : ℕ, 0 < n ∧
        numberFieldTowerBaseSubgroupPadicCyclotomicDegree
            (K := K) (L := L) 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
  obtain
      ⟨τ, hτσ, hτdecomposition, hτdegree,
        n, hn, hdegree⟩ :=
    exists_numberFieldTowerFinitePadicLift_of_finitePlace
      (K := K) (L := L) v p σ
  have hgenerate :=
    numberFieldTowerFiniteQuotientCoordinate_generates_of_galoisGenerator
      (K := K) (L := L) τ σ.1 hτσ hσ
  refine
    ⟨τ, hτσ, hτdecomposition, hτdegree,
      numberFieldTowerFinitePadicCyclicFixedField_finiteDimensional
        (K := K) (L := L) p τ hτdegree,
      numberFieldTowerBaseField_le_finitePadicCyclicFixedField
        (K := K) (L := L) p τ,
      numberFieldTowerFinitePadicCyclicFixedField_inf_topField
        (K := K) (L := L) p τ hgenerate,
      n, hn, hdegree⟩

theorem

exists_finitePlacePrimaryCyclotomicAuxiliaryFixedField

L1798 ↗

GlobalClassFieldTheory.Reciprocity.exists_finitePlacePrimaryCyclotomicAuxiliaryFixedField

Documentation

A p-primary local generator admits a genuine auxiliary number field whose compositum with the rational p-primary cyclotomic field contains L.

Besides the field containment, the construction records the two properties needed for descent: the auxiliary field meets L exactly in K, and the chosen absolute lift has positive integral cyclotomic degree.

Source context 17 commands

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

open scoped IsMulCommutative NumberField
open AlgebraicNumberTheory IsDedekindDomain NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open GlobalClassFields
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⟩
attribute [local instance]
  rationalSeparableClosureAlgebra
local instance finitePadicAuxiliaryExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicAuxiliaryExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance finitePadicAuxiliaryExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) := by
  let e :
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ≃*
        Gal(L / K) :=
    numberFieldTowerExtensionQuotientEquivGaloisGroup K L
  exact
    { is_comm :=
        ⟨fun x y => by
          apply e.injective
          rw [map_mul, map_mul]
          exact
            (inferInstance :
              IsMulCommutative (Gal(L / K))).is_comm.comm
                (e x) (e y)⟩ }

Lean source · full declaration

theorem exists_finitePlacePrimaryCyclotomicAuxiliaryFixedField
    (v : HeightOneSpectrum (𝓞 K))
    (p : Nat.Primes)
    (σ :
      absoluteValueDecompositionGroup K
        (chosenFinitePlaceExtension (L := L) v).1)
    (hgenerate :
      Subgroup.closure
          ({σ.1} : Set (Gal(L/K))) =
        ⊤)
    (hprimary :
      σ.1 ∈
        CommGroup.primaryComponent
          (Gal(L/K)) p.1) :
    letI _ : Algebra K (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureBaseAlgebra K L
    letI _ : Algebra L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureTopAlgebra L
    letI _ : IsScalarTower K L (SeparableClosure ℚ) :=
      numberFieldTowerSeparableClosureScalarTower K L
    ∃ τ : (numberFieldTowerBaseSubgroup K L).toSubgroup,
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
          (numberFieldTowerFiniteQuotientCoordinate
            (K := K) (L := L) τ) =
        σ.1 ∧
      (numberFieldTowerSeparableClosureEquivBaseSubgroup K L).symm τ ∈
        absoluteValueDecompositionGroup K
          (numberFieldTowerFinitePlaceExtensionToSeparableClosure
            K L v
            (chosenFinitePlaceExtension (L := L) v)).1 ∧
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠
        1 ∧
      FiniteDimensional ℚ
        (numberFieldTowerFinitePadicCyclicFixedField
          (K := K) (L := L) p τ) ∧
      numberFieldTowerBaseField K L ≤
        numberFieldTowerFinitePadicCyclicFixedField
          (K := K) (L := L) p τ ∧
      numberFieldTowerFinitePadicCyclicFixedField
            (K := K) (L := L) p τ ⊓
          numberFieldInRationalSeparableClosure L =
        numberFieldTowerBaseField K L ∧
      numberFieldInRationalSeparableClosure L ≤
        numberFieldTowerFinitePadicCyclicFixedField
              (K := K) (L := L) p τ ⊔
          rationalCyclotomicPadicField p ∧
      ∃ n : ℕ, 0 < n ∧
        numberFieldTowerBaseSubgroupPadicCyclotomicDegree
            (K := K) (L := L) 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
  obtain
      ⟨τ, hτσ, hτdecomposition, hτdegree,
        hfinite, hbase, hintersection,
        n, hn, hdegree⟩ :=
    exists_finitePlaceCyclotomicAuxiliaryFixedField
      (K := K) (L := L) v p σ hgenerate
  have hprimaryQuotient :
      numberFieldTowerFiniteQuotientCoordinate
          (K := K) (L := L) τ ∈
        CommGroup.primaryComponent
          ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
            extensionSubgroup
              (numberFieldTowerBaseSubgroup K L)
              (numberFieldTowerTopSubgroup L)
              (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
          p.1 := by
    obtain ⟨m, hm⟩ := hprimary
    refine ⟨m, ?_⟩
    let e :=
      numberFieldTowerExtensionQuotientEquivGaloisGroup K L
    let q :=
      numberFieldTowerFiniteQuotientCoordinate
        (K := K) (L := L) τ
    let N : ℕ := p.1 ^ m
    have hq : e q = σ.1 := by
      exact hτσ
    have hmN : σ.1 ^ N = 1 := by
      exact hm
    change q ^ N = 1
    apply e.injective
    calc
      e (q ^ N) = (e q) ^ N := by
        exact map_pow e q N
      _ = σ.1 ^ N := by rw [hq]
      _ = 1 := hmN
      _ = e 1 := (map_one e).symm
  have hcontainment :=
    numberFieldTowerTopField_le_finitePadicCyclicFixedField_sup_padicCyclotomicField
      (K := K) (L := L) p τ n hn hdegree
        hprimaryQuotient
  exact
    ⟨τ, hτσ, hτdecomposition, hτdegree,
      hfinite, hbase, hintersection,
      hcontainment, n, hn, hdegree⟩

Module documentation

The finite p-adic auxiliary field

Declarations