NYLL
Module

SmallHilbertClassFieldMaximalSubextension.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.SmallHilbertClassFieldMaximalSubextension
18 declarations indexed from sourceView source ↗

Module documentation

The maximal everywhere-unramified abelian subextension

The selected small Hilbert class field is characterized in actual field order. Its rational absolute class-formation norm subgroup is exactly the intrinsic small-Hilbert subgroup of its fixed-field base. The order-reversing finite abelian classification then places every actual finite abelian extension unramified at all finite and infinite places inside the selected field.

Imports3
Imported by4

Declarations

def

smallHilbertMaximalSubextensionIdeleClassCommGroup

L37 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertMaximalSubextensionIdeleClassCommGroup
Documentation

Fix the canonical quotient structure at the boundary between ordinary idele classes and additive fixed subgroups.

Source context 6 commands

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

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

SmallHilbertTransportedAddSubgroupData

L44 ↗
GlobalClassFieldTheory.GlobalClassFields.SmallHilbertTransportedAddSubgroupData
Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · full declaration
structure SmallHilbertTransportedAddSubgroupData
    {A B : Type} [AddGroup A] [AddGroup B]
    (e : A ≃+ B) (H : AddSubgroup A) where
  subgroup : AddSubgroup B
  map_symm : subgroup.map e.symm.toAddMonoidHom = H
def

smallHilbertTransportedAddSubgroupData

L50 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertTransportedAddSubgroupData
Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · full declaration
def smallHilbertTransportedAddSubgroupData
    {A B : Type} [AddGroup A] [AddGroup B]
    (e : A ≃+ B) (H : AddSubgroup A) :
    SmallHilbertTransportedAddSubgroupData e H where
  subgroup := H.map e.toAddMonoidHom
  map_symm :=
    (AddSubgroup.map_symm_eq_iff_map_eq
      (K := H) (H := H.map e.toAddMonoidHom) (e := e)).2 rfl
theorem

smallHilbertAddSubgroup_eq_of_map_symm_eq

L59 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertAddSubgroup_eq_of_map_symm_eq
Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem smallHilbertAddSubgroup_eq_of_map_symm_eq
    {A B : Type} [AddGroup A] [AddGroup B]
    (e : A ≃+ B) (H J : AddSubgroup B)
    (h : H.map e.symm.toAddMonoidHom =
      J.map e.symm.toAddMonoidHom) :
    H = J
def

smallHilbertClassFieldMaximalIdeleClassEquiv

L69 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldMaximalIdeleClassEquiv
Documentation

The fixed-field idèle-class equivalence at the selected small-Hilbert base, named once so later subgroup comparisons do not reconstruct it.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
def smallHilbertClassFieldMaximalIdeleClassEquiv
    (K : Type) [Field K] [NumberField K] :
    Additive (IdeleClassGroup (smallHilbertClassFieldBase K)) ≃+
      ambientFixedAddSubgroup rationalIdeleClassRepresentation
        (smallHilbertClassFieldBaseSubgroup K)
def

smallHilbertClassFieldMaximalIntrinsicNormSubgroup

L79 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldMaximalIntrinsicNormSubgroup
Documentation

The intrinsic ordinary norm subgroup at the selected base, with its additive carrier fixed in the declaration type.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
def smallHilbertClassFieldMaximalIntrinsicNormSubgroup
    (K : Type) [Field K] [NumberField K] :
    AddSubgroup (Additive (IdeleClassGroup (smallHilbertClassFieldBase K)))
def

smallHilbertClassFieldMaximalTransportData

L85 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldMaximalTransportData
Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
def smallHilbertClassFieldMaximalTransportData
    (K : Type) [Field K] [NumberField K] :
    SmallHilbertTransportedAddSubgroupData
      (smallHilbertClassFieldMaximalIdeleClassEquiv K)
      (smallHilbertClassFieldMaximalIntrinsicNormSubgroup K)
def

smallHilbertClassFieldMaximalNormEndpoint

L97 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldMaximalNormEndpoint
Documentation

A short typed name for the transported intrinsic subgroup used below. Keeping this endpoint opaque prevents the fixed-field aliases from being re-elaborated when the inverse transport is applied.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
def smallHilbertClassFieldMaximalNormEndpoint
    (K : Type) [Field K] [NumberField K] :
    AddSubgroup
      (ambientFixedAddSubgroup rationalIdeleClassRepresentation
        (smallHilbertClassFieldBaseSubgroup K))
theorem

smallHilbertClassFieldMaximalNormEndpoint_map_symm

L104 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldMaximalNormEndpoint_map_symm
Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem smallHilbertClassFieldMaximalNormEndpoint_map_symm
    (K : Type) [Field K] [NumberField K] :
    (smallHilbertClassFieldMaximalNormEndpoint K).map
        (smallHilbertClassFieldMaximalIdeleClassEquiv K).symm.toAddMonoidHom =
      smallHilbertClassFieldMaximalIntrinsicNormSubgroup K
theorem

smallHilbertClassFieldMaximalNormEndpoint_eq_public

L111 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldMaximalNormEndpoint_eq_public
Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem smallHilbertClassFieldMaximalNormEndpoint_eq_public
    (K : Type) [Field K] [NumberField K] :
    smallHilbertClassFieldMaximalNormEndpoint K =
      smallHilbertNormSubgroupInRationalClassFormation
        (numberFieldTowerFiniteAbstractField K
          (smallHilbertClassFieldNormAmbient K))
theorem

smallHilbertClassFieldMaximalNormSubgroup_map_symm

L121 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldMaximalNormSubgroup_map_symm
Documentation

Mapping the selected abstract norm subgroup back to the ordinary idèle-class group gives the named intrinsic subgroup.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem smallHilbertClassFieldMaximalNormSubgroup_map_symm
    (K : Type) [Field K] [NumberField K] :
    ((smallHilbertClassFieldSubextension K).normSubgroup
        rationalIdeleClassRepresentation).map
      (smallHilbertClassFieldMaximalIdeleClassEquiv K).symm.toAddMonoidHom =
        smallHilbertClassFieldMaximalIntrinsicNormSubgroup K
theorem

smallHilbertClassFieldMaximalNormSubgroup_map_eq_endpoint_map

L168 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldMaximalNormSubgroup_map_eq_endpoint_map
Documentation

Both subgroups have the same inverse image under the fixed-field idèle-class equivalence.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem smallHilbertClassFieldMaximalNormSubgroup_map_eq_endpoint_map
    (K : Type) [Field K] [NumberField K] :
    ((smallHilbertClassFieldSubextension K).normSubgroup
        rationalIdeleClassRepresentation).map
      (smallHilbertClassFieldMaximalIdeleClassEquiv K).symm.toAddMonoidHom =
      (smallHilbertClassFieldMaximalNormEndpoint K).map
        (smallHilbertClassFieldMaximalIdeleClassEquiv K).symm.toAddMonoidHom
theorem

smallHilbertClassFieldMaximalNormSubgroup_eq_endpoint

L185 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldMaximalNormSubgroup_eq_endpoint
Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem smallHilbertClassFieldMaximalNormSubgroup_eq_endpoint
    (K : Type) [Field K] [NumberField K] :
    (smallHilbertClassFieldSubextension K).normSubgroup
        rationalIdeleClassRepresentation =
      smallHilbertClassFieldMaximalNormEndpoint K
theorem

smallHilbertClassFieldSubextension_normSubgroup

L205 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldSubextension_normSubgroup
Documentation

The selected small Hilbert class-field subextension realizes exactly the intrinsic small-Hilbert norm subgroup in the rational absolute class formation.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem smallHilbertClassFieldSubextension_normSubgroup
    (K : Type) [Field K] [NumberField K] :
    (smallHilbertClassFieldSubextension K).normSubgroup
        rationalIdeleClassRepresentation =
      smallHilbertNormSubgroupInRationalClassFormation
        (numberFieldTowerFiniteAbstractField K
          (smallHilbertClassFieldNormAmbient K))
def

finiteAbelianSubextensionIsEverywhereUnramified

L227 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteAbelianSubextensionIsEverywhereUnramified
Documentation

The actual fixed-field extension represented by a finite abelian subextension of the selected rational base is everywhere unramified.

Naming this predicate keeps the fixed-field instance tower out of the signatures of every theorem which uses it.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
def finiteAbelianSubextensionIsEverywhereUnramified
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (smallHilbertClassFieldBaseSubgroup K)) : Prop
theorem

everywhereUnramifiedAbelianSubextension_le_smallHilbertClassFieldSubextension

L263 ↗
GlobalClassFieldTheory.GlobalClassFields.everywhereUnramifiedAbelianSubextension_le_smallHilbertClassFieldSubextension
Documentation

Every finite abelian subextension of the selected rational fixed-field base which is unramified at every finite and infinite place is contained in the selected small Hilbert class-field subextension.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem
    everywhereUnramifiedAbelianSubextension_le_smallHilbertClassFieldSubextension
    (K : Type) [Field K] [NumberField K]
    (P : FiniteAbelianSubextension
      (smallHilbertClassFieldBaseSubgroup K)) :
    finiteAbelianSubextensionIsEverywhereUnramified K P →
      P ≤ smallHilbertClassFieldSubextension K
theorem

smallHilbertClassFieldSubextension_isEverywhereUnramifiedAndMaximalAbelian

L312 ↗
GlobalClassFieldTheory.GlobalClassFields.smallHilbertClassFieldSubextension_isEverywhereUnramifiedAndMaximalAbelian
Documentation

The selected small Hilbert class field is genuinely everywhere unramified, and its finite abelian subextension is maximal among all actual everywhere-unramified abelian subextensions of the same rational fixed-field base.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem
    smallHilbertClassFieldSubextension_isEverywhereUnramifiedAndMaximalAbelian
    (K : Type) [Field K] [NumberField K] :
    IsEverywhereUnramified K (smallHilbertClassField K) ∧
      ∀ P : FiniteAbelianSubextension
          (smallHilbertClassFieldBaseSubgroup K),
        finiteAbelianSubextensionIsEverywhereUnramified K P →
          P ≤ smallHilbertClassFieldSubextension K
theorem

finiteAbelianExtension_nonempty_algHom_to_smallHilbertClassField_of_everywhereUnramified

L330 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteAbelianExtension_nonempty_algHom_to_smallHilbertClassField_of_everywhereUnramified
Documentation

Every finite abelian extension of K which is unramified at all finite and infinite places has a genuine K-embedding into the selected small Hilbert class field of K.

Source context 7 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation KummerTheory
open IdealClassFieldTheory LocalClassFieldTheory NumberField Reciprocity
attribute [local instance] smallHilbertMaximalSubextensionIdeleClassCommGroup
Lean source · statement
theorem
    finiteAbelianExtension_nonempty_algHom_to_smallHilbertClassField_of_everywhereUnramified
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L]
    [IsAbelianGalois K L]
    [IsUnramifiedAtInfinitePlaces K L]
    (hunramifiedFinite :
      _root_.ramifiedBaseFinitePlaces
          (K := K) (L := L) = ∅) :
    Nonempty (L →ₐ[K] smallHilbertClassField K)

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