NYLL
Module

SeparableUnitsNorm.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.SeparableUnitsNorm
16 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: the abstract norm on separable-closure units

The coefficient module in local class field theory is the unit group of a separable closure. This file compares the norm defined in the abstract class-formation framework by a sum over abstract Galois cosets with the ordinary field norm. The comparison is proved first for an arbitrary (possibly infinite) Galois ambient field, so it does not require the ground field to be perfect.

Imports4
Imported by13

Declarations

def

baseUnitsEquivGaloisAmbientFixed

L41 ↗
LocalClassFieldTheory.baseUnitsEquivGaloisAmbientFixed
Documentation

Canonical identification of Kˣ with the coefficient group fixed by the full absolute Galois group.

Source context 7 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
Lean source · statement
def baseUnitsEquivGaloisAmbientFixed :
    Additive Kˣ ≃+ ambientFixedAddSubgroup
      (galoisAmbientUnitsRep K Ω)
      (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
theorem

baseUnitsEquivGaloisAmbientFixed_val

L54 ↗
LocalClassFieldTheory.baseUnitsEquivGaloisAmbientFixed_val
Documentation

States the theorem baseUnitsEquivGaloisAmbientFixed_val.

Source context 7 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
Lean source · statement
theorem baseUnitsEquivGaloisAmbientFixed_val (x : Kˣ) :
    ((Additive.toMul
      ((baseUnitsEquivGaloisAmbientFixed K Ω (Additive.ofMul x)).1 :
        Additive Ωˣ) : Ωˣ) : Ω) = algebraMap K Ω (x : K)
instance

baseFixingExtensionQuotient_finite

L65 ↗
LocalClassFieldTheory.baseFixingExtensionQuotient_finite
Documentation

Provides the instance baseFixingExtensionQuotient_finite.

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section FiniteGaloisIntermediate
variable (E : IntermediateField K Ω) [FiniteDimensional K E] [IsGalois K E]
Lean source · statement
instance baseFixingExtensionQuotient_finite :
    Finite ((closedFixingSubgroup K Ω
        (⊥ : IntermediateField K Ω)).toSubgroup ⧸
      extensionSubgroup
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E)
        (fixingSubgroupLeBase K Ω E))
theorem

relativeCosetAction_intermediateFieldUnit_val

L77 ↗
LocalClassFieldTheory.relativeCosetAction_intermediateFieldUnit_val
Documentation

States the theorem relativeCosetAction_intermediateFieldUnit_val.

Source context 10 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section FiniteGaloisIntermediate
variable (E : IntermediateField K Ω) [FiniteDimensional K E] [IsGalois K E]
omit [FiniteDimensional K E] in
Lean source · statement
theorem relativeCosetAction_intermediateFieldUnit_val
    (x : Eˣ)
    (q : (closedFixingSubgroup K Ω
        (⊥ : IntermediateField K Ω)).toSubgroup ⧸
      extensionSubgroup
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E)
        (fixingSubgroupLeBase K Ω E)) :
    ((Additive.toMul
      (relativeCosetAction (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)
        (intermediateFieldUnitsEquivGaloisFixed K Ω E
          (Additive.ofMul x)) q) : Ωˣ) : Ω) =
      E.val ((baseFixingExtensionQuotientEquivGaloisGroup K Ω E q) (x : E))
theorem

relativeNorm_intermediateFieldUnit_val

L121 ↗
LocalClassFieldTheory.relativeNorm_intermediateFieldUnit_val
Documentation

On units coming from a finite Galois intermediate field, the abstract relative norm is the ordinary field norm.

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section FiniteGaloisIntermediate
variable (E : IntermediateField K Ω) [FiniteDimensional K E] [IsGalois K E]
Lean source · statement
theorem relativeNorm_intermediateFieldUnit_val (x : Eˣ) :
    ((Additive.toMul
      ((relativeNorm (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)
        (intermediateFieldUnitsEquivGaloisFixed K Ω E
          (Additive.ofMul x))).1 : Additive Ωˣ) : Ωˣ) : Ω) =
      algebraMap K Ω (Algebra.norm K (x : E))
theorem

relativeNorm_intermediateFieldUnit

L175 ↗
LocalClassFieldTheory.relativeNorm_intermediateFieldUnit
Documentation

Equivariant form of the norm comparison, with both fixed coefficient groups identified with the corresponding field unit groups.

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section FiniteGaloisIntermediate
variable (E : IntermediateField K Ω) [FiniteDimensional K E] [IsGalois K E]
Lean source · statement
theorem relativeNorm_intermediateFieldUnit (x : Eˣ) :
    relativeNorm (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)
        (intermediateFieldUnitsEquivGaloisFixed K Ω E
          (Additive.ofMul x)) =
      baseUnitsEquivGaloisAmbientFixed K Ω
        (Additive.ofMul (normUnits K E x))
theorem

map_finiteNormSubgroup_eq_additiveNormSubgroup

L190 ↗
LocalClassFieldTheory.map_finiteNormSubgroup_eq_additiveNormSubgroup
Documentation

Under the base-field fixed-unit equivalence, the abstract finite norm subgroup is exactly the ordinary field-norm subgroup.

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section FiniteGaloisIntermediate
variable (E : IntermediateField K Ω) [FiniteDimensional K E] [IsGalois K E]
Lean source · statement
theorem map_finiteNormSubgroup_eq_additiveNormSubgroup :
    (finiteNormSubgroup (galoisAmbientUnitsRep K Ω)
      (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
      (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)).map
        (baseUnitsEquivGaloisAmbientFixed K Ω).symm.toAddMonoidHom =
      additiveNormSubgroup K E
def

finiteNormQuotientEquivNormQuotient

L230 ↗
LocalClassFieldTheory.finiteNormQuotientEquivNormQuotient
Documentation

The abstract finite norm quotient is the actual multiplicative field norm quotient, written additively for the abstract class-formation API.

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section FiniteGaloisIntermediate
variable (E : IntermediateField K Ω) [FiniteDimensional K E] [IsGalois K E]
Lean source · statement
def finiteNormQuotientEquivNormQuotient :
    FiniteNormQuotient (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E) ≃+
      Additive (NormQuotient K E)
theorem

finiteNormQuotientEquivNormQuotient_finiteNormClass

L304 ↗
LocalClassFieldTheory.finiteNormQuotientEquivNormQuotient_finiteNormClass
Documentation

The fixed-unit comparison carries the canonical finite norm class to the canonical field norm class. The concrete quotient representation remains private to the proof of this boundary theorem.

Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section FiniteGaloisIntermediate
variable (E : IntermediateField K Ω) [FiniteDimensional K E] [IsGalois K E]
Lean source · statement
theorem finiteNormQuotientEquivNormQuotient_finiteNormClass
    (a : ambientFixedAddSubgroup (galoisAmbientUnitsRep K Ω)
      (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))) :
    finiteNormQuotientEquivNormQuotient K Ω E
        (finiteNormClass (galoisAmbientUnitsRep K Ω)
          (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
          (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E) a) =
      (MonoidHom.toAdditive (normClass K E))
        ((baseUnitsEquivGaloisAmbientFixed K Ω).symm a)
instance

embeddedFieldRangeFiniteDimensional

L348 ↗
LocalClassFieldTheory.embeddedFieldRangeFiniteDimensional
Source context 9 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section EmbeddedFiniteGaloisExtension
variable (L : Type) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  (i : L →ₐ[K] Ω)
Lean source · statement
instance embeddedFieldRangeFiniteDimensional :
    FiniteDimensional K (AlgHom.fieldRange i)
instance

embeddedFieldRangeIsGalois

L352 ↗
LocalClassFieldTheory.embeddedFieldRangeIsGalois
Source context 10 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section EmbeddedFiniteGaloisExtension
variable (L : Type) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  (i : L →ₐ[K] Ω)
noncomputable local instance embeddedFieldRangeFiniteDimensional :
    FiniteDimensional K (AlgHom.fieldRange i) :=
  (AlgEquiv.ofInjectiveField i).toLinearEquiv.finiteDimensional
Lean source · statement
instance embeddedFieldRangeIsGalois :
    IsGalois K (AlgHom.fieldRange i)
theorem

normUnits_embeddedExtensionAlgEquiv

L358 ↗
LocalClassFieldTheory.normUnits_embeddedExtensionAlgEquiv
Documentation

The field norm is invariant under an algebra equivalence, at unit level.

Source context 12 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section EmbeddedFiniteGaloisExtension
variable (L : Type) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  (i : L →ₐ[K] Ω)
noncomputable local instance embeddedFieldRangeFiniteDimensional :
    FiniteDimensional K (AlgHom.fieldRange i) :=
  (AlgEquiv.ofInjectiveField i).toLinearEquiv.finiteDimensional
noncomputable local instance embeddedFieldRangeIsGalois :
    IsGalois K (AlgHom.fieldRange i) :=
  IsGalois.of_algEquiv (AlgEquiv.ofInjectiveField i)
omit [IsGalois K Ω] [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem normUnits_embeddedExtensionAlgEquiv (x : Lˣ) :
    normUnits K (AlgHom.fieldRange i)
        (Units.mapEquiv (AlgEquiv.ofInjectiveField i).toMulEquiv x) =
      normUnits K L x
theorem

localNormSubgroup_fieldRange_eq

L369 ↗
LocalClassFieldTheory.localNormSubgroup_fieldRange_eq
Documentation

The ordinary norm subgroups are independent of the chosen realization of the finite extension inside the ambient Galois extension.

Source context 12 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section EmbeddedFiniteGaloisExtension
variable (L : Type) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  (i : L →ₐ[K] Ω)
noncomputable local instance embeddedFieldRangeFiniteDimensional :
    FiniteDimensional K (AlgHom.fieldRange i) :=
  (AlgEquiv.ofInjectiveField i).toLinearEquiv.finiteDimensional
noncomputable local instance embeddedFieldRangeIsGalois :
    IsGalois K (AlgHom.fieldRange i) :=
  IsGalois.of_algEquiv (AlgEquiv.ofInjectiveField i)
omit [IsGalois K Ω] [FiniteDimensional K L] [IsGalois K L] in
Lean source · statement
theorem localNormSubgroup_fieldRange_eq :
    localNormSubgroup K (AlgHom.fieldRange i) = localNormSubgroup K L
theorem

relativeNorm_embeddedExtensionUnit

L389 ↗
LocalClassFieldTheory.relativeNorm_embeddedExtensionUnit
Documentation

The abstract relative norm attached to an embedded finite Galois extension is the actual field norm on its unit group.

Source context 11 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section EmbeddedFiniteGaloisExtension
variable (L : Type) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  (i : L →ₐ[K] Ω)
noncomputable local instance embeddedFieldRangeFiniteDimensional :
    FiniteDimensional K (AlgHom.fieldRange i) :=
  (AlgEquiv.ofInjectiveField i).toLinearEquiv.finiteDimensional
noncomputable local instance embeddedFieldRangeIsGalois :
    IsGalois K (AlgHom.fieldRange i) :=
  IsGalois.of_algEquiv (AlgEquiv.ofInjectiveField i)
Lean source · statement
theorem relativeNorm_embeddedExtensionUnit (x : Lˣ) :
    relativeNorm (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω (AlgHom.fieldRange i))
        (fixingSubgroupLeBase K Ω (AlgHom.fieldRange i))
        (embeddedFieldUnitsEquivGaloisFixed K Ω L i (Additive.ofMul x)) =
      baseUnitsEquivGaloisAmbientFixed K Ω
        (Additive.ofMul (normUnits K L x))
def

finiteNormQuotientEquivEmbeddedNormQuotient

L406 ↗
LocalClassFieldTheory.finiteNormQuotientEquivEmbeddedNormQuotient
Documentation

For an embedded finite Galois extension L/K, the finite norm quotient in the abstract class formation is the actual quotient Kˣ/N_{L/K}Lˣ.

Source context 11 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section EmbeddedFiniteGaloisExtension
variable (L : Type) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  (i : L →ₐ[K] Ω)
noncomputable local instance embeddedFieldRangeFiniteDimensional :
    FiniteDimensional K (AlgHom.fieldRange i) :=
  (AlgEquiv.ofInjectiveField i).toLinearEquiv.finiteDimensional
noncomputable local instance embeddedFieldRangeIsGalois :
    IsGalois K (AlgHom.fieldRange i) :=
  IsGalois.of_algEquiv (AlgEquiv.ofInjectiveField i)
Lean source · statement
def finiteNormQuotientEquivEmbeddedNormQuotient :
    FiniteNormQuotient (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω (AlgHom.fieldRange i))
        (fixingSubgroupLeBase K Ω (AlgHom.fieldRange i)) ≃+
      Additive (NormQuotient K L)
theorem

finiteNormQuotientEquivEmbeddedNormQuotient_finiteNormClass

L421 ↗
LocalClassFieldTheory.finiteNormQuotientEquivEmbeddedNormQuotient_finiteNormClass
Documentation

The embedded-extension comparison carries a canonical finite norm class to the corresponding field norm class, followed by the canonical transport from the embedded field range to L.

Source context 11 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation CyclicCohomology
noncomputable section
open scoped BigOperators
variable (K : Type) (Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
  [IsGalois K Ω]
section EmbeddedFiniteGaloisExtension
variable (L : Type) [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
  (i : L →ₐ[K] Ω)
noncomputable local instance embeddedFieldRangeFiniteDimensional :
    FiniteDimensional K (AlgHom.fieldRange i) :=
  (AlgEquiv.ofInjectiveField i).toLinearEquiv.finiteDimensional
noncomputable local instance embeddedFieldRangeIsGalois :
    IsGalois K (AlgHom.fieldRange i) :=
  IsGalois.of_algEquiv (AlgEquiv.ofInjectiveField i)
Lean source · statement
theorem finiteNormQuotientEquivEmbeddedNormQuotient_finiteNormClass
    (a : ambientFixedAddSubgroup (galoisAmbientUnitsRep K Ω)
      (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))) :
    finiteNormQuotientEquivEmbeddedNormQuotient K Ω L i
        (finiteNormClass (galoisAmbientUnitsRep K Ω)
          (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
          (closedFixingSubgroup K Ω (AlgHom.fieldRange i))
          (fixingSubgroupLeBase K Ω (AlgHom.fieldRange i)) a) =
      (MulEquiv.toAdditive
        (normQuotientEquivOfNormSubgroupEq K (AlgHom.fieldRange i) L
          (localNormSubgroup_fieldRange_eq K Ω L i)))
        ((MonoidHom.toAdditive (normClass K (AlgHom.fieldRange i)))
          ((baseUnitsEquivGaloisAmbientFixed K Ω).symm a))

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