Module

ClosedFiniteIndexClassFieldOriginalField.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldOriginalField

10 declarations indexed from sourceView source ↗

Module documentation

Transport to the original number field

This leaf installs the original-field algebra tower and transports the canonical norm-range computation back to the original idèle class group.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldNormRange

Imported by3

instance

closedFiniteIndexClassFieldBaseAlgebraOverOriginal

L31 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldBaseAlgebraOverOriginal

Documentation

The canonical fixed-field copy, regarded as an algebra over the original number field.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexClassFieldBaseAlgebraOverOriginal
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    Algebra K
      (closedFiniteIndexClassFieldBase
        (K := K) H hclosed)

def

closedFiniteIndexClassFieldBaseEquivOverOriginal

L43 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldBaseEquivOverOriginal

Documentation

The base-field identification as an equivalence of algebras over the original number field.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

def closedFiniteIndexClassFieldBaseEquivOverOriginal
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    K ≃ₐ[K]
      closedFiniteIndexClassFieldBase
        (K := K) H hclosed

instance

closedFiniteIndexClassFieldAlgebraOverOriginal

L57 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldAlgebraOverOriginal

Documentation

The selected class field, regarded as an algebra over the original number field through its canonical fixed-field copy.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexClassFieldAlgebraOverOriginal
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    Algebra K
      (closedFiniteIndexClassField
        (K := K) H hclosed)

theorem

closedFiniteIndexClassField_algebraMap_original

L76 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassField_algebraMap_original

Documentation

The scalar map into the selected class field is the canonical base equivalence followed by fixed-field inclusion.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem closedFiniteIndexClassField_algebraMap_original
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
    (x : K) :
    algebraMap K
        (closedFiniteIndexClassField
          (K := K) H hclosed) x =
      algebraMap
        (closedFiniteIndexClassFieldBase
          (K := K) H hclosed)
        (closedFiniteIndexClassField
          (K := K) H hclosed)
        (closedFiniteIndexClassFieldBaseEquiv
          (K := K) H hclosed x)

instance

closedFiniteIndexClassFieldBaseFiniteDimensionalOverOriginal

L93 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldBaseFiniteDimensionalOverOriginal

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance
    closedFiniteIndexClassFieldBaseFiniteDimensionalOverOriginal
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    FiniteDimensional K
      (closedFiniteIndexClassFieldBase
        (K := K) H hclosed)

instance

closedFiniteIndexClassFieldScalarTowerOverOriginal

L104 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldScalarTowerOverOriginal

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexClassFieldScalarTowerOverOriginal
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    IsScalarTower K
      (closedFiniteIndexClassFieldBase
        (K := K) H hclosed)
      (closedFiniteIndexClassField
        (K := K) H hclosed)

instance

closedFiniteIndexClassFieldFiniteDimensionalOverOriginal

L115 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldFiniteDimensionalOverOriginal

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance
    closedFiniteIndexClassFieldFiniteDimensionalOverOriginal
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    FiniteDimensional K
      (closedFiniteIndexClassField
        (K := K) H hclosed)

instance

closedFiniteIndexClassFieldIsGaloisOverOriginal

L129 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldIsGaloisOverOriginal

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance closedFiniteIndexClassFieldIsGaloisOverOriginal
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    IsGalois K
      (closedFiniteIndexClassField
        (K := K) H hclosed)

instance

closedFiniteIndexClassFieldIsAbelianGaloisOverOriginal

L189 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldIsAbelianGaloisOverOriginal

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

instance
    closedFiniteIndexClassFieldIsAbelianGaloisOverOriginal
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    IsAbelianGalois K
      (closedFiniteIndexClassField
        (K := K) H hclosed)

theorem

closedFiniteIndexClassField_ideleClassNorm_range

L205 ↗

GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassField_ideleClassNorm_range

Documentation

The selected class field has determinant-norm range exactly H in the idèle class group of the original number field.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]

Lean source · statement

theorem closedFiniteIndexClassField_ideleClassNorm_range
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    (_root_.ideleClassNorm K
      (closedFiniteIndexClassField
        (K := K) H hclosed)).range = H

Module documentation

Transport to the original number field

Declarations