NYLL
Module

IdeleClassDirectLimitFiniteLevelCore.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IdeleClassDirectLimitFiniteLevelCore
11 declarations indexed from sourceView source ↗

Module documentation

Finite levels of the rational idele-class direct limit

Normal closures, finite-level scalar extension, tower base change, and the canonical embeddings into the rational idele-class direct limit.

Imports4
Imported by2

Declarations

instance

rationalIntermediateNumberField

L34 ↗
GlobalClassFieldTheory.Reciprocity.rationalIntermediateNumberField
Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
Lean source · statement
instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K
instance

rationalTowerClassGroupCommGroup

L39 ↗
GlobalClassFieldTheory.Reciprocity.rationalTowerClassGroupCommGroup
Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
instance rationalTowerClassGroupCommGroup
    (K N : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] [FiniteDimensional ℚ N]
    [Algebra K N] [IsScalarTower ℚ K N] [FiniteDimensional K N] :
    CommGroup (TowerRelativeIdeleGroup.ClassGroup ℚ K N)
instance

rationalTowerClassGroupMul

L49 ↗
GlobalClassFieldTheory.Reciprocity.rationalTowerClassGroupMul
Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
instance rationalTowerClassGroupMul
    (K N : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] [FiniteDimensional ℚ N]
    [Algebra K N] [IsScalarTower ℚ K N] [FiniteDimensional K N] :
    Mul (TowerRelativeIdeleGroup.ClassGroup ℚ K N)
def

rationalNormalClosure

L61 ↗
GlobalClassFieldTheory.Reciprocity.rationalNormalClosure
Documentation

The canonical finite Galois closure, inside SeparableClosure ℚ, of a finite rational intermediate field.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
def rationalNormalClosure
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] :
    FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ)
def

rationalBaseFixingCosetEquivNormalClosure

L75 ↗
GlobalClassFieldTheory.Reciprocity.rationalBaseFixingCosetEquivNormalClosure
Documentation

Absolute left cosets fixing a finite rational intermediate field, identified with its embeddings into the canonical normal closure.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
def
    rationalBaseFixingCosetEquivNormalClosure
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] :
    ((RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ)
          (⊥ : IntermediateField ℚ (SeparableClosure ℚ))).toSubgroup ⧸
      extensionSubgroup
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ)
          (⊥ : IntermediateField ℚ (SeparableClosure ℚ)))
        (RamificationTheory.closedFixingSubgroup
          ℚ (SeparableClosure ℚ) K)
        (LocalClassFieldTheory.fixingSubgroupLeBase
          ℚ (SeparableClosure ℚ) K)) ≃
      (K →ₐ[ℚ] rationalNormalClosure K)
def

rationalIntermediateIdeleClassToNormalClosure

L99 ↗
GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToNormalClosure
Documentation

Embed the actual idele class group of a finite rational intermediate field into the relative presentation at its canonical finite Galois closure.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
def rationalIntermediateIdeleClassToNormalClosure
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] :
    IdeleClassGroup K →*
      RelativeIdeleGroup.ClassGroup ℚ (rationalNormalClosure K)
def

rationalIntermediateIdeleClassToDirectLimit

L111 ↗
GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToDirectLimit
Documentation

The canonical map from the actual idele class group of a finite rational intermediate field to the absolute idele-class direct limit.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
def rationalIntermediateIdeleClassToDirectLimit
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] :
    IdeleClassGroup K →* rationalIdeleClassDirectLimit
theorem

rationalIntermediateIdeleClassToDirectLimit_baseChange

L122 ↗
GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToDirectLimit_baseChange
Documentation

Passing from the relative presentation of a finite rational intermediate field to its ordinary idele class group commutes with the canonical map to the absolute direct limit.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
theorem
    rationalIntermediateIdeleClassToDirectLimit_baseChange
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K]
    (c : RelativeIdeleGroup.ClassGroup ℚ K) :
    rationalIntermediateIdeleClassToDirectLimit K
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := K) c) =
      rationalRelativeIdeleClassToDirectLimit
        (rationalNormalClosure K)
        (RelativeIdeleGroup.classEmbedding (IntermediateField.inclusion
          (IntermediateField.le_normalClosure K)) c)
theorem

rationalFiniteGaloisIdeleClassToDirectLimit_baseChange

L155 ↗
GlobalClassFieldTheory.Reciprocity.rationalFiniteGaloisIdeleClassToDirectLimit_baseChange
Documentation

At a finite Galois rational intermediate field, the ordinary idele-class comparison followed by the absolute direct-limit map is the canonical finite-level map itself.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
theorem
    rationalFiniteGaloisIdeleClassToDirectLimit_baseChange
    (E : FiniteGaloisIntermediateField ℚ (SeparableClosure ℚ))
    (c : RelativeIdeleGroup.ClassGroup ℚ E) :
    rationalIntermediateIdeleClassToDirectLimit
        (E : IntermediateField ℚ (SeparableClosure ℚ))
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := E) c) =
      rationalRelativeIdeleClassToDirectLimit E c
theorem

rationalRelativeIdeleClassEmbedding_commutativeSquare

L169 ↗
GlobalClassFieldTheory.Reciprocity.rationalRelativeIdeleClassEmbedding_commutativeSquare
Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
theorem rationalRelativeIdeleClassEmbedding_commutativeSquare
    {F E N₁ N₂ : IntermediateField ℚ (SeparableClosure ℚ)}
    [NumberField F] [NumberField E] [NumberField N₁] [NumberField N₂]
    (hFE : F ≤ E) (hFN₁ : F ≤ N₁) (hEN₂ : E ≤ N₂) (hN₁N₂ : N₁ ≤ N₂)
    (c : RelativeIdeleGroup.ClassGroup ℚ F) :
    RelativeIdeleGroup.classEmbedding (K := ℚ) (L := E) (M := N₂)
        (IntermediateField.inclusion hEN₂)
        (RelativeIdeleGroup.classEmbedding (K := ℚ) (L := F) (M := E)
          (IntermediateField.inclusion hFE) c) =
      RelativeIdeleGroup.classEmbedding (K := ℚ) (L := N₁) (M := N₂)
        (IntermediateField.inclusion hN₁N₂)
        (RelativeIdeleGroup.classEmbedding (K := ℚ) (L := F) (M := N₁)
          (IntermediateField.inclusion hFN₁) c)
theorem

rationalIntermediateIdeleClassToDirectLimit_extension

L194 ↗
GlobalClassFieldTheory.Reciprocity.rationalIntermediateIdeleClassToDirectLimit_extension
Documentation

The canonical maps from nested rational intermediate fields to the idele-class direct limit agree after scalar extension.

Source context 8 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
open CyclicCohomology
attribute [local instance]
  relativeAdeleRingIntermediateAlgebra
local instance rationalIntermediateNumberField
    (K : IntermediateField ℚ (SeparableClosure ℚ))
    [FiniteDimensional ℚ K] : NumberField K :=
  NumberField.of_module_finite ℚ K
Lean source · statement
theorem
    rationalIntermediateIdeleClassToDirectLimit_extension
    {F E : IntermediateField ℚ (SeparableClosure ℚ)}
    [FiniteDimensional ℚ F] [FiniteDimensional ℚ E]
    (hFE : F ≤ E)
    (c : RelativeIdeleGroup.ClassGroup ℚ F) :
    rationalIntermediateIdeleClassToDirectLimit E
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := E)
          (RelativeIdeleGroup.classEmbedding (K := ℚ) (L := F) (M := E)
            (IntermediateField.inclusion hFE) c)) =
      rationalIntermediateIdeleClassToDirectLimit F
        (_root_.relativeIdeleClassBaseChangeMulEquiv
          (K := ℚ) (L := F) c)

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