Module

IntermediateNormAbelianization.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.Reciprocity.IntermediateNormAbelianization

5 declarations indexed from sourceView source ↗

Module documentation

Abelianized restriction over intermediate fields

For a finite Galois extension and an arbitrary intermediate field, this file identifies the image of abelianized restriction with the image of the fixing subgroup. It then proves naturality for the ordinary idèle-class norm and identifies its range as the Artin preimage of that abelianized fixing-subgroup image. No normality of the intermediate extension over the base is assumed.

Imports2

Imported by2

def

intermediateAbelianizedRestriction

L33 ↗

GlobalClassFieldTheory.Reciprocity.intermediateAbelianizedRestriction

Documentation

Restriction from the Galois group over an intermediate field, passed to abelianizations.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K N : Type}
    [Field K] [NumberField K]
    [Field N] [NumberField N]
    [Algebra K N] [IsGalois K N]

Lean source · statement

def intermediateAbelianizedRestriction
    (M : IntermediateField K N) :
    Abelianization Gal(N / M) →* Abelianization Gal(N / K)

theorem

intermediateAbelianizedRestriction_range_eq_fixingSubgroup_image

L42 ↗

GlobalClassFieldTheory.Reciprocity.intermediateAbelianizedRestriction_range_eq_fixingSubgroup_image

Documentation

The image of abelianized restriction from an intermediate field is the image of its fixing subgroup in the ambient abelianization.

Source context 5 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K N : Type}
    [Field K] [NumberField K]
    [Field N] [NumberField N]
    [Algebra K N] [IsGalois K N]
omit [NumberField K] [NumberField N] [IsGalois K N] in

Lean source · statement

theorem intermediateAbelianizedRestriction_range_eq_fixingSubgroup_image
    (M : IntermediateField K N) :
    (intermediateAbelianizedRestriction (K := K) (N := N) M).range =
      M.fixingSubgroup.map
        (Abelianization.of : Gal(N / K) →* Abelianization Gal(N / K))

theorem

intermediateAbelianizedRestriction_comp_globalNormResidue_range_eq_fixingSubgroup_image

L73 ↗

GlobalClassFieldTheory.Reciprocity.intermediateAbelianizedRestriction_comp_globalNormResidue_range_eq_fixingSubgroup_image

Documentation

After the surjective global norm-residue map over an intermediate field, abelianized restriction still has exactly the fixing-subgroup image.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K N : Type}
    [Field K] [NumberField K]
    [Field N] [NumberField N]
    [Algebra K N] [IsGalois K N]

Lean source · statement

theorem
    intermediateAbelianizedRestriction_comp_globalNormResidue_range_eq_fixingSubgroup_image
    (M : IntermediateField K N) :
    ((intermediateAbelianizedRestriction (K := K) (N := N) M).comp
        (globalNormResidueAbelianizationMonoidHom M N)).range =
      M.fixingSubgroup.map
        (Abelianization.of : Gal(N / K) →* Abelianization Gal(N / K))

theorem

globalNormResidueAbelianization_comp_ideleClassNorm_intermediate

L100 ↗

GlobalClassFieldTheory.Reciprocity.globalNormResidueAbelianization_comp_ideleClassNorm_intermediate

Documentation

Ordinary idèle-class norm from an arbitrary intermediate field agrees with restriction of the finite-Galois global norm-residue symbol after abelianization. No normality of the intermediate field over the base is assumed.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K N : Type}
    [Field K] [NumberField K]
    [Field N] [NumberField N]
    [Algebra K N] [IsGalois K N]

Lean source · statement

theorem globalNormResidueAbelianization_comp_ideleClassNorm_intermediate
    (M : IntermediateField K N) :
    (globalNormResidueAbelianizationMonoidHom K N).comp
        (_root_.ideleClassNorm K M) =
      (intermediateAbelianizedRestriction (K := K) (N := N) M).comp
        (globalNormResidueAbelianizationMonoidHom M N)

theorem

ideleClassNorm_range_eq_artin_preimage_abelianizedFixingSubgroup

L113 ↗

GlobalClassFieldTheory.Reciprocity.ideleClassNorm_range_eq_artin_preimage_abelianizedFixingSubgroup

Documentation

The norm subgroup from an arbitrary intermediate field is the inverse image, under finite-Galois global reciprocity, of the image of its fixing subgroup in the ambient Galois abelianization.

Source context 4 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
variable
    {K N : Type}
    [Field K] [NumberField K]
    [Field N] [NumberField N]
    [Algebra K N] [IsGalois K N]

Lean source · statement

theorem ideleClassNorm_range_eq_artin_preimage_abelianizedFixingSubgroup
    (M : IntermediateField K N) :
    (_root_.ideleClassNorm K M).range =
      (M.fixingSubgroup.map
        (Abelianization.of : Gal(N / K) →* Abelianization Gal(N / K))).comap
        (globalNormResidueAbelianizationMonoidHom K N)

Module documentation

Abelianized restriction over intermediate fields

Declarations

intermediateAbelianizedRestriction

intermediateAbelianizedRestriction_range_eq_fixingSubgroup_image

intermediateAbelianizedRestriction_comp_globalNormResidue_range_eq_fixingSubgroup_image

globalNormResidueAbelianization_comp_ideleClassNorm_intermediate

ideleClassNorm_range_eq_artin_preimage_abelianizedFixingSubgroup