NYLL
Module

SmallHilbertTowerRealization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.SmallHilbertTowerRealization
66 declarations indexed from sourceView source ↗

Module documentation

Actual realization of the two-stage small Hilbert tower

The first small Hilbert class field is the actual finite abelian subextension selected in HilbertClassFieldRealization. Over its actual fixed field, the closed finite-index small-Hilbert norm subgroup has a finite Galois norm neighbourhood. We embed that neighbourhood in the rational separable closure compatibly with the already chosen first stage. Finite abelian classification then selects the second small Hilbert class field over the literal first-stage subgroup.

The compatibility of the embedding is essential: an unrelated chosen copy of the middle number field would produce a class field over a conjugate closed subgroup rather than over the first-stage subgroup itself.

Imports3
Imported by2

Declarations

def

smallHilbertTowerIdeleClassCommGroup

L49 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerIdeleClassCommGroup
Documentation

The ordinary idèle-class operations used by the two-stage transport, fixed at the canonical principal-subgroup quotient.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
Lean source · statement
def smallHilbertTowerIdeleClassCommGroup
    (F : Type) [Field F] [NumberField F] :
    CommGroup (IdeleClassGroup F)
theorem

addSubgroup_comap_symm_eq_map

L56 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.addSubgroup_comap_symm_eq_map
Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
Lean source · statement
theorem addSubgroup_comap_symm_eq_map
    {A B : Type*} [AddGroup A] [AddGroup B]
    (H : AddSubgroup A) (e : A ≃+ B) :
    H.comap e.symm.toAddMonoidHom =
      H.map e.toAddMonoidHom
abbrev

closedFiniteIndexNormAmbientCanonicalBaseAlgebra

L63 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.closedFiniteIndexNormAmbientCanonicalBaseAlgebra
Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
Lean source · statement
abbrev
    closedFiniteIndexNormAmbientCanonicalBaseAlgebra
    (F : Type) [Field F] [NumberField F]
    (H : Subgroup (IdeleClassGroup F))
    (hclosed : IsClosed (H : Set (IdeleClassGroup F)))
    [H.FiniteIndex] :
    Algebra F
      (closedFiniteIndexClassFieldNormAmbient
        (K := F) H hclosed)
abbrev

smallHilbertTowerMiddleFiniteAbstractField

L81 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerMiddleFiniteAbstractField
Source context 15 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
Lean source · statement
abbrev smallHilbertTowerMiddleFiniteAbstractField :
    FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
instance

smallHilbertTowerMiddleAbstractQuotientFinite

L108 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerMiddleAbstractQuotientFinite
Source context 17 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
Lean source · statement
instance
    smallHilbertTowerMiddleAbstractQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          L.field (le_baseField L.field))
instance

smallHilbertTowerMiddleFiniteDimensional

L119 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerMiddleFiniteDimensional
Source context 17 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
Lean source · statement
instance
    smallHilbertTowerMiddleFiniteDimensional :
    FiniteDimensional ℚ E
instance

smallHilbertTowerMiddleNumberField

L125 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerMiddleNumberField
Source context 17 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
Lean source · statement
instance
    smallHilbertTowerMiddleNumberField :
    NumberField E
def

smallHilbertTowerMiddleNormSubgroup

L133 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerMiddleNormSubgroup
Documentation

The canonical small-Hilbert subgroup over the literal middle field. This typed endpoint avoids repeatedly reducing the finite-abstract-field package merely to recover its field = L.field projection.

Source context 17 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
Lean source · statement
def smallHilbertTowerMiddleNormSubgroup :
    AddSubgroup
      (ambientFixedAddSubgroup
        rationalIdeleClassRepresentation L.field)
theorem

smallHilbertTowerMiddleNormSubgroup_eq_map

L144 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerMiddleNormSubgroup_eq_map
Documentation

The typed comap endpoint is the canonical transported map endpoint. This uses only the generic additive equivalence law.

Source context 17 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
Lean source · statement
theorem smallHilbertTowerMiddleNormSubgroup_eq_map :
    smallHilbertTowerMiddleNormSubgroup K L =
      (smallHilbertClassFieldNormSubgroup (K := E)).toAddSubgroup.map
        (rationalAbstractFixedFieldIdeleClassEquivFixed
          L.field
          (hfinite := smallHilbertTowerMiddleAbstractQuotientFinite K L)).toAddMonoidHom
def

smallHilbertTowerNormAmbientAlgebra

L156 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerNormAmbientAlgebra
Source context 17 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
Lean source · statement
def
    smallHilbertTowerNormAmbientAlgebra :
    Algebra E N
def

smallHilbertTowerNormAmbientSMul

L166 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerNormAmbientSMul
Source context 18 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
Lean source · statement
def
    smallHilbertTowerNormAmbientSMul :
    SMul E N
def

smallHilbertTowerNormAmbientModule

L173 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerNormAmbientModule
Source context 18 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
Lean source · statement
def
    smallHilbertTowerNormAmbientModule :
    Module E N
theorem

smallHilbertTowerNormAmbientScalarTower

L179 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerNormAmbientScalarTower
Source context 18 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
Lean source · statement
theorem
    smallHilbertTowerNormAmbientScalarTower :
    @IsScalarTower ℚ E N
      (Algebra.toSMul (R := ℚ) (A := E))
      (smallHilbertTowerNormAmbientSMul K L)
      (Algebra.toSMul (R := ℚ) (A := N))
def

smallHilbertTowerNormAmbientAlgHom

L190 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerNormAmbientAlgHom
Source context 18 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
Lean source · statement
def
    smallHilbertTowerNormAmbientAlgHom :
    E →ₐ[ℚ] N
theorem

smallHilbertTowerNormAmbientAlgHom_apply

L200 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerNormAmbientAlgHom_apply
Source context 18 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
Lean source · statement
theorem smallHilbertTowerNormAmbientAlgHom_apply
    (x : E) :
    smallHilbertTowerNormAmbientAlgHom K L x =
      algebraMap E N x
theorem

smallHilbertTowerNormAmbientIsGalois

L206 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerNormAmbientIsGalois
Source context 18 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
Lean source · statement
theorem
    smallHilbertTowerNormAmbientIsGalois :
    IsGalois E N
def

smallHilbertNormNeighborhoodForwardAlignment

L218 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodForwardAlignment
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
def
    smallHilbertNormNeighborhoodForwardAlignment :
    SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ
def

smallHilbertNormNeighborhoodAlignment

L234 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodAlignment
Documentation

The separable-closure automorphism which aligns an arbitrary chosen embedding of the norm-neighbourhood field with the already embedded middle field.

Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
def
    smallHilbertNormNeighborhoodAlignment :
    SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ
theorem

smallHilbertNormNeighborhoodForwardAlignment_apply

L240 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodForwardAlignment_apply
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
theorem smallHilbertNormNeighborhoodForwardAlignment_apply
    (x : E) :
    smallHilbertNormNeighborhoodForwardAlignment K L
        (x : SeparableClosure ℚ) =
      (numberFieldSeparableClosureEmbedding N)
        (algebraMap E N x)
def

smallHilbertNormNeighborhoodEmbedding

L267 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodEmbedding
Documentation

A controlled embedding of the concrete finite Galois norm neighbourhood. Its restriction to the middle field is the literal inclusion of that fixed field in SeparableClosure ℚ.

Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
def
    smallHilbertNormNeighborhoodEmbedding :
    N →ₐ[ℚ] SeparableClosure ℚ
theorem

smallHilbertNormNeighborhoodEmbedding_algebraMap

L274 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodEmbedding_algebraMap
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
theorem smallHilbertNormNeighborhoodEmbedding_algebraMap
    (x : E) :
    smallHilbertNormNeighborhoodEmbedding K L
        (algebraMap E N x) =
      (x : SeparableClosure ℚ)
abbrev

smallHilbertNormNeighborhoodEmbeddedBase

L288 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodEmbeddedBase
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
abbrev smallHilbertNormNeighborhoodEmbeddedBase :
    ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
abbrev

smallHilbertNormNeighborhoodEmbeddedField

L296 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodEmbeddedField
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
abbrev smallHilbertNormNeighborhoodEmbeddedField :
    ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)
theorem

smallHilbertNormNeighborhoodEmbeddedField_le_base

L303 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodEmbeddedField_le_base
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
theorem smallHilbertNormNeighborhoodEmbeddedField_le_base :
    (smallHilbertNormNeighborhoodEmbeddedField K L).toSubgroup ≤
      (smallHilbertNormNeighborhoodEmbeddedBase K L).toSubgroup
theorem

smallHilbertNormNeighborhoodEmbeddedBase_eq

L321 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodEmbeddedBase_eq
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
theorem smallHilbertNormNeighborhoodEmbeddedBase_eq :
    smallHilbertNormNeighborhoodEmbeddedBase K L = L.field
def

smallHilbertNormNeighborhoodSeparableClosureEquiv

L344 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormNeighborhoodSeparableClosureEquiv
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · full declaration
def
    smallHilbertNormNeighborhoodSeparableClosureEquiv :
    let j := smallHilbertNormNeighborhoodEmbedding K L
    let i := j.comp (smallHilbertTowerNormAmbientAlgHom K L)
    let : Algebra E (SeparableClosure ℚ) :=
      i.toRingHom.toAlgebra
    SeparableClosure E ≃ₐ[E] SeparableClosure ℚ := by
  intro j i alg
  let : @IsScalarTower ℚ E (SeparableClosure ℚ)
      (Algebra.toSMul (R := ℚ) (A := E))
      alg.toSMul
      (Algebra.toSMul (R := ℚ) (A := SeparableClosure ℚ)) :=
    IsScalarTower.of_algebraMap_eq' i.comp_algebraMap.symm
  let : IsSepClosure E (SeparableClosure ℚ) :=
    ⟨IsSepClosure.sep_closed ℚ,
      Algebra.isSeparable_tower_top_of_isSeparable
        ℚ E (SeparableClosure ℚ)⟩
  exact
    IsSepClosure.equiv E
      (SeparableClosure E) (SeparableClosure ℚ)
def

smallHilbertFiniteGaloisNormNeighborhoodRaw

L365 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodRaw
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
def
    smallHilbertFiniteGaloisNormNeighborhoodRaw :
    FiniteGaloisSubextension
      (smallHilbertNormNeighborhoodEmbeddedBase K L)
def

rebaseFiniteGaloisSubextension

L405 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseFiniteGaloisSubextension
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
def rebaseFiniteGaloisSubextension
    {G : Type} [Group G] [TopologicalSpace G]
    {B B' : ClosedSubgroup G} (h : B = B')
    (P : FiniteGaloisSubextension B) :
    FiniteGaloisSubextension B'
theorem

rebaseFiniteGaloisSubextension_field

L413 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseFiniteGaloisSubextension_field
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
theorem rebaseFiniteGaloisSubextension_field
    {G : Type} [Group G] [TopologicalSpace G]
    {B B' : ClosedSubgroup G} (h : B = B')
    (P : FiniteGaloisSubextension B) :
    (rebaseFiniteGaloisSubextension h P).field = P.field
theorem

rebaseRationalFiniteGaloisSubextension_fixedField_eq

L421 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rebaseRationalFiniteGaloisSubextension_fixedField_eq
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
theorem
    rebaseRationalFiniteGaloisSubextension_fixedField_eq
    {B B' : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)}
    (h : B = B') (P : FiniteGaloisSubextension B) :
    (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
      (rebaseFiniteGaloisSubextension h P).below).restrictScalars ℚ =
        (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
          P.below).restrictScalars ℚ
def

smallHilbertFiniteGaloisNormNeighborhood

L436 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhood
Documentation

An actual finite Galois norm neighbourhood over the literal first-stage subgroup. It is produced by the finite-index Kummer construction and the controlled embedding above.

Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
def smallHilbertFiniteGaloisNormNeighborhood :
    FiniteGaloisSubextension L.field
def

smallHilbertFiniteGaloisNormNeighborhoodNormSubgroup

L444 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodNormSubgroup
Documentation

The abstract norm subgroup of the chosen neighbourhood, pinned to the literal middle-field carrier.

Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
def smallHilbertFiniteGaloisNormNeighborhoodNormSubgroup :
    AddSubgroup
      (ambientFixedAddSubgroup
        rationalIdeleClassRepresentation L.field)
abbrev

smallHilbertFiniteGaloisNormNeighborhoodTopField

L451 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodTopField
Source context 19 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
Lean source · statement
abbrev
    smallHilbertFiniteGaloisNormNeighborhoodTopField : Type
instance

smallHilbertFiniteGaloisNormNeighborhoodQuotientFinite

L459 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodQuotientFinite
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
instance
    smallHilbertFiniteGaloisNormNeighborhoodQuotientFinite :
    Finite
      (L.field.toSubgroup ⧸
        extensionSubgroup L.field
          (smallHilbertFiniteGaloisNormNeighborhood K L).field
          (smallHilbertFiniteGaloisNormNeighborhood K L).below)
instance

smallHilbertFiniteGaloisNormNeighborhoodFiniteDimensional

L468 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodFiniteDimensional
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
instance
    smallHilbertFiniteGaloisNormNeighborhoodFiniteDimensional :
    FiniteDimensional E E₂
instance

smallHilbertFiniteGaloisNormNeighborhoodScalarTower

L477 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodScalarTower
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
instance
    smallHilbertFiniteGaloisNormNeighborhoodScalarTower :
    IsScalarTower ℚ E E₂
instance

smallHilbertFiniteGaloisNormNeighborhoodAbsoluteFiniteDimensional

L482 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodAbsoluteFiniteDimensional
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
instance
    smallHilbertFiniteGaloisNormNeighborhoodAbsoluteFiniteDimensional :
    FiniteDimensional ℚ E₂
instance

smallHilbertFiniteGaloisNormNeighborhoodNumberField

L487 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodNumberField
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
instance
    smallHilbertFiniteGaloisNormNeighborhoodNumberField :
    NumberField E₂
instance

smallHilbertFiniteGaloisNormNeighborhoodIsGalois

L492 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodIsGalois
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
instance
    smallHilbertFiniteGaloisNormNeighborhoodIsGalois :
    IsGalois E E₂
theorem

smallHilbertFiniteGaloisNormNeighborhood_fixedField_eq_range

L501 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhood_fixedField_eq_range
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem
    smallHilbertFiniteGaloisNormNeighborhood_fixedField_eq_range :
    (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
      (smallHilbertFiniteGaloisNormNeighborhood K L).below).restrictScalars ℚ =
        AlgHom.fieldRange
          (smallHilbertNormNeighborhoodEmbedding K L)
def

smallHilbertFiniteGaloisNormNeighborhoodTopEquiv

L521 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodTopEquiv
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
def
    smallHilbertFiniteGaloisNormNeighborhoodTopEquiv :
    N ≃ₐ[ℚ]
      (abstractRelativeFixedField ℚ (SeparableClosure ℚ)
        (smallHilbertFiniteGaloisNormNeighborhood K L).below).restrictScalars ℚ
theorem

smallHilbertFiniteGaloisNormNeighborhoodTopEquiv_algebraMap

L532 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodTopEquiv_algebraMap
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem
    smallHilbertFiniteGaloisNormNeighborhoodTopEquiv_algebraMap
    (x : E) :
    smallHilbertFiniteGaloisNormNeighborhoodTopEquiv K L
        (algebraMap E N x) =
      algebraMap E
        E₂ x
def

smallHilbertFiniteGaloisNormNeighborhoodRelativeTopEquiv

L546 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhoodRelativeTopEquiv
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
def
    smallHilbertFiniteGaloisNormNeighborhoodRelativeTopEquiv :
    N ≃ₐ[E] E₂
theorem

smallHilbertFiniteGaloisNormNeighborhood_ordinaryNorm_le

L554 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhood_ordinaryNorm_le
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem
    smallHilbertFiniteGaloisNormNeighborhood_ordinaryNorm_le :
    (_root_.ideleClassNorm E N).range ≤
      smallHilbertClassFieldNormSubgroup (K := E)
theorem

smallHilbertFiniteGaloisNormNeighborhood_ordinaryNormRange_eq

L563 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhood_ordinaryNormRange_eq
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem
    smallHilbertFiniteGaloisNormNeighborhood_ordinaryNormRange_eq :
    (_root_.ideleClassNorm E N).range =
      (_root_.ideleClassNorm E E₂).range
theorem

smallHilbertFiniteGaloisNormNeighborhood_abstractNormMap_eq

L573 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhood_abstractNormMap_eq
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem
    smallHilbertFiniteGaloisNormNeighborhood_abstractNormMap_eq :
    ((smallHilbertFiniteGaloisNormNeighborhood K L).normSubgroup
        rationalIdeleClassRepresentation).map
          (rationalAbstractFixedFieldIdeleClassEquivFixed
            L.field
            (hfinite := smallHilbertTowerMiddleAbstractQuotientFinite K L)).symm.toAddMonoidHom =
      (_root_.ideleClassNorm E E₂).range.toAddSubgroup
theorem

smallHilbertFiniteGaloisNormNeighborhood_abstractNormMap_eq_ordinaryNormRange

L600 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhood_abstractNormMap_eq_ordinaryNormRange
Documentation

The abstract norm map lands directly in the ordinary norm range of the chosen neighbourhood. Composing the two named subgroup equalities here keeps downstream membership proofs pointwise.

Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem
    smallHilbertFiniteGaloisNormNeighborhood_abstractNormMap_eq_ordinaryNormRange :
    ((smallHilbertFiniteGaloisNormNeighborhood K L).normSubgroup
        rationalIdeleClassRepresentation).map
          (rationalAbstractFixedFieldIdeleClassEquivFixed
            L.field
            (hfinite := smallHilbertTowerMiddleAbstractQuotientFinite K L)).symm.toAddMonoidHom =
      (_root_.ideleClassNorm E N).range.toAddSubgroup
theorem

smallHilbertFiniteGaloisNormNeighborhood_abstractNormMap_mem_ordinaryNormRange

L613 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhood_abstractNormMap_mem_ordinaryNormRange
Documentation

Pointwise form of the combined norm-range equality.

Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem
    smallHilbertFiniteGaloisNormNeighborhood_abstractNormMap_mem_ordinaryNormRange
    (a : Additive (IdeleClassGroup E))
    (ha :
      a ∈ ((smallHilbertFiniteGaloisNormNeighborhood K L).normSubgroup
        rationalIdeleClassRepresentation).map
          (rationalAbstractFixedFieldIdeleClassEquivFixed
            L.field
            (hfinite := smallHilbertTowerMiddleAbstractQuotientFinite K L)).symm.toAddMonoidHom) :
    a ∈ (_root_.ideleClassNorm E N).range.toAddSubgroup
theorem

smallHilbertFiniteGaloisNormNeighborhood_normSubgroup_le

L631 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertFiniteGaloisNormNeighborhood_normSubgroup_le
Documentation

The actual finite Galois norm neighbourhood has abstract norm subgroup contained in the canonical small-Hilbert subgroup of the middle fixed field. This is the source-producing norm-topology input; no norm-openness premise is assumed.

Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem smallHilbertFiniteGaloisNormNeighborhood_normSubgroup_le :
    ∀ a : ambientFixedAddSubgroup
        rationalIdeleClassRepresentation L.field,
      a ∈ smallHilbertFiniteGaloisNormNeighborhoodNormSubgroup K L →
        a ∈ smallHilbertTowerMiddleNormSubgroup K L
theorem

smallHilbertNormSubgroupInRationalClassFormation_isNormOpen

L660 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertNormSubgroupInRationalClassFormation_isNormOpen
Documentation

The canonical small-Hilbert subgroup of the actual middle fixed field is open in the genuine norm topology.

Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem smallHilbertNormSubgroupInRationalClassFormation_isNormOpen :
    IsNormOpen rationalIdeleClassRepresentation L.field
      (smallHilbertTowerMiddleNormSubgroup K L :
        Set
          (ambientFixedAddSubgroup
            rationalIdeleClassRepresentation L.field))
def

secondSmallHilbertClassFieldSubextension

L676 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldSubextension
Documentation

The second small Hilbert class field as an actual finite abelian subextension of the literal first-stage field.

Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
def secondSmallHilbertClassFieldSubextension :
    FiniteAbelianSubextension L.field
theorem

secondSmallHilbertClassFieldSubextension_normSubgroup

L692 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldSubextension_normSubgroup
Documentation

The second-stage extension realizes exactly the canonical small-Hilbert norm subgroup of the actual middle field.

Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
theorem secondSmallHilbertClassFieldSubextension_normSubgroup :
    (secondSmallHilbertClassFieldSubextension K L).normSubgroup
        rationalIdeleClassRepresentation =
      smallHilbertTowerMiddleNormSubgroup K L
abbrev

secondSmallHilbertClassFieldTopField

L708 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldTopField
Source context 20 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
Lean source · statement
abbrev secondSmallHilbertClassFieldTopField : Type
instance

secondSmallHilbertClassFieldSubextensionQuotientFinite

L714 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldSubextensionQuotientFinite
Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
instance
    secondSmallHilbertClassFieldSubextensionQuotientFinite :
    Finite
      (L.field.toSubgroup ⧸
        extensionSubgroup L.field
          (secondSmallHilbertClassFieldSubextension K L).field
          (secondSmallHilbertClassFieldSubextension K L).below)
instance

secondSmallHilbertClassFieldTopFiniteDimensional

L723 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldTopFiniteDimensional
Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
instance
    secondSmallHilbertClassFieldTopFiniteDimensional :
    FiniteDimensional E T₂
instance

secondSmallHilbertClassFieldTopScalarTower

L732 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldTopScalarTower
Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
instance
    secondSmallHilbertClassFieldTopScalarTower :
    IsScalarTower ℚ E T₂
instance

secondSmallHilbertClassFieldTopAbsoluteFiniteDimensional

L737 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldTopAbsoluteFiniteDimensional
Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
instance
    secondSmallHilbertClassFieldTopAbsoluteFiniteDimensional :
    FiniteDimensional ℚ T₂
instance

secondSmallHilbertClassFieldTopNumberField

L742 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldTopNumberField
Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
instance
    secondSmallHilbertClassFieldTopNumberField :
    NumberField T₂
instance

secondSmallHilbertClassFieldTopIsGalois

L747 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldTopIsGalois
Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
instance
    secondSmallHilbertClassFieldTopIsGalois :
    IsGalois E T₂
theorem

secondSmallHilbertClassFieldSubextension_abstractNormMap_eq_actualNormRange

L756 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldSubextension_abstractNormMap_eq_actualNormRange
Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
theorem
    secondSmallHilbertClassFieldSubextension_abstractNormMap_eq_actualNormRange :
    ((secondSmallHilbertClassFieldSubextension K L).normSubgroup
        rationalIdeleClassRepresentation).map
          (rationalAbstractFixedFieldIdeleClassEquivFixed
            L.field
            (hfinite := smallHilbertTowerMiddleAbstractQuotientFinite K L)).symm.toAddMonoidHom =
      (_root_.ideleClassNorm E T₂).range.toAddSubgroup
theorem

secondSmallHilbertClassFieldSubextension_abstractNormMap_eq_smallHilbertNormSubgroup

L780 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldSubextension_abstractNormMap_eq_smallHilbertNormSubgroup
Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
theorem
    secondSmallHilbertClassFieldSubextension_abstractNormMap_eq_smallHilbertNormSubgroup :
    ((secondSmallHilbertClassFieldSubextension K L).normSubgroup
        rationalIdeleClassRepresentation).map
          (rationalAbstractFixedFieldIdeleClassEquivFixed
            L.field
            (hfinite := smallHilbertTowerMiddleAbstractQuotientFinite K L)).symm.toAddMonoidHom =
      (smallHilbertClassFieldNormSubgroup (K := E)).toAddSubgroup
theorem

secondSmallHilbertClassFieldSubextension_ideleClassNorm_range

L810 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.secondSmallHilbertClassFieldSubextension_ideleClassNorm_range
Documentation

The actual second small Hilbert class field has exactly the intrinsic small-Hilbert norm range over the literal middle fixed field.

Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
theorem secondSmallHilbertClassFieldSubextension_ideleClassNorm_range :
    (_root_.ideleClassNorm E T₂).range =
      smallHilbertClassFieldNormSubgroup (K := E)
theorem

smallHilbertTowerMiddleNormSubgroup_eq_conjugationEndpoint

L822 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerMiddleNormSubgroup_eq_conjugationEndpoint
Documentation

Compatibility of the typed middle endpoint with the canonical endpoint used by the conjugation API.

Source context 21 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section RationalFixedField
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field)
local notation "E" =>
  abstractFixedField ℚ (SeparableClosure ℚ) L.field
local notation "N" =>
  smallHilbertClassFieldNormAmbient E
attribute [local instance] smallHilbertTowerNormAmbientAlgebra
attribute [local instance] smallHilbertTowerNormAmbientIsGalois
local notation "E₂" =>
  smallHilbertFiniteGaloisNormNeighborhoodTopField K L
local notation "T₂" => secondSmallHilbertClassFieldTopField K L
Lean source · statement
theorem smallHilbertTowerMiddleNormSubgroup_eq_conjugationEndpoint :
    smallHilbertTowerMiddleNormSubgroup K L =
      smallHilbertNormSubgroupInRationalClassFormation
        (L.toFiniteGaloisExtension.toFiniteAbstractFieldExtension).field
def

smallHilbertTowerSecondSubextension

L842 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerSecondSubextension
Documentation

The actual second small Hilbert class field over the selected first small Hilbert class field of K.

Source context 15 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section ActualTower
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def smallHilbertTowerSecondSubextension :
    FiniteAbelianSubextension
      (smallHilbertClassFieldSubextension K).field
theorem

smallHilbertTowerSecondSubextension_normSubgroup

L852 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerSecondSubextension_normSubgroup
Documentation

Exact norm-subgroup equation for the actual second stage.

Source context 15 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section ActualTower
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
theorem smallHilbertTowerSecondSubextension_normSubgroup :
    (smallHilbertTowerSecondSubextension K).normSubgroup
        rationalIdeleClassRepresentation =
      smallHilbertTowerMiddleNormSubgroup
        (numberFieldTowerFiniteAbstractField K
          (smallHilbertClassFieldNormAmbient K))
        (smallHilbertClassFieldSubextension K)
def

smallHilbertTowerGaloisRealization

L866 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertTowerGaloisRealization
Documentation

The actual two-stage small Hilbert tower, packaged as a finite Galois subextension of the original selected base subgroup.

Source context 15 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open AlgebraicNumberTheory
open ClassFormation
open CyclicCohomology
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open RamificationTheory
open Reciprocity
attribute [local instance] smallHilbertTowerIdeleClassCommGroup
section ActualTower
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
def smallHilbertTowerGaloisRealization :
    FiniteGaloisSubextension
      (smallHilbertClassFieldBaseSubgroup K)

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