Module

SmallHilbertPrincipalization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.SmallHilbertPrincipalization

10 declarations indexed from sourceView source ↗

Module documentation

Principalization in the selected small Hilbert class field

The selected second small Hilbert class field is Galois over the canonical fixed-field copy of the original base, and its maximal abelian intermediate field is the selected first small Hilbert class field. Witt transfer therefore places every idele class extended from that fixed-field copy in the norm range from the second stage. Functoriality of actual idele extension along the degree-one identification of the original field with its fixed-field copy gives the same range inclusion for idele classes extended from the original field itself.

The exact second-stage norm subgroup is the intrinsic small-Hilbert subgroup, so the genuine map from the original field on small-Hilbert quotients is trivial. Its naturality with extension of ideal classes then gives the class-group, integral-ideal, and fractional-ideal forms of principalization over the original number field.

Imports3

Imported by2

instance

smallHilbertPrincipalization_ideleClassGroupIsMulCommutative

L46 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertPrincipalization_ideleClassGroupIsMulCommutative

Source context 9 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity

Lean source · statement

instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

instance

smallHilbertPrincipalization_ideleClassSubgroupNormal

L52 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertPrincipalization_ideleClassSubgroupNormal

Source context 10 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
local instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩

Lean source · statement

instance
    smallHilbertPrincipalization_ideleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal

instance

smallHilbertPrincipalization_smallHilbertQuotientGroup

L58 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertPrincipalization_smallHilbertQuotientGroup

Source context 11 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
local instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    smallHilbertPrincipalization_ideleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative

Lean source · statement

instance
    smallHilbertPrincipalization_smallHilbertQuotientGroup
    {F : Type} [Field F] [NumberField F] :
    Group
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F))

instance

smallHilbertPrincipalization_smallHilbertQuotientOne

L67 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertPrincipalization_smallHilbertQuotientOne

Source context 12 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
local instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    smallHilbertPrincipalization_ideleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
local instance
    smallHilbertPrincipalization_smallHilbertQuotientGroup
    {F : Type} [Field F] [NumberField F] :
    Group
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  QuotientGroup.Quotient.group
    (smallHilbertClassFieldNormSubgroup (K := F))

Lean source · statement

instance
    smallHilbertPrincipalization_smallHilbertQuotientOne
    {F : Type} [Field F] [NumberField F] :
    One
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F))

theorem

smallHilbertClassFieldIdeleExtensionMap_apply_eq_one

L78 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldIdeleExtensionMap_apply_eq_one

Source context 14 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
local instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    smallHilbertPrincipalization_ideleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
local instance
    smallHilbertPrincipalization_smallHilbertQuotientGroup
    {F : Type} [Field F] [NumberField F] :
    Group
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  QuotientGroup.Quotient.group
    (smallHilbertClassFieldNormSubgroup (K := F))
local instance
    smallHilbertPrincipalization_smallHilbertQuotientOne
    {F : Type} [Field F] [NumberField F] :
    One
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  ⟨(smallHilbertPrincipalization_smallHilbertQuotientGroup
    (F := F)).one⟩
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassFieldIdeleExtensionMap_apply_eq_one
    (q : IdeleClassGroup K ⧸
      smallHilbertClassFieldNormSubgroup (K := K)) :
    smallHilbertClassFieldIdeleExtensionMap
        K (smallHilbertClassField K) q =
      (1 : IdeleClassGroup (smallHilbertClassField K) ⧸
        smallHilbertClassFieldNormSubgroup
          (K := smallHilbertClassField K))

theorem

smallHilbertClassFieldIdeleExtensionMap_eq_one

L121 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldIdeleExtensionMap_eq_one

Documentation

The map induced by genuine idele extension from the original number field on the two small-Hilbert reciprocity quotients is trivial.

Source context 14 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
local instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    smallHilbertPrincipalization_ideleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
local instance
    smallHilbertPrincipalization_smallHilbertQuotientGroup
    {F : Type} [Field F] [NumberField F] :
    Group
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  QuotientGroup.Quotient.group
    (smallHilbertClassFieldNormSubgroup (K := F))
local instance
    smallHilbertPrincipalization_smallHilbertQuotientOne
    {F : Type} [Field F] [NumberField F] :
    One
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  ⟨(smallHilbertPrincipalization_smallHilbertQuotientGroup
    (F := F)).one⟩
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassFieldIdeleExtensionMap_eq_one :
    @Eq
      ((IdeleClassGroup K ⧸
          smallHilbertClassFieldNormSubgroup (K := K)) →*
        (IdeleClassGroup (smallHilbertClassField K) ⧸
          smallHilbertClassFieldNormSubgroup
            (K := smallHilbertClassField K)))
      (smallHilbertClassFieldIdeleExtensionMap
        K (smallHilbertClassField K))
      (1 :
        (IdeleClassGroup K ⧸
          smallHilbertClassFieldNormSubgroup (K := K)) →*
        (IdeleClassGroup (smallHilbertClassField K) ⧸
          smallHilbertClassFieldNormSubgroup
            (K := smallHilbertClassField K)))

theorem

smallHilbertClassFieldClassGroupExtension_apply_eq_one

L141 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldClassGroupExtension_apply_eq_one

Source context 14 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
local instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    smallHilbertPrincipalization_ideleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
local instance
    smallHilbertPrincipalization_smallHilbertQuotientGroup
    {F : Type} [Field F] [NumberField F] :
    Group
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  QuotientGroup.Quotient.group
    (smallHilbertClassFieldNormSubgroup (K := F))
local instance
    smallHilbertPrincipalization_smallHilbertQuotientOne
    {F : Type} [Field F] [NumberField F] :
    One
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  ⟨(smallHilbertPrincipalization_smallHilbertQuotientGroup
    (F := F)).one⟩
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassFieldClassGroupExtension_apply_eq_one
    (c : ClassGroup (𝓞 K)) :
    ClassGroup.extendedHom
        (𝓞 K) (𝓞 (smallHilbertClassField K)) c =
      (1 : ClassGroup (𝓞 (smallHilbertClassField K)))

theorem

smallHilbertClassFieldClassGroupExtension_eq_one

L176 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldClassGroupExtension_eq_one

Documentation

Extension of ideal classes from a number field to its selected small Hilbert class field is the trivial homomorphism. This follows directly from the naturality equality identifying actual idele extension with actual extension of ideal classes.

Source context 14 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
local instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    smallHilbertPrincipalization_ideleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
local instance
    smallHilbertPrincipalization_smallHilbertQuotientGroup
    {F : Type} [Field F] [NumberField F] :
    Group
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  QuotientGroup.Quotient.group
    (smallHilbertClassFieldNormSubgroup (K := F))
local instance
    smallHilbertPrincipalization_smallHilbertQuotientOne
    {F : Type} [Field F] [NumberField F] :
    One
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  ⟨(smallHilbertPrincipalization_smallHilbertQuotientGroup
    (F := F)).one⟩
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem smallHilbertClassFieldClassGroupExtension_eq_one :
    @Eq
      (ClassGroup (𝓞 K) →*
        ClassGroup (𝓞 (smallHilbertClassField K)))
      (ClassGroup.extendedHom
        (𝓞 K) (𝓞 (smallHilbertClassField K)))
      (1 : ClassGroup (𝓞 K) →*
        ClassGroup (𝓞 (smallHilbertClassField K)))

theorem

allIdealsBecomePrincipalInSmallHilbertClassField

L191 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.allIdealsBecomePrincipalInSmallHilbertClassField

Documentation

Every ideal of a number field becomes principal after extension to the selected small Hilbert class field.

Source context 14 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
local instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    smallHilbertPrincipalization_ideleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
local instance
    smallHilbertPrincipalization_smallHilbertQuotientGroup
    {F : Type} [Field F] [NumberField F] :
    Group
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  QuotientGroup.Quotient.group
    (smallHilbertClassFieldNormSubgroup (K := F))
local instance
    smallHilbertPrincipalization_smallHilbertQuotientOne
    {F : Type} [Field F] [NumberField F] :
    One
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  ⟨(smallHilbertPrincipalization_smallHilbertQuotientGroup
    (F := F)).one⟩
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem allIdealsBecomePrincipalInSmallHilbertClassField :
    ∀ I : Ideal (𝓞 K),
      (I.map
        (algebraMap
          (𝓞 K)
          (𝓞 (smallHilbertClassField K)))).IsPrincipal

theorem

allFractionalIdealsBecomePrincipalInSmallHilbertClassField

L204 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.allFractionalIdealsBecomePrincipalInSmallHilbertClassField

Documentation

Every nonzero fractional ideal of a number field becomes a principal fractional ideal after extension to the selected small Hilbert class field.

Source context 14 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
local instance
    smallHilbertPrincipalization_ideleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    smallHilbertPrincipalization_ideleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
local instance
    smallHilbertPrincipalization_smallHilbertQuotientGroup
    {F : Type} [Field F] [NumberField F] :
    Group
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  QuotientGroup.Quotient.group
    (smallHilbertClassFieldNormSubgroup (K := F))
local instance
    smallHilbertPrincipalization_smallHilbertQuotientOne
    {F : Type} [Field F] [NumberField F] :
    One
      (IdeleClassGroup F ⧸
        smallHilbertClassFieldNormSubgroup (K := F)) :=
  ⟨(smallHilbertPrincipalization_smallHilbertQuotientGroup
    (F := F)).one⟩
variable (K : Type) [Field K] [NumberField K]

Lean source · statement

theorem allFractionalIdealsBecomePrincipalInSmallHilbertClassField :
    ∀ I : FractionalIdealGroup K,
      FractionalIdealGroup.extension
          K (smallHilbertClassField K) I ∈
        (toPrincipalIdeal
          (𝓞 (smallHilbertClassField K))
          (smallHilbertClassField K)).range

Module documentation

Principalization in the selected small Hilbert class field

Declarations