NYLL
Module

PrincipalIdealTransfer.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.PrincipalIdealTransfer
18 declarations indexed from sourceView source ↗

Module documentation

Transfer input for the principal ideal theorem

At the generic level, the Galois correspondence realizes a subgroup S ≤ Gal(M / K) as an intermediate field, while the transfer construction independently realizes Gal(M / M^S) inside Gal(M / K). Identifying these subgroups puts the commutator transfer in the form covered by Witt's theorem. This generic input assumes neither a class-field realization nor a norm-subgroup equality.

The theorems below specialize that input to the selected actual two-stage small Hilbert tower and transport it to genuine idèle-class extension and norm maps.

Imports10
Imported by2

Declarations

instance

principalIdealTransferIdeleClassGroupIsMulCommutative

L50 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.principalIdealTransferIdeleClassGroupIsMulCommutative
Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
Lean source · statement
instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
instance

principalIdealTransferIdeleClassSubgroupNormal

L56 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.principalIdealTransferIdeleClassSubgroupNormal
Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
Lean source · statement
instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal
theorem

ideleClassExtension_range_le_of_intermediate

L64 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.ideleClassExtension_range_le_of_intermediate
Documentation

Extension-range containment descends along the lower leg of a finite Galois tower.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
theorem ideleClassExtension_range_le_of_intermediate
    (F E U : Type)
    [Field F] [NumberField F]
    [Field E] [NumberField E]
    [Field U] [NumberField U]
    [Algebra F U] [FiniteDimensional F U] [IsGalois F U]
    [Algebra F E] [Algebra E U] [IsScalarTower F E U]
    [FiniteDimensional F E] [FiniteDimensional E U]
    [IsGalois F E] [IsGalois E U]
    (N : Subgroup (IdeleClassGroup U))
    (hcontainment : (ideleClassExtension E U).range ≤ N) :
    (ideleClassExtension F U).range ≤ N
theorem

rationalFiniteNormTransferCanonicalMembership_to_explicitNormMembership

L87 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalMembership_to_explicitNormMembership
Documentation

Internal bridge from the opaque rational transfer endpoint to the explicit relative norm range used by the selected tower.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · full declaration
theorem
    rationalFiniteNormTransferCanonicalMembership_to_explicitNormMembership
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hHKnormal : (CyclicCohomology.extensionSubgroup K H hHK).Normal)
    (hLHnormal : (CyclicCohomology.extensionSubgroup H L hLH).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hKHfinite : Finite
      (K.toSubgroup ⧸ CyclicCohomology.extensionSubgroup K H hHK)]
    [hHfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H (le_baseField H))]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ CyclicCohomology.extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K)
    (hmembership :
      rationalFiniteNormTransferCanonicalOrdinaryExtensionNormMembership
        K H L hHK hLH hHKnormal hLHnormal c) :
    let F := abstractFixedField ℚ (SeparableClosure ℚ) K
    let E := abstractRelativeFixedField ℚ (SeparableClosure ℚ) hHK
    let U := abstractRelativeFixedField ℚ (SeparableClosure ℚ) hLH
    letI : FiniteDimensional ℚ F :=
      RationalFiniteNormTransferInternal.fixedFiniteDimensional
        (hKfinite := hKfinite) K
    letI : FiniteDimensional F E :=
      RationalFiniteNormTransferInternal.relativeFiniteDimensional
        (hKfinite := hKfinite) (hfinite := hKHfinite)
        K H hHK
    letI : IsScalarTower ℚ F E :=
      RationalFiniteNormTransferInternal.relativeScalarTower K H hHK
    letI : FiniteDimensional ℚ E :=
      RationalFiniteNormTransferInternal.relativeAbsoluteFiniteDimensional
        (hKfinite := hKfinite) (hfinite := hKHfinite)
        K H hHK
    letI : NumberField F :=
      RationalFiniteNormTransferInternal.fixedNumberField
        (hKfinite := hKfinite) K
    letI : NumberField E :=
      RationalFiniteNormTransferInternal.relativeNumberField
        (hKfinite := hKfinite) (hfinite := hKHfinite)
        K H hHK
    letI : FiniteDimensional ℚ U :=
      RationalFiniteNormTransferInternal.relativeAbsoluteFiniteDimensional
        (hKfinite := hHfinite) (hfinite := hHLfinite)
        H L hLH
    letI : NumberField U :=
      RationalFiniteNormTransferInternal.relativeNumberField
        (hKfinite := hHfinite) (hfinite := hHLfinite)
        H L hLH
    letI : Algebra E U := by
      change Algebra
        (abstractFixedField ℚ (SeparableClosure ℚ) H) U
      exact U.algebra
    letI : Module E U := by
      change Module
        (abstractFixedField ℚ (SeparableClosure ℚ) H) U
      exact
        (U.algebra : Algebra
          (abstractFixedField ℚ (SeparableClosure ℚ) H) U).toModule
    letI : FiniteDimensional E U := by
      change FiniteDimensional
        (abstractFixedField ℚ (SeparableClosure ℚ) H) U
      exact RationalFiniteNormTransferInternal.relativeFiniteDimensional
        (hKfinite := hHfinite) (hfinite := hHLfinite)
        H L hLH
    letI : IsScalarTower ℚ E U := by
      change IsScalarTower ℚ
        (abstractFixedField ℚ (SeparableClosure ℚ) H) U
      exact RationalFiniteNormTransferInternal.relativeScalarTower H L hLH
    letI : IsGalois F E :=
      RationalFiniteNormTransferInternal.relativeIsGalois
        K H hHK hHKnormal
    letI : IsGalois E U := by
      change IsGalois
        (abstractFixedField ℚ (SeparableClosure ℚ) H) U
      exact RationalFiniteNormTransferInternal.relativeIsGalois
        H L hLH hLHnormal
    ideleClassExtension F E c ∈ (_root_.ideleClassNorm E U).range := by
  dsimp only
  unfold
    rationalFiniteNormTransferCanonicalOrdinaryExtensionNormMembership
    at hmembership
  unfold rationalFiniteNormTransferRelativeNormMembership at hmembership
  unfold
    rationalFiniteNormTransferOrdinaryExtensionRepresentative
    at hmembership
  exact hmembership
theorem

rationalFiniteNormTransferCanonicalFiniteNormClassZero_of_commutator

L190 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalFiniteNormClassZero_of_commutator
Documentation

The commutator transfer supplies the canonical zero class used by the rational finite-norm bridge.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
theorem
    rationalFiniteNormTransferCanonicalFiniteNormClassZero_of_commutator
    (K₀ : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (M : FiniteGaloisSubextension K₀.field)
    (H T : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hTH : T.toSubgroup ≤ H.toSubgroup)
    (hHK : H.toSubgroup ≤ K₀.field.toSubgroup)
    (hmiddle : M.intermediateField (commutator M.extensionQuotient) = H)
    (htop : M.field = T)
    [hHTfinite : Finite
      (H.toSubgroup ⧸ CyclicCohomology.extensionSubgroup H T hTH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := K₀.finite) K₀.field) :
    rationalFiniteNormTransferCanonicalFiniteNormClassZero
      (hKfinite := K₀.finite) (hHLfinite := hHTfinite)
      K₀.field H T hHK hTH c
def

smallHilbertClassFieldCanonicalFiniteNormClassZeroStatement

L270 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldCanonicalFiniteNormClassZeroStatement
Documentation

The selected two-stage tower supplies a canonical zero finite-norm class for every idele class over its base fixed field.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
def
    smallHilbertClassFieldCanonicalFiniteNormClassZeroStatement : Prop
theorem

smallHilbertClassFieldCanonicalFiniteNormClassZeroStatement_proof

L290 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldCanonicalFiniteNormClassZeroStatement_proof
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
theorem
    smallHilbertClassFieldCanonicalFiniteNormClassZeroStatement_proof :
    smallHilbertClassFieldCanonicalFiniteNormClassZeroStatement K
def

smallHilbertClassFieldCanonicalNormMembershipStatement

L331 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldCanonicalNormMembershipStatement
Documentation

The canonical zero classes of the selected tower satisfy the opaque rational relative norm-membership endpoint.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
def
    smallHilbertClassFieldCanonicalNormMembershipStatement : Prop
theorem

smallHilbertClassFieldCanonicalNormMembershipStatement_proof

L362 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldCanonicalNormMembershipStatement_proof
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
theorem
    smallHilbertClassFieldCanonicalNormMembershipStatement_proof :
    smallHilbertClassFieldCanonicalNormMembershipStatement K
abbrev

smallHilbertClassFieldExplicitNormMembershipStatement

L414 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldExplicitNormMembershipStatement
Documentation

The selected rational transfer endpoint, exposed on the explicit relative fixed-field spine used by the tower containment.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
abbrev
    smallHilbertClassFieldExplicitNormMembershipStatement : Prop
structure

SmallHilbertClassFieldExplicitNormMembershipData

L511 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.SmallHilbertClassFieldExplicitNormMembershipData
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · full declaration
structure SmallHilbertClassFieldExplicitNormMembershipData
    (K : Type) [Field K] [NumberField K] : Type where
  membership : smallHilbertClassFieldExplicitNormMembershipStatement K
def

smallHilbertClassFieldExplicitNormMembershipData_proof

L515 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldExplicitNormMembershipData_proof
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · full declaration
def
    smallHilbertClassFieldExplicitNormMembershipData_proof :
    SmallHilbertClassFieldExplicitNormMembershipData K where
  membership := by
    unfold smallHilbertClassFieldExplicitNormMembershipStatement
    dsimp only
    intro c
    let K₀ :=
      numberFieldTowerFiniteAbstractField K
        (smallHilbertClassFieldNormAmbient K)
    let L := smallHilbertClassFieldSubextension K
    let N := smallHilbertTowerSecondSubextension K
    let H := L.field
    let hMH : N.field.toSubgroup ≤ H.toSubgroup := N.below
    let hHK : H.toSubgroup ≤ K₀.field.toSubgroup := L.below
    let hHKnormal :
        (CyclicCohomology.extensionSubgroup K₀.field H hHK).Normal :=
      L.normal
    let hMHnormal :
        (CyclicCohomology.extensionSubgroup H N.field hMH).Normal :=
      N.normal
    let hKHfinite : Finite
        (K₀.field.toSubgroup ⧸
          CyclicCohomology.extensionSubgroup K₀.field H hHK) :=
      L.finite
    let hHMfinite : Finite
        (H.toSubgroup ⧸
          CyclicCohomology.extensionSubgroup H N.field hMH) :=
      N.finite
    let hHfinite : Finite
        ((baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
          CyclicCohomology.extensionSubgroup
            (baseField
              (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
            H (le_baseField H)) :=
      FiniteGaloisSubextension.finite_extension_trans
        hHK (le_baseField K₀.field)
    have hmembershipAll :=
      smallHilbertClassFieldCanonicalNormMembershipStatement_proof K
    unfold
      smallHilbertClassFieldCanonicalNormMembershipStatement
      at hmembershipAll
    have hmembership :
        rationalFiniteNormTransferCanonicalOrdinaryExtensionNormMembership
          (hKfinite := K₀.finite) (hKHfinite := hKHfinite)
          (hHLfinite := hHMfinite)
          K₀.field H N.field hHK hMH hHKnormal hMHnormal c :=
      hmembershipAll c
    exact
      rationalFiniteNormTransferCanonicalMembership_to_explicitNormMembership
        (hKfinite := K₀.finite) (hKHfinite := hKHfinite)
        (hHfinite := hHfinite) (hHLfinite := hHMfinite)
        K₀.field H N.field hHK hMH hHKnormal hMHnormal c hmembership
def

smallHilbertClassFieldBaseSecondNormRangeContainment

L575 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldBaseSecondNormRangeContainment
Documentation

The named proposition underlying the fixed-field-base form of the two-stage transfer containment. Keeping the dependent idele maps behind one opaque boundary prevents every consumer from reconstructing their instance towers while elaborating a theorem signature.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
def smallHilbertClassFieldBaseSecondNormRangeContainment : Prop
theorem

smallHilbertClassFieldBase_ideleClassExtension_range_le_secondNormRange

L585 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldBase_ideleClassExtension_range_le_secondNormRange
Documentation

Witt transfer for the genuine selected two-stage tower: every idele class extended from the selected base fixed field to the first small Hilbert class field is a norm from the actual second stage.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
theorem
    smallHilbertClassFieldBase_ideleClassExtension_range_le_secondNormRange :
    smallHilbertClassFieldBaseSecondNormRangeContainment K
def

smallHilbertClassFieldSecondNormRangeContainment

L614 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldSecondNormRangeContainment
Documentation

The named proposition underlying the original-base form of the two-stage transfer containment.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
def smallHilbertClassFieldSecondNormRangeContainment : Prop
structure

SmallHilbertClassFieldSecondNormRangeContainmentData

L619 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.SmallHilbertClassFieldSecondNormRangeContainmentData
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · full declaration
structure SmallHilbertClassFieldSecondNormRangeContainmentData
    (K : Type) [Field K] [NumberField K] : Type where
  containment : smallHilbertClassFieldSecondNormRangeContainment K
def

smallHilbertClassFieldSecondNormRangeContainmentData_proof

L623 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassFieldSecondNormRangeContainmentData_proof
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · full declaration
def
    smallHilbertClassFieldSecondNormRangeContainmentData_proof :
    SmallHilbertClassFieldSecondNormRangeContainmentData K where
  containment := by
    unfold smallHilbertClassFieldSecondNormRangeContainment
    let : IsGalois K (smallHilbertClassFieldBase K) :=
      IsGalois.of_algEquiv
        (smallHilbertClassFieldBaseEquivOverOriginal K)
    have hbase :=
      smallHilbertClassFieldBase_ideleClassExtension_range_le_secondNormRange K
    unfold smallHilbertClassFieldBaseSecondNormRangeContainment at hbase
    exact
      ideleClassExtension_range_le_of_intermediate
        K (smallHilbertClassFieldBase K) (smallHilbertClassField K)
        (smallHilbertClassFieldNormSubgroup
          (K := smallHilbertClassField K)) hbase
theorem

smallHilbertClassField_ideleClassExtension_range_le_secondNormRange

L644 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.smallHilbertClassField_ideleClassExtension_range_le_secondNormRange
Documentation

Every idele class extended from the original number field to its selected small Hilbert class field is a norm from the actual second stage. This is the original-base form of the middle vertical arrow in the principal-ideal-theorem diagram.

Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open GlobalClassFields
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
variable (K : Type) [Field K] [NumberField K]
local instance
    principalIdealTransferIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  ⟨⟨fun a b => mul_comm a b⟩⟩
local instance
    principalIdealTransferIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  N.normal_of_isMulCommutative
Lean source · statement
theorem
    smallHilbertClassField_ideleClassExtension_range_le_secondNormRange :
    smallHilbertClassFieldSecondNormRangeContainment K

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