Module

FiniteAbelianClassFieldCorrespondenceTopology.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FiniteAbelianClassFieldCorrespondenceTopology

15 declarations indexed from sourceView source ↗

Module documentation

Ordinary topology in the finite abelian class-field correspondence

The ordinary norm subgroup attached to a finite abelian subextension is the genuine determinant-norm range on its canonical actual fixed fields. Consequently it is open and closed in the ordinary idele-class topology and has finite index.

The actual fixed fields are exposed below through named carriers with canonical instances. This keeps the public topology statements free of local-instance towers. The selected class field of a closed finite-index subgroup, together with its norm-range and degree-index theorems, is provided by ClosedFiniteIndexClassField.

Imports3

Imported by2

instance

finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra

L41 ↗

GlobalClassFieldTheory.GlobalClassFields.finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra

Documentation

Use the same rational algebra structure as the ordinary correspondence when constructing all named fixed-field carriers below.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity

Lean source · statement

instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ)

abbrev

ordinaryIdeleClassNormBase

L47 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormBase

Documentation

The actual fixed-field base represented by a finite abstract field.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

abbrev ordinaryIdeleClassNormBase
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) : Type

abbrev

ordinaryIdeleClassNormExtension

L54 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormExtension

Documentation

The actual relative fixed field represented by a finite abelian subextension.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

abbrev ordinaryIdeleClassNormExtension
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) : Type

instance

ordinaryIdeleClassNormBaseFiniteDimensional

L60 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormBaseFiniteDimensional

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

instance ordinaryIdeleClassNormBaseFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    FiniteDimensional ℚ (ordinaryIdeleClassNormBase K)

instance

ordinaryIdeleClassNormExtensionFiniteDimensional

L67 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormExtensionFiniteDimensional

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

instance ordinaryIdeleClassNormExtensionFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional
      (ordinaryIdeleClassNormBase K)
      (ordinaryIdeleClassNormExtension K L)

instance

ordinaryIdeleClassNormScalarTower

L78 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormScalarTower

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

instance ordinaryIdeleClassNormScalarTower
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsScalarTower ℚ
      (ordinaryIdeleClassNormBase K)
      (ordinaryIdeleClassNormExtension K L)

instance

ordinaryIdeleClassNormExtensionAbsoluteFiniteDimensional

L87 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormExtensionAbsoluteFiniteDimensional

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

instance ordinaryIdeleClassNormExtensionAbsoluteFiniteDimensional
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    FiniteDimensional ℚ
      (ordinaryIdeleClassNormExtension K L)

instance

ordinaryIdeleClassNormBaseNumberField

L97 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormBaseNumberField

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

instance ordinaryIdeleClassNormBaseNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    NumberField (ordinaryIdeleClassNormBase K)

instance

ordinaryIdeleClassNormExtensionNumberField

L103 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormExtensionNumberField

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

instance ordinaryIdeleClassNormExtensionNumberField
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    NumberField (ordinaryIdeleClassNormExtension K L)

instance

ordinaryIdeleClassNormExtensionIsAbelianGalois

L111 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormExtensionIsAbelianGalois

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

instance ordinaryIdeleClassNormExtensionIsAbelianGalois
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsAbelianGalois
      (ordinaryIdeleClassNormBase K)
      (ordinaryIdeleClassNormExtension K L)

theorem

ordinaryIdeleClassNormSubgroup_eq_namedNormRange

L122 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_eq_namedNormRange

Documentation

The represented ordinary norm subgroup is the determinant-norm range on the named actual fixed fields.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

theorem ordinaryIdeleClassNormSubgroup_eq_namedNormRange
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    ordinaryIdeleClassNormSubgroup K L =
      (_root_.ideleClassNorm
        (ordinaryIdeleClassNormBase K)
        (ordinaryIdeleClassNormExtension K L)).range.toAddSubgroup

theorem

ordinaryIdeleClassNormSubgroup_isOpen

L137 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_isOpen

Documentation

The ordinary norm subgroup represented by a finite abelian subextension is open in the natural topology of the idele class group of the canonical actual fixed field.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

theorem ordinaryIdeleClassNormSubgroup_isOpen
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsOpen
      (ordinaryIdeleClassNormSubgroup K L :
        Set
          (Additive
            (IdeleClassGroup
              (ordinaryIdeleClassNormBase K))))

theorem

ordinaryIdeleClassNormSubgroup_isClosed

L154 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_isClosed

Documentation

The ordinary norm subgroup represented by a finite abelian subextension is closed in the natural idele-class topology.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

theorem ordinaryIdeleClassNormSubgroup_isClosed
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    IsClosed
      (ordinaryIdeleClassNormSubgroup K L :
        Set
          (Additive
            (IdeleClassGroup
              (ordinaryIdeleClassNormBase K))))

theorem

ordinaryIdeleClassNormSubgroup_finiteIndex

L171 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_finiteIndex

Documentation

The ordinary norm subgroup represented by a finite abelian subextension has finite index.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

theorem ordinaryIdeleClassNormSubgroup_finiteIndex
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    (ordinaryIdeleClassNormSubgroup K L).FiniteIndex

theorem

ordinaryIdeleClassNormSubgroup_index_eq_finrank

L189 ↗

GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_index_eq_finrank

Documentation

The index of the ordinary norm subgroup represented by a finite abelian subextension is the degree of its actual relative fixed-field extension.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open LocalClassFieldTheory
open Reciprocity
/-- Use the same rational algebra structure as the ordinary correspondence
when constructing all named fixed-field carriers below. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondenceTopology_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra

Lean source · statement

theorem ordinaryIdeleClassNormSubgroup_index_eq_finrank
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    (ordinaryIdeleClassNormSubgroup K L).index =
      Module.finrank
        (ordinaryIdeleClassNormBase K)
        (ordinaryIdeleClassNormExtension K L)

Module documentation

Ordinary topology in the finite abelian class-field correspondence

Declarations