NYLL
Module

FinitePadicCyclicData.lean

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

Module documentation

Finite p-adic cyclic data for local-global Artin compatibility

This module packages the simultaneous finite-quotient and cyclotomic coordinates and the corresponding abstract auxiliary subextension.

Imports1
Imported by4

Declarations

instance

(anonymous instance)

L37 ↗
Source context 11 commands

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

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

numberFieldTowerExtensionNormal

L40 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerExtensionNormal
Source context 12 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
Lean source · statement
instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal
instance

finitePadicTowerExtensionQuotientFinite

L47 ↗
GlobalClassFieldTheory.Reciprocity.finitePadicTowerExtensionQuotientFinite
Source context 13 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
Lean source · statement
instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
instance

numberFieldTowerExtensionQuotientIsMulCommutative

L56 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerExtensionQuotientIsMulCommutative
Source context 14 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
Lean source · statement
instance numberFieldTowerExtensionQuotientIsMulCommutative :
    IsMulCommutative
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
instance

numberFieldTowerBaseSubgroupCompactSpace

L81 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseSubgroupCompactSpace
Source context 15 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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 numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup
def

continuousSubgroupSubtype

L88 ↗
GlobalClassFieldTheory.Reciprocity.continuousSubgroupSubtype
Documentation

Inclusion of a subgroup equipped with its subtype topology.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · full declaration
def continuousSubgroupSubtype
    {A : Type*} [Group A] [TopologicalSpace A]
    (H : Subgroup A) : H →ₜ* A where
  toMonoidHom := H.subtype
  continuous_toFun := continuous_subtype_val
def

numberFieldTowerFiniteQuotientCoordinate

L96 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFiniteQuotientCoordinate
Documentation

The finite quotient coordinate on the compatible embedded copy of the absolute Galois group of K.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def numberFieldTowerFiniteQuotientCoordinate :
    (numberFieldTowerBaseSubgroup K L).toSubgroup →ₜ*
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L))
def

rationalSeparableClosurePadicCyclotomicDegree

L114 ↗
GlobalClassFieldTheory.Reciprocity.rationalSeparableClosurePadicCyclotomicDegree
Documentation

The genuine p-adic cyclotomic degree on the rational absolute Galois group.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def rationalSeparableClosurePadicCyclotomicDegree
    (p : Nat.Primes) :
    Gal(SeparableClosure ℚ / ℚ) →ₜ*
      Multiplicative ℤ_[p.1]
theorem

rationalSeparableClosurePadicCyclotomicDegree_ker

L124 ↗
GlobalClassFieldTheory.Reciprocity.rationalSeparableClosurePadicCyclotomicDegree_ker
Documentation

The kernel of the absolute p-adic cyclotomic degree is exactly the fixing subgroup of the actual p-primary cyclotomic field in the rational separable closure.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem rationalSeparableClosurePadicCyclotomicDegree_ker
    (p : Nat.Primes) :
    (rationalSeparableClosurePadicCyclotomicDegree
        p).toMonoidHom.ker =
      (rationalCyclotomicPadicField p).fixingSubgroup
def

numberFieldTowerBaseSubgroupPadicCyclotomicDegree

L196 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerBaseSubgroupPadicCyclotomicDegree
Documentation

The genuine rational cyclotomic p-adic degree restricted to the compatible embedded copy of the absolute Galois group of K.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def numberFieldTowerBaseSubgroupPadicCyclotomicDegree
    (p : Nat.Primes) :
    (numberFieldTowerBaseSubgroup K L).toSubgroup →ₜ*
      Multiplicative ℤ_[p.1]
def

numberFieldTowerFinitePadicCoordinate

L206 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCoordinate
Documentation

The simultaneous finite-extension and cyclotomic p-adic coordinate on the compatible absolute Galois group of K.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def numberFieldTowerFinitePadicCoordinate
    (p : Nat.Primes) :
    (numberFieldTowerBaseSubgroup K L).toSubgroup →ₜ*
      (((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ×
        Multiplicative ℤ_[p.1])
def

numberFieldTowerFinitePadicImage

L236 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicImage
Documentation

The actual image of the simultaneous finite and p-adic cyclotomic coordinate, as a closed subgroup of the product.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def numberFieldTowerFinitePadicImage
    (p : Nat.Primes) :
    ClosedSubgroup
      (((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
          extensionSubgroup
            (numberFieldTowerBaseSubgroup K L)
            (numberFieldTowerTopSubgroup L)
            (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) ×
        Multiplicative ℤ_[p.1])
def

numberFieldTowerFinitePadicImageDegree

L269 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicImageDegree
Documentation

The p-adic degree on the actual simultaneous-coordinate image is its second projection.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def numberFieldTowerFinitePadicImageDegree
    (p : Nat.Primes) :
    (numberFieldTowerFinitePadicImage
        (K := K) (L := L) p).toSubgroup →ₜ*
      Multiplicative ℤ_[p.1]
theorem

numberFieldTowerFinitePadicImageDegree_ker_finite

L284 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicImageDegree_ker_finite
Documentation

The kernel of the p-adic degree on the simultaneous-coordinate image is finite: its first projection injects it into the finite Galois quotient.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem numberFieldTowerFinitePadicImageDegree_ker_finite
    (p : Nat.Primes) :
    Finite
      (numberFieldTowerFinitePadicImageDegree
        (K := K) (L := L) p).toMonoidHom.ker
def

numberFieldTowerFinitePadicRangeRestriction

L315 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicRangeRestriction
Documentation

The simultaneous coordinate with codomain restricted to its actual closed image.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def numberFieldTowerFinitePadicRangeRestriction
    (p : Nat.Primes) :
    (numberFieldTowerBaseSubgroup K L).toSubgroup →ₜ*
      (numberFieldTowerFinitePadicImage
        (K := K) (L := L) p).toSubgroup
theorem

numberFieldTowerFinitePadicImageDegree_rangeRestriction_apply

L332 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicImageDegree_rangeRestriction_apply
Documentation

The degree projection of the restricted simultaneous coordinate is the original cyclotomic degree. Keeping this pointwise boundary avoids unfolding the closed-image package in downstream proofs.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem numberFieldTowerFinitePadicImageDegree_rangeRestriction_apply
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    numberFieldTowerFinitePadicImageDegree
        (K := K) (L := L) p
        (numberFieldTowerFinitePadicRangeRestriction
          (K := K) (L := L) p τ) =
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
        (K := K) (L := L) p τ
theorem

numberFieldTowerFinitePadicRangeRestriction_surjective

L345 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicRangeRestriction_surjective
Documentation

Restriction to the actual simultaneous-coordinate image is surjective.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem numberFieldTowerFinitePadicRangeRestriction_surjective
    (p : Nat.Primes) :
    Function.Surjective
      (numberFieldTowerFinitePadicRangeRestriction
        (K := K) (L := L) p)
def

numberFieldTowerFinitePadicCyclicPreimage

L357 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicPreimage
Documentation

The inverse image in the compatible absolute Galois group of the closed cyclic subgroup generated by one simultaneous finite/p-adic coordinate.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def numberFieldTowerFinitePadicCyclicPreimage
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    ClosedSubgroup
      (numberFieldTowerBaseSubgroup K L).toSubgroup
theorem

numberFieldTowerFinitePadicCyclicPreimage_normal

L384 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicPreimage_normal
Documentation

The simultaneous finite/cyclotomic coordinate has abelian image, so the inverse image of the closed cyclic subgroup generated by one coordinate is normal in the compatible absolute Galois group of K.

Consequently, the auxiliary fixed field constructed below is Galois over the embedded copy of K, as in the field diagram of the finite-place reduction.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem numberFieldTowerFinitePadicCyclicPreimage_normal
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    (numberFieldTowerFinitePadicCyclicPreimage
      (K := K) (L := L) p τ).toSubgroup.Normal
theorem

numberFieldTowerFinitePadicCyclicPreimage_isOpen

L408 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicPreimage_isOpen
Documentation

A lift with nontrivial p-adic degree generates an open cyclic preimage in the compatible absolute Galois group.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem numberFieldTowerFinitePadicCyclicPreimage_isOpen
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hτ :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠
        1) :
    IsOpen
      ((numberFieldTowerFinitePadicCyclicPreimage
          (K := K) (L := L) p τ :
        ClosedSubgroup
          (numberFieldTowerBaseSubgroup K L).toSubgroup) :
        Set (numberFieldTowerBaseSubgroup K L).toSubgroup)
theorem

numberFieldTowerFinitePadicCyclicImageDegree_injective

L453 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicImageDegree_injective
Documentation

For a lift whose finite coordinate is p-primary and whose cyclotomic degree is a positive integer, the p-adic degree is injective on its actual closed cyclic image.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · full declaration
theorem numberFieldTowerFinitePadicCyclicImageDegree_injective
    (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) :
    let P :=
      numberFieldTowerFinitePadicImage
        (K := K) (L := L) p
    let γ : P.toSubgroup :=
      numberFieldTowerFinitePadicRangeRestriction
        (K := K) (L := L) p τ
    Function.Injective
      (((numberFieldTowerFinitePadicImageDegree
          (K := K) (L := L) p).comp
        (continuousSubgroupSubtype
          (ClassFormation.padicCyclicClosure γ).toSubgroup)) :
        ClassFormation.padicCyclicClosure γ →
          Multiplicative ℤ_[p.1]) := by
  dsimp only
  let H :=
    numberFieldTowerBaseSubgroup K L
  let T :=
    numberFieldTowerTopSubgroup L
  let N :=
    extensionSubgroup H T
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)
  let Q := H.toSubgroup ⧸ N
  let P :=
    numberFieldTowerFinitePadicImage
      (K := K) (L := L) p
  let γ : P.toSubgroup :=
    numberFieldTowerFinitePadicRangeRestriction
      (K := K) (L := L) p τ
  let finiteProjection :
      P.toSubgroup →ₜ* Q :=
    { toFun := fun z => z.1.1
      map_one' := rfl
      map_mul' := fun _ _ => rfl
      continuous_toFun :=
        continuous_fst.comp continuous_subtype_val }
  let degree :=
    numberFieldTowerFinitePadicImageDegree
      (K := K) (L := L) p
  let extensionSubgroupClosed : IsClosed (N : Set H.toSubgroup) :=
    extensionSubgroup_isClosed H T
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)
  let extensionSubgroupFiniteIndex : N.FiniteIndex :=
    N.finiteIndex_of_finite_quotient
  let quotientDiscreteTopology : DiscreteTopology Q :=
    QuotientGroup.discreteTopology
      (N.isOpen_of_isClosed_of_finiteIndex
        extensionSubgroupClosed)
  obtain ⟨m, hm⟩ := hprimary
  apply
    ClassFormation.padicCyclicClosure_degree_injective_of_primePower_finiteCoordinate
        p.1 finiteProjection degree
        (γ := γ) (m := m) (n := n)
  · intro x y hxy
    apply Subtype.ext
    exact hxy
  · exact hn
  · exact hm
  · exact hdegree
theorem

numberFieldTowerFinitePadicCyclicPreimage_inf_padicKernel_le_extensionSubgroup

L533 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicPreimage_inf_padicKernel_le_extensionSubgroup
Documentation

On a positive-degree lift with p-primary finite coordinate, the intersection of its cyclic preimage with the cyclotomic p-adic kernel already fixes L.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem
    numberFieldTowerFinitePadicCyclicPreimage_inf_padicKernel_le_extensionSubgroup
    (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) :
    (numberFieldTowerFinitePadicCyclicPreimage
          (K := K) (L := L) p τ).toSubgroup ⊓
        (numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p).toMonoidHom.ker ≤
      extensionSubgroup
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerTopSubgroup L)
        (numberFieldTowerTopSubgroup_le_baseSubgroup K L)
def

numberFieldTowerFinitePadicCyclicFixedSubgroup

L606 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedSubgroup
Documentation

The cyclic preimage, embedded back into the rational absolute Galois group. Its fixed field is the concrete auxiliary number field used in the finite-place reduction.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def numberFieldTowerFinitePadicCyclicFixedSubgroup
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    ClosedSubgroup (Gal(SeparableClosure ℚ / ℚ))
theorem

numberFieldTowerFinitePadicCyclicFixedSubgroup_generator_mem

L629 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedSubgroup_generator_mem
Documentation

The distinguished simultaneous finite/cyclotomic lift itself lies in the auxiliary subgroup whose fixed field is used for descent.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem numberFieldTowerFinitePadicCyclicFixedSubgroup_generator_mem
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    (τ : Gal(SeparableClosure ℚ / ℚ)) ∈
      (numberFieldTowerFinitePadicCyclicFixedSubgroup
        (K := K) (L := L) p τ).toSubgroup
theorem

numberFieldTowerFinitePadicCyclicFixedSubgroup_le_baseSubgroup

L657 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedSubgroup_le_baseSubgroup
Documentation

The auxiliary cyclic fixed subgroup lies in the subgroup fixing the compatible embedded copy of K.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem numberFieldTowerFinitePadicCyclicFixedSubgroup_le_baseSubgroup
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ).toSubgroup ≤
      (numberFieldTowerBaseSubgroup K L).toSubgroup
theorem

numberFieldTowerFinitePadicCyclicFixedSubgroup_extension_normal

L674 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedSubgroup_extension_normal
Documentation

The auxiliary fixed field is Galois over the compatible embedded copy of K. On subgroup coordinates this is normality of the embedded cyclic-preimage subgroup inside the base fixing subgroup.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem
    numberFieldTowerFinitePadicCyclicFixedSubgroup_extension_normal
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerFinitePadicCyclicFixedSubgroup
        (K := K) (L := L) p τ)
      (numberFieldTowerFinitePadicCyclicFixedSubgroup_le_baseSubgroup
        (K := K) (L := L) p τ)).Normal
theorem

numberFieldTowerFinitePadicCyclicFixedSubgroup_extensionSubgroup

L718 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedSubgroup_extensionSubgroup
Documentation

The relative subgroup defined by the ambient auxiliary fixed subgroup is exactly the original cyclic preimage inside the compatible absolute Galois group of K.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem
    numberFieldTowerFinitePadicCyclicFixedSubgroup_extensionSubgroup
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    extensionSubgroup
        (numberFieldTowerBaseSubgroup K L)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ)
        (numberFieldTowerFinitePadicCyclicFixedSubgroup_le_baseSubgroup
          (K := K) (L := L) p τ) =
      (numberFieldTowerFinitePadicCyclicPreimage
        (K := K) (L := L) p τ).toSubgroup
theorem

numberFieldTowerFinitePadicCyclicFixedSubgroup_inf_absolutePadicKernel_le_topSubgroup

L749 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedSubgroup_inf_absolutePadicKernel_le_topSubgroup
Documentation

Ambient form of the kernel-intersection statement.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem
    numberFieldTowerFinitePadicCyclicFixedSubgroup_inf_absolutePadicKernel_le_topSubgroup
    (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) :
    (numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ).toSubgroup ⊓
        (rationalSeparableClosurePadicCyclotomicDegree
          p).toMonoidHom.ker ≤
      (numberFieldTowerTopSubgroup L).toSubgroup
theorem

numberFieldTowerFinitePadicCyclicFixedSubgroup_isOpen

L804 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicFixedSubgroup_isOpen
Documentation

A nonzero-degree cyclic lift cuts out an open subgroup of the rational absolute Galois group.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem numberFieldTowerFinitePadicCyclicFixedSubgroup_isOpen
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hτ :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠
        1) :
    IsOpen
      ((numberFieldTowerFinitePadicCyclicFixedSubgroup
          (K := K) (L := L) p τ :
        ClosedSubgroup
          (Gal(SeparableClosure ℚ / ℚ))) :
        Set (Gal(SeparableClosure ℚ / ℚ)))
def

numberFieldTowerFinitePadicCyclicGaloisSubextension

L833 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicCyclicGaloisSubextension
Documentation

The auxiliary cyclic fixed subgroup as a genuine finite Galois subextension of the compatible abstract field attached to K.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · full declaration
def
    numberFieldTowerFinitePadicCyclicGaloisSubextension
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hτ :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠
        1) :
    FiniteGaloisSubextension
      (numberFieldTowerBaseSubgroup K L) where
  field :=
    numberFieldTowerFinitePadicCyclicFixedSubgroup
      (K := K) (L := L) p τ
  below :=
    numberFieldTowerFinitePadicCyclicFixedSubgroup_le_baseSubgroup
      (K := K) (L := L) p τ
  normal :=
    numberFieldTowerFinitePadicCyclicFixedSubgroup_extension_normal
      (K := K) (L := L) p τ
  finite := by
    rw [
      numberFieldTowerFinitePadicCyclicFixedSubgroup_extensionSubgroup
        (K := K) (L := L) p τ]
    exact
      Subgroup.quotient_finite_of_isOpen
        (numberFieldTowerFinitePadicCyclicPreimage
          (K := K) (L := L) p τ).toSubgroup
        (numberFieldTowerFinitePadicCyclicPreimage_isOpen
          (K := K) (L := L) p τ hτ)
def

numberFieldTowerFinitePadicAuxiliaryAbstractField

L866 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryAbstractField
Documentation

The auxiliary fixed subgroup, with its absolute finite-index witness, as the finite abstract field used by fixed-field global reciprocity.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def numberFieldTowerFinitePadicAuxiliaryAbstractField
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup)
    (hτ :
      numberFieldTowerBaseSubgroupPadicCyclotomicDegree
          (K := K) (L := L) p τ ≠
        1) :
    FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
def

numberFieldTowerFinitePadicAuxiliaryCompositumSubextension

L883 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
Documentation

Base change of L / K to the auxiliary cyclic fixed field. Its top subgroup is the intersection of the auxiliary fixing subgroup with the subgroup fixing L, hence its concrete top field is the auxiliary compositum with L.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
def
    numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
    (p : Nat.Primes)
    (τ : (numberFieldTowerBaseSubgroup K L).toSubgroup) :
    FiniteAbelianSubextension
      (numberFieldTowerFinitePadicCyclicFixedSubgroup
        (K := K) (L := L) p τ)
theorem

numberFieldTowerFinitePadicAuxiliaryCompositumSubextension_isUnramified

L900 ↗
GlobalClassFieldTheory.Reciprocity.numberFieldTowerFinitePadicAuxiliaryCompositumSubextension_isUnramified
Documentation

The auxiliary compositum is unramified for the genuine cyclotomic degree datum. The proof is the key p-primary intersection: full cyclotomic inertia lies in every p-adic cyclotomic kernel, and the latter intersection already fixes L.

Source context 16 commands

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

open scoped IsMulCommutative NumberField
open NumberField
open IdeleGroup RelativeIdeleGroup
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open CyclicCohomology
open KummerTheory ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
local instance (p : Nat.Primes) : Fact p.1.Prime :=
  ⟨p.2⟩
local instance numberFieldTowerExtensionNormal :
    (extensionSubgroup
      (numberFieldTowerBaseSubgroup K L)
      (numberFieldTowerTopSubgroup L)
      (numberFieldTowerTopSubgroup_le_baseSubgroup K L)).Normal :=
  numberFieldTowerExtensionSubgroup_normal K L
local instance finitePadicTowerExtensionQuotientFinite :
    Finite
      ((numberFieldTowerBaseSubgroup K L).toSubgroup ⧸
        extensionSubgroup
          (numberFieldTowerBaseSubgroup K L)
          (numberFieldTowerTopSubgroup L)
          (numberFieldTowerTopSubgroup_le_baseSubgroup K L)) :=
  numberFieldTowerExtensionQuotient_finite K L
noncomputable local instance numberFieldTowerExtensionQuotientIsMulCommutative :
    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)⟩ }
local instance numberFieldTowerBaseSubgroupCompactSpace :
    CompactSpace
      (numberFieldTowerBaseSubgroup K L).toSubgroup :=
  isCompact_iff_compactSpace.mp
    (numberFieldTowerBaseSubgroup K L).isClosed'.isCompact
Lean source · statement
theorem
    numberFieldTowerFinitePadicAuxiliaryCompositumSubextension_isUnramified
    (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) :
    (numberFieldTowerFinitePadicAuxiliaryCompositumSubextension
        (K := K) (L := L) p τ).toFiniteGaloisExtension.IsUnramified
      rationalCyclotomicDegreeData

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