NYLL
Module

ClosedFiniteIndexClassFieldConstruction.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldConstruction
8 declarations indexed from sourceView source ↗

Module documentation

Construction of a closed finite-index class field

This leaf fixes the finite Galois norm neighbourhood, abstract subextension, and canonical fixed-field presentation attached to a closed finite-index idèle-class subgroup. Norm-range and reciprocity statements live in later leaves so their elaboration environments do not remain resident here.

Imports3
Imported by2

Declarations

abbrev

closedFiniteIndexClassFieldNormAmbient

L35 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldNormAmbient
Documentation

The concrete finite Galois norm neighbourhood used to construct the class field of H.

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
abbrev closedFiniteIndexClassFieldNormAmbient
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] : Type
theorem

closedFiniteIndexClassFieldNormAmbient_normRange_le

L43 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldNormAmbient_normRange_le
Documentation

The named norm-neighbourhood containment used by the selected ordinary class-field construction.

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 closedFiniteIndexClassFieldNormAmbient_normRange_le
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    (_root_.ideleClassNorm K
      (closedFiniteIndexClassFieldNormAmbient
        (K := K) H hclosed)).range ≤ H
abbrev

closedFiniteIndexClassFieldBaseSubgroup

L56 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldBaseSubgroup
Documentation

The compatible abstract base subgroup used by the selected class field of H.

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
abbrev closedFiniteIndexClassFieldBaseSubgroup
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex]
abbrev

closedFiniteIndexClassFieldReciprocityFiniteAbstractField

L68 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldReciprocityFiniteAbstractField
Documentation

A reducible finite-abstract-field package whose field projection is definitionally the selected base subgroup. Keeping this presentation transparent avoids dependent quotient transports through the opaque tower package in reciprocity consumers.

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
abbrev
    closedFiniteIndexClassFieldReciprocityFiniteAbstractField
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    ClassFormation.FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
abbrev

closedFiniteIndexClassFieldSubextension

L81 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldSubextension
Documentation

The finite abelian subextension selected by a closed finite-index idèle-class subgroup.

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
abbrev closedFiniteIndexClassFieldSubextension
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    ClassFormation.FiniteAbelianSubextension
      (closedFiniteIndexClassFieldBaseSubgroup
        (K := K) H hclosed)
abbrev

closedFiniteIndexClassFieldBase

L96 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldBase
Documentation

The canonical fixed-field copy of the original number field used by the selected class field of H.

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
abbrev closedFiniteIndexClassFieldBase
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] : Type
abbrev

closedFiniteIndexClassField

L105 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassField
Documentation

The actual finite abelian class field selected by H.

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
abbrev closedFiniteIndexClassField
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] : Type
abbrev

closedFiniteIndexClassFieldBaseEquiv

L117 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldBaseEquiv
Documentation

The canonical equivalence from the original number field to the fixed-field base of its selected class 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
abbrev closedFiniteIndexClassFieldBaseEquiv
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    K ≃ₐ[ℚ]
      closedFiniteIndexClassFieldBase
        (K := K) H hclosed

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