NYLL
Module

NormLimitation.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.NormLimitation
5 declarations indexed from sourceView source ↗

Module documentation

The norm limitation theorem

For an arbitrary finite extension L / K, let N be its chosen finite normal closure, let E be the distinguished copy of L in N, and let A be the largest abelian Galois intermediate field contained in E. This file proves

N_{L/K} C_L = N_{A/K} C_A.

The proof applies finite reciprocity over N / K to E and A. Their Artin preimages agree because the fixing subgroup of A is obtained from the fixing subgroup of E by adjoining the commutator subgroup, which is killed by abelianization. The final step transports the norm range from the distinguished copy E back to the original field L.

Imports3
Imported by2

Declarations

theorem

finiteNormalClosureMaximalAbelianSubfield_fixingSubgroup_image_eq_originalFixingSubgroup_image

L45 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteNormalClosureMaximalAbelianSubfield_fixingSubgroup_image_eq_originalFixingSubgroup_image
Documentation

The fixing subgroup of the maximal abelian subfield and the fixing subgroup of the original field copy have the same image in the abelianization of the normal-closure Galois group.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
variable
    (K : Type) (L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem
    finiteNormalClosureMaximalAbelianSubfield_fixingSubgroup_image_eq_originalFixingSubgroup_image :
    (finiteNormalClosureMaximalAbelianSubfield K L).fixingSubgroup.map
        (Abelianization.of :
          Gal(finiteNormalClosure K L / K) →*
            Abelianization Gal(finiteNormalClosure K L / K)) =
      (finiteNormalClosureOriginalFixingSubgroup K L).map
        (Abelianization.of :
          Gal(finiteNormalClosure K L / K) →*
            Abelianization Gal(finiteNormalClosure K L / K))
theorem

finiteNormalClosureOriginalField_ideleClassNorm_range_eq_maximalAbelianSubfield

L75 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteNormalClosureOriginalField_ideleClassNorm_range_eq_maximalAbelianSubfield
Documentation

The distinguished original field copy and its maximal abelian subfield have the same idèle-class norm subgroup.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
variable
    (K : Type) (L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem
    finiteNormalClosureOriginalField_ideleClassNorm_range_eq_maximalAbelianSubfield :
    (_root_.ideleClassNorm K
        (finiteNormalClosureOriginalField K L)).range =
      (_root_.ideleClassNorm K
        (finiteNormalClosureMaximalAbelianSubfield K L)).range
theorem

ideleClassNorm_range_eq_maximalAbelianSubfield

L120 ↗
GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_range_eq_maximalAbelianSubfield
Documentation

Norm limitation: an arbitrary finite extension and its maximal abelian Galois subextension inside the chosen normal closure have the same actual idèle-class norm subgroup in the base field.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
variable
    (K : Type) (L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem ideleClassNorm_range_eq_maximalAbelianSubfield :
    (_root_.ideleClassNorm K L).range =
      (_root_.ideleClassNorm K
        (finiteNormalClosureMaximalAbelianSubfield K L)).range
theorem

normLimitation

L138 ↗
GlobalClassFieldTheory.GlobalClassFields.normLimitation
Documentation

Membership form of the norm limitation theorem.

Source context 6 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
variable
    (K : Type) (L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
Lean source · statement
theorem normLimitation (c : IdeleClassGroup K) :
    c ∈ (_root_.ideleClassNorm K L).range ↔
      c ∈ (_root_.ideleClassNorm K
        (finiteNormalClosureMaximalAbelianSubfield K L)).range
theorem

finiteNormalClosureMaximalAbelianSubfield_eq_originalField_of_isAbelianGalois

L147 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteNormalClosureMaximalAbelianSubfield_eq_originalField_of_isAbelianGalois
Documentation

If the original extension is already abelian Galois, its distinguished copy is the maximal abelian subfield selected by norm limitation.

Source context 7 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
variable
    (K : Type) (L : Type)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]
omit [FiniteDimensional K L] in
Lean source · statement
theorem
    finiteNormalClosureMaximalAbelianSubfield_eq_originalField_of_isAbelianGalois
    [IsAbelianGalois K L] :
    finiteNormalClosureMaximalAbelianSubfield K L =
      finiteNormalClosureOriginalField K L

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