NYLL
Module

IntermediateFieldNormResidueNaturality.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.IntermediateFieldNormResidueNaturality
12 declarations indexed from sourceView source ↗

Module documentation

Restriction naturality for the concrete local norm-residue symbol

The abstract class formation supplies restriction naturality. This file constructs the field-facing restriction map for two finite Galois intermediate fields in the fixed separable closure and transports the naturality identity to the concrete local norm-residue symbol.

The intermediate-field restriction is packaged here so callers do not have to install the auxiliary Algebra E F and scalar-tower instances attached to an inclusion E ≤ F.

Imports5
Imported by3

Declarations

abbrev

absoluteGalois

L41 ↗
LocalClassFieldTheory.absoluteGalois
Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
abbrev absoluteGalois (K : Type) [Field K]
abbrev

absoluteUnits

L44 ↗
LocalClassFieldTheory.absoluteUnits
Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
abbrev absoluteUnits (K : Type) [Field K] :
    Rep ℤ (absoluteGalois K)
abbrev

abstractBase

L48 ↗
LocalClassFieldTheory.abstractBase
Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
abbrev abstractBase (K : Type) [Field K] :
    ClosedSubgroup (absoluteGalois K)
def

embeddedBaseNormClass

L59 ↗
LocalClassFieldTheory.embeddedBaseNormClass
Documentation

The finite abstract norm class represented by a base-field unit in an explicit separable-closure realization.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
section AbstractToConcrete
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def embeddedBaseNormClass
    (i : L →ₐ[K] SeparableClosure K) (a : Kˣ) :
    FiniteNormQuotient (absoluteUnits K) (abstractBase K)
      (finiteGaloisAbstractExtensionOfEmbedding K L i).field
      (finiteGaloisAbstractExtensionOfEmbedding K L i).below
theorem

concreteNormResidueSymbolOfEmbedding_eq_abstract

L74 ↗
LocalClassFieldTheory.concreteNormResidueSymbolOfEmbedding_eq_abstract
Documentation

Before specializing the local datum, the concrete norm-residue symbol is the abstract norm-residue class transported through the canonical quotient equivalence. This pointwise transport formula expresses abstract restriction naturality as a statement about actual field automorphisms.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
section AbstractToConcrete
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem concreteNormResidueSymbolOfEmbedding_eq_abstract
    (i : L →ₐ[K] SeparableClosure K)
    (D : DegreeData (absoluteGalois K))
    (v : ValuationData D (absoluteUnits K))
    (hcf : SatisfiesClassFieldAxiom (absoluteUnits K)) (a : Kˣ) :
    concreteNormResidueSymbolOfEmbedding K L i D v hcf a =
      (finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding
        K L i).abelianizationCongr
        (Additive.toMul
          (D.normResidueSymbol (absoluteUnits K) v hcf (intrinsicFiniteAbstractBase K)
            (finiteGaloisAbstractExtensionOfEmbedding K L i)
            (embeddedBaseNormClass K L i a)))
theorem

commGroup_abelianizationCongr_of

L140 ↗
LocalClassFieldTheory.commGroup_abelianizationCongr_of
Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
section IntermediateRestriction
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem commGroup_abelianizationCongr_of
    {G H : Type*} [Group G] [CommGroup H]
    (q : G ≃* H) (x : G) :
    (Abelianization.equivOfComm (H := H)).symm
        (q.abelianizationCongr (Abelianization.of x)) =
      q x
theorem

intermediateFieldRestrict_abstractQuotient_mk

L152 ↗
LocalClassFieldTheory.intermediateFieldRestrict_abstractQuotient_mk
Source context 10 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
section IntermediateRestriction
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem intermediateFieldRestrict_abstractQuotient_mk
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsGalois K E] [IsGalois K F]
    (sigma : (abstractBase K).toSubgroup) :
    intermediateFieldRestrictNormalHom E F hEF
        (finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K F F.val
          (QuotientGroup.mk sigma)) =
      finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K E E.val
        (QuotientGroup.mk (Subgroup.inclusion le_rfl sigma))
theorem

embeddedAbstractExtension_field_le

L185 ↗
LocalClassFieldTheory.embeddedAbstractExtension_field_le
Source context 10 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
section IntermediateRestriction
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem embeddedAbstractExtension_field_le
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsGalois K E] [IsGalois K F] :
    (finiteGaloisAbstractExtensionOfEmbedding K F F.val).field.toSubgroup ≤
      (finiteGaloisAbstractExtensionOfEmbedding K E E.val).field.toSubgroup
theorem

intermediateFieldRestrict_abstractAbelianization_of_mk

L201 ↗
LocalClassFieldTheory.intermediateFieldRestrict_abstractAbelianization_of_mk
Source context 10 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
section IntermediateRestriction
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem intermediateFieldRestrict_abstractAbelianization_of_mk
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsAbelianGalois K E] [IsAbelianGalois K F]
    (sigma : (abstractBase K).toSubgroup) :
    intermediateFieldRestrictNormalHom E F hEF
        ((Abelianization.equivOfComm (H := Gal(F / K))).symm
          ((finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding
            K F F.val).abelianizationCongr
              (Abelianization.of (QuotientGroup.mk sigma)))) =
      (Abelianization.equivOfComm (H := Gal(E / K))).symm
        ((finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding
          K E E.val).abelianizationCongr
            (normResidueNaturalityAbelianizedRestriction
              (abstractBase K) (abstractBase K)
              (finiteGaloisAbstractExtensionOfEmbedding K E E.val).field
              (finiteGaloisAbstractExtensionOfEmbedding K F F.val).field
              (finiteGaloisAbstractExtensionOfEmbedding K E E.val).below
              (finiteGaloisAbstractExtensionOfEmbedding K F F.val).below
              le_rfl (embeddedAbstractExtension_field_le K E F hEF)
              (Abelianization.of (QuotientGroup.mk sigma))))
theorem

intermediateFieldRestrict_abstractAbelianization

L267 ↗
LocalClassFieldTheory.intermediateFieldRestrict_abstractAbelianization
Source context 10 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
section IntermediateRestriction
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem intermediateFieldRestrict_abstractAbelianization
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsAbelianGalois K E] [IsAbelianGalois K F]
    (z : Abelianization
      (finiteGaloisAbstractExtensionOfEmbedding K F F.val).extensionQuotient) :
    intermediateFieldRestrictNormalHom E F hEF
        ((Abelianization.equivOfComm (H := Gal(F / K))).symm
          ((finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K F F.val).abelianizationCongr
            z)) =
      (Abelianization.equivOfComm (H := Gal(E / K))).symm
        ((finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding K E E.val).abelianizationCongr
          (normResidueNaturalityAbelianizedRestriction
            (abstractBase K) (abstractBase K)
            (finiteGaloisAbstractExtensionOfEmbedding K E E.val).field
            (finiteGaloisAbstractExtensionOfEmbedding K F F.val).field
            (finiteGaloisAbstractExtensionOfEmbedding K E E.val).below
            (finiteGaloisAbstractExtensionOfEmbedding K F F.val).below
            le_rfl (embeddedAbstractExtension_field_le K E F hEF) z))
theorem

concreteNormResidueAutomorphism_restrict

L297 ↗
LocalClassFieldTheory.concreteNormResidueAutomorphism_restrict
Documentation

Restriction naturality for the concrete norm-residue symbol, before specializing the three structures of the local class formation. Both extensions are literal intermediate fields of the fixed separable closure, so the vertical Galois map is the actual restriction map above.

Source context 10 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
section IntermediateRestriction
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem concreteNormResidueAutomorphism_restrict
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsAbelianGalois K E] [IsAbelianGalois K F]
    (D : DegreeData (absoluteGalois K))
    (v : ValuationData D (absoluteUnits K))
    (hcf : SatisfiesClassFieldAxiom (absoluteUnits K)) (a : Kˣ) :
    intermediateFieldRestrictNormalHom E F hEF
        ((Abelianization.equivOfComm (H := Gal(F / K))).symm
          (concreteNormResidueSymbolOfEmbedding
            K F F.val D v hcf a)) =
      (Abelianization.equivOfComm (H := Gal(E / K))).symm
        (concreteNormResidueSymbolOfEmbedding
          K E E.val D v hcf a)
theorem

localArtinAutomorphism_restrict

L415 ↗
LocalClassFieldTheory.localArtinAutomorphism_restrict
Documentation

Restriction naturality for the canonical local norm-residue symbol, expressed through automorphisms of finite abelian intermediate fields.

Source context 9 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory CyclicCohomology KummerTheory
open ClassFormation LocalClassFieldTheory
open scoped IsMulCommutative
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
section IntermediateRestriction
variable (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localArtinAutomorphism_restrict
    (E F : IntermediateField K (SeparableClosure K)) (hEF : E ≤ F)
    [FiniteDimensional K E] [FiniteDimensional K F]
    [IsAbelianGalois K E] [IsAbelianGalois K F] (a : Kˣ) :
    intermediateFieldRestrictNormalHom E F hEF
        ((Abelianization.equivOfComm (H := Gal(F / K))).symm
          (localArtinMonoidHom K F a)) =
      (Abelianization.equivOfComm (H := Gal(E / K))).symm
        (localArtinMonoidHom K E a)

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