Module

AbsoluteUnitsFixedField.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.AbsoluteUnitsFixedField

9 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: Galois units and fixed fields

For local reciprocity the coefficient module in the abstract class formation is A = (K^sep)ˣ. This file identifies its subgroup fixed by the actual closed fixing subgroup of an intermediate field E with the image of Eˣ.

The result is stated for an arbitrary Galois ambient extension. In particular it applies to SeparableClosure K / K for every field K; no perfectness, local-field, or finite-dimensional hypothesis is needed. Using the separable closure is essential in positive characteristic: the fixed field of Aut(K^alg/K) inside K^alg need not be K when K is imperfect.

Imports3

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.ClosedFixingSubgroup
Nyll.GaloisCohomology.Kummer.Abstract.KummerDelta
Mathlib.RepresentationTheory.Rep.Basic

Imported by3

abbrev

galoisAmbientUnitsRep

L37 ↗

LocalClassFieldTheory.galoisAmbientUnitsRep

Documentation

The actual Galois representation on Ωˣ, written additively for the group-cohomology API.

Source context 4 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

abbrev galoisAmbientUnitsRep : Rep ℤ (Gal(Ω / K))

def

intermediateFieldUnitsToGaloisAmbient

L42 ↗

LocalClassFieldTheory.intermediateFieldUnitsToGaloisAmbient

Documentation

Inclusion of the units of an intermediate field into the units of the chosen Galois ambient field, in additive notation.

Source context 4 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

def intermediateFieldUnitsToGaloisAmbient
    (E : IntermediateField K Ω) :
    Additive Eˣ →+ Additive Ωˣ

theorem

intermediateFieldUnitsToGaloisAmbient_apply

L49 ↗

LocalClassFieldTheory.intermediateFieldUnitsToGaloisAmbient_apply

Documentation

States the theorem intermediateFieldUnitsToGaloisAmbient_apply.

Source context 4 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]

Lean source · statement

theorem intermediateFieldUnitsToGaloisAmbient_apply
    (E : IntermediateField K Ω) (x : Eˣ) :
    intermediateFieldUnitsToGaloisAmbient K Ω E (Additive.ofMul x) =
      Additive.ofMul (Units.map E.val.toRingHom x)

theorem

mem_galoisAmbientUnits_fixed_iff

L59 ↗

LocalClassFieldTheory.mem_galoisAmbientUnits_fixed_iff

Documentation

An ambient unit is fixed by Gal(Ω/E) exactly when its underlying field element belongs to E.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem mem_galoisAmbientUnits_fixed_iff
    (E : IntermediateField K Ω)
    (x : Additive Ωˣ) :
    x ∈ ambientFixedAddSubgroup (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω E) ↔
      ((Additive.toMul x : Ωˣ) : Ω) ∈ E

theorem

intermediateFieldUnitsToGaloisAmbient_range

L109 ↗

LocalClassFieldTheory.intermediateFieldUnitsToGaloisAmbient_range

Documentation

The image of Eˣ in Ωˣ is precisely the abstract fixed subgroup A_E used in the abstract class-formation framework.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem intermediateFieldUnitsToGaloisAmbient_range
    (E : IntermediateField K Ω) :
    (intermediateFieldUnitsToGaloisAmbient K Ω E).range =
      ambientFixedAddSubgroup (galoisAmbientUnitsRep K Ω)
        (closedFixingSubgroup K Ω E)

def

intermediateFieldUnitsEquivGaloisFixed

L150 ↗

LocalClassFieldTheory.intermediateFieldUnitsEquivGaloisFixed

Documentation

Canonical additive equivalence Eˣ ≃ A_E for the actual ambient-unit representation.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

def intermediateFieldUnitsEquivGaloisFixed
    (E : IntermediateField K Ω) :
    Additive Eˣ ≃+ ambientFixedAddSubgroup (galoisAmbientUnitsRep K Ω)
      (closedFixingSubgroup K Ω E)

theorem

intermediateFieldUnitsEquivGaloisFixed_coe

L166 ↗

LocalClassFieldTheory.intermediateFieldUnitsEquivGaloisFixed_coe

Documentation

States the theorem intermediateFieldUnitsEquivGaloisFixed_coe.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem intermediateFieldUnitsEquivGaloisFixed_coe
    (E : IntermediateField K Ω) (x : Additive Eˣ) :
    (intermediateFieldUnitsEquivGaloisFixed K Ω E x).1 =
        intermediateFieldUnitsToGaloisAmbient K Ω E x

def

embeddedFieldUnitsEquivGaloisFixed

L176 ↗

LocalClassFieldTheory.embeddedFieldUnitsEquivGaloisFixed

Documentation

For an embedded extension i : L → Ω, the coefficient group fixed by Gal(Ω/i(L)) is canonically the actual unit group Lˣ. This is the form needed when an abstract finite extension is realized inside a separable closure.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

def embeddedFieldUnitsEquivGaloisFixed
    (L : Type) [Field L] [Algebra K L]
    (i : L →ₐ[K] Ω) :
    Additive Lˣ ≃+ ambientFixedAddSubgroup (galoisAmbientUnitsRep K Ω)
      (closedFixingSubgroup K Ω (AlgHom.fieldRange i))

theorem

embeddedFieldUnitsEquivGaloisFixed_coe

L187 ↗

LocalClassFieldTheory.embeddedFieldUnitsEquivGaloisFixed_coe

Documentation

States the theorem embeddedFieldUnitsEquivGaloisFixed_coe.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory KummerTheory CyclicCohomology
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω]
variable [IsGalois K Ω]

Lean source · statement

theorem embeddedFieldUnitsEquivGaloisFixed_coe
    (L : Type) [Field L] [Algebra K L]
    (i : L →ₐ[K] Ω) (x : Lˣ) :
    (embeddedFieldUnitsEquivGaloisFixed K Ω L i (Additive.ofMul x)).1 =
      Additive.ofMul (Units.map i.toRingHom.toMonoidHom x)

Module documentation

Finite local reciprocity: Galois units and fixed fields

Declarations