Module

FiniteGaloisRealization.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteGaloisRealization

20 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: realizing finite Galois extensions in a separable closure

Every finite Galois extension L/K is embedded into the chosen separable closure of K. Its image supplies the concrete closed subgroup used by the abstract class-field theory. The resulting abstract fixed coefficient group is Lˣ, and the resulting abstract extension quotient is the actual Gal(L/K).

No perfectness hypothesis is imposed; this includes equal-characteristic local fields such as finite extensions of 𝔽_q((t)).

Realization relative to an explicit embedding

The chosen realization

Imports4

Mathlib.SetTheory.Cardinal.Finite
Mathlib.FieldTheory.SeparableClosure
Nyll.ClassFieldTheory.AlgebraicNumberTheory.SeparableClosureEmbedding
Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.GaloisExtensionQuotient

Imported by4

def

finiteGaloisFieldRangeOfEmbedding

L40 ↗

LocalClassFieldTheory.finiteGaloisFieldRangeOfEmbedding

Documentation

The embedded copy of L determined by an explicit embedding into the fixed separable closure. Keeping the embedding visible is what makes the canonicity argument in the finite local reciprocity theorem meaningful.

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisFieldRangeOfEmbedding
    (i : L →ₐ[K] SeparableClosure K) :
    IntermediateField K (SeparableClosure K)

def

finiteGaloisFieldRangeEquivOfEmbedding

L46 ↗

LocalClassFieldTheory.finiteGaloisFieldRangeEquivOfEmbedding

Documentation

An explicit embedding identifies L with its field range.

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisFieldRangeEquivOfEmbedding
    (i : L →ₐ[K] SeparableClosure K) :
    L ≃ₐ[K] finiteGaloisFieldRangeOfEmbedding K L i

instance

finiteGaloisFieldRangeOfEmbedding_isGalois

L52 ↗

LocalClassFieldTheory.finiteGaloisFieldRangeOfEmbedding_isGalois

Documentation

The image of an embedded finite Galois extension is again Galois over the base field.

Source context 4 commands

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

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

Lean source · statement

instance finiteGaloisFieldRangeOfEmbedding_isGalois
    (i : L →ₐ[K] SeparableClosure K) :
    IsGalois K (finiteGaloisFieldRangeOfEmbedding K L i)

instance

finiteGaloisFieldRangeOfEmbedding_finiteDimensional

L58 ↗

LocalClassFieldTheory.finiteGaloisFieldRangeOfEmbedding_finiteDimensional

Documentation

The image of an embedded finite extension is finite-dimensional over the base field.

Source context 4 commands

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

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

Lean source · statement

instance finiteGaloisFieldRangeOfEmbedding_finiteDimensional
    (i : L →ₐ[K] SeparableClosure K) :
    FiniteDimensional K (finiteGaloisFieldRangeOfEmbedding K L i)

def

finiteGaloisClosedFixingSubgroupOfEmbedding

L65 ↗

LocalClassFieldTheory.finiteGaloisClosedFixingSubgroupOfEmbedding

Documentation

The closed fixing subgroup attached to an explicit realization of L/K in the separable closure.

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisClosedFixingSubgroupOfEmbedding
    (i : L →ₐ[K] SeparableClosure K) :
    ClosedSubgroup (Gal(SeparableClosure K / K))

instance

finiteGaloisExtensionSubgroupOfEmbedding_normal

L73 ↗

LocalClassFieldTheory.finiteGaloisExtensionSubgroupOfEmbedding_normal

Documentation

The fixing subgroup of an embedded finite Galois extension is normal in the absolute subgroup.

Source context 4 commands

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

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

Lean source · statement

instance finiteGaloisExtensionSubgroupOfEmbedding_normal
    (i : L →ₐ[K] SeparableClosure K) :
    (extensionSubgroup
      (closedFixingSubgroup K (SeparableClosure K)
        (⊥ : IntermediateField K (SeparableClosure K)))
      (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)
      (fixingSubgroupLeBase K (SeparableClosure K)
        (finiteGaloisFieldRangeOfEmbedding K L i))).Normal

def

finiteGaloisUnitsEquivAbstractFixedOfEmbedding

L93 ↗

LocalClassFieldTheory.finiteGaloisUnitsEquivAbstractFixedOfEmbedding

Documentation

The fixed coefficient group attached to an explicit realization is canonically the actual unit group Lˣ.

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisUnitsEquivAbstractFixedOfEmbedding
    (i : L →ₐ[K] SeparableClosure K) :
    Additive Lˣ ≃+
      ambientFixedAddSubgroup
        (galoisAmbientUnitsRep K (SeparableClosure K))
        (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)

theorem

finiteGaloisUnitsEquivAbstractFixedOfEmbedding_coe

L104 ↗

LocalClassFieldTheory.finiteGaloisUnitsEquivAbstractFixedOfEmbedding_coe

Documentation

The fixed-module equivalence sends a field unit to the unit induced by the chosen embedding.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem finiteGaloisUnitsEquivAbstractFixedOfEmbedding_coe
    (i : L →ₐ[K] SeparableClosure K) (x : Lˣ) :
    (finiteGaloisUnitsEquivAbstractFixedOfEmbedding K L i
      (Additive.ofMul x)).1 =
      Additive.ofMul (Units.map i.toRingHom.toMonoidHom x)

def

finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding

L113 ↗

LocalClassFieldTheory.finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding

Documentation

The abstract class-formation extension quotient attached to an explicit realization of L/K is the actual relative Galois group.

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisAbstractQuotientEquivGaloisGroupOfEmbedding
    (i : L →ₐ[K] SeparableClosure K) :
    ((closedFixingSubgroup K (SeparableClosure K)
        (⊥ : IntermediateField K (SeparableClosure K))).toSubgroup ⧸
      extensionSubgroup
        (closedFixingSubgroup K (SeparableClosure K)
          (⊥ : IntermediateField K (SeparableClosure K)))
        (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)
        (fixingSubgroupLeBase K (SeparableClosure K)
          (finiteGaloisFieldRangeOfEmbedding K L i))) ≃*
      Gal(L / K)

theorem

finiteGaloisExtensionSubgroupOfEmbedding_index_eq_finrank

L131 ↗

LocalClassFieldTheory.finiteGaloisExtensionSubgroupOfEmbedding_index_eq_finrank

Documentation

The subgroup attached to an explicit finite Galois realization has index equal to the ordinary field degree.

Source context 4 commands

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

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

Lean source · statement

theorem finiteGaloisExtensionSubgroupOfEmbedding_index_eq_finrank
    (i : L →ₐ[K] SeparableClosure K) :
    (extensionSubgroup
      (closedFixingSubgroup K (SeparableClosure K)
        (⊥ : IntermediateField K (SeparableClosure K)))
      (finiteGaloisClosedFixingSubgroupOfEmbedding K L i)
        (fixingSubgroupLeBase K (SeparableClosure K)
          (finiteGaloisFieldRangeOfEmbedding K L i))).index =
      Module.finrank K L

def

finiteGaloisFieldRange

L170 ↗

LocalClassFieldTheory.finiteGaloisFieldRange

Documentation

The embedded copy of L inside the fixed separable closure.

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisFieldRange : IntermediateField K (SeparableClosure K)

def

finiteGaloisFieldRangeEquiv

L175 ↗

LocalClassFieldTheory.finiteGaloisFieldRangeEquiv

Documentation

The chosen embedding identifies L with its actual field range.

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisFieldRangeEquiv :
    L ≃ₐ[K] finiteGaloisFieldRange K L

instance

finiteGaloisFieldRange_isGalois

L181 ↗

LocalClassFieldTheory.finiteGaloisFieldRange_isGalois

Documentation

The canonical realization of a finite Galois extension is Galois over the base field.

Source context 4 commands

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

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

Lean source · statement

instance finiteGaloisFieldRange_isGalois :
    IsGalois K (finiteGaloisFieldRange K L)

instance

finiteGaloisFieldRange_finiteDimensional

L187 ↗

LocalClassFieldTheory.finiteGaloisFieldRange_finiteDimensional

Documentation

The canonical realization of a finite extension is finite-dimensional over the base field.

Source context 4 commands

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

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

Lean source · statement

instance finiteGaloisFieldRange_finiteDimensional :
    FiniteDimensional K (finiteGaloisFieldRange K L)

def

finiteGaloisClosedFixingSubgroup

L194 ↗

LocalClassFieldTheory.finiteGaloisClosedFixingSubgroup

Documentation

The concrete closed subgroup of the absolute separable Galois group attached to L/K.

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisClosedFixingSubgroup :
    ClosedSubgroup (Gal(SeparableClosure K / K))

instance

finiteGaloisExtensionSubgroup_normal

L200 ↗

LocalClassFieldTheory.finiteGaloisExtensionSubgroup_normal

Documentation

The fixing subgroup of the canonical finite Galois realization is normal.

Source context 4 commands

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

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

Lean source · statement

instance finiteGaloisExtensionSubgroup_normal :
    (extensionSubgroup
      (closedFixingSubgroup K (SeparableClosure K)
        (⊥ : IntermediateField K (SeparableClosure K)))
      (finiteGaloisClosedFixingSubgroup K L)
      (fixingSubgroupLeBase K (SeparableClosure K)
        (finiteGaloisFieldRange K L))).Normal

def

finiteGaloisUnitsEquivAbstractFixed

L219 ↗

LocalClassFieldTheory.finiteGaloisUnitsEquivAbstractFixed

Documentation

The actual coefficient group fixed by the concrete subgroup attached to L/K is canonically Lˣ.

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisUnitsEquivAbstractFixed :
    Additive Lˣ ≃+
      ambientFixedAddSubgroup
        (galoisAmbientUnitsRep K (SeparableClosure K))
        (finiteGaloisClosedFixingSubgroup K L)

theorem

finiteGaloisUnitsEquivAbstractFixed_coe

L230 ↗

LocalClassFieldTheory.finiteGaloisUnitsEquivAbstractFixed_coe

Documentation

The canonical fixed-module equivalence sends a unit through the chosen embedding.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory
noncomputable section
variable (K L : Type) [Field K] [Field L] [Algebra K L]
  [FiniteDimensional K L] [IsGalois K L]
omit [FiniteDimensional K L] in

Lean source · statement

theorem finiteGaloisUnitsEquivAbstractFixed_coe (x : Lˣ) :
    (finiteGaloisUnitsEquivAbstractFixed K L (Additive.ofMul x)).1 =
      Additive.ofMul
        (Units.map
          (AlgebraicNumberTheory.separableEmbeddingIntoSeparableClosure K L).toRingHom.toMonoidHom
            x)

def

finiteGaloisAbstractQuotientEquivGaloisGroup

L240 ↗

LocalClassFieldTheory.finiteGaloisAbstractQuotientEquivGaloisGroup

Documentation

For the concrete realization of L/K, the exact quotient used by the abstract class-formation framework is canonically the actual Galois group Gal(L/K).

Source context 4 commands

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

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

Lean source · statement

def finiteGaloisAbstractQuotientEquivGaloisGroup :
    ((closedFixingSubgroup K (SeparableClosure K)
        (⊥ : IntermediateField K (SeparableClosure K))).toSubgroup ⧸
      extensionSubgroup
        (closedFixingSubgroup K (SeparableClosure K)
          (⊥ : IntermediateField K (SeparableClosure K)))
        (finiteGaloisClosedFixingSubgroup K L)
        (fixingSubgroupLeBase K (SeparableClosure K)
          (finiteGaloisFieldRange K L))) ≃*
      Gal(L / K)

theorem

finiteGaloisExtensionSubgroup_index_eq_finrank

L254 ↗

LocalClassFieldTheory.finiteGaloisExtensionSubgroup_index_eq_finrank

Documentation

The chosen realization has subgroup index equal to [L : K].

Source context 4 commands

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

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

Lean source · statement

theorem finiteGaloisExtensionSubgroup_index_eq_finrank :
    (extensionSubgroup
      (closedFixingSubgroup K (SeparableClosure K)
        (⊥ : IntermediateField K (SeparableClosure K)))
      (finiteGaloisClosedFixingSubgroup K L)
      (fixingSubgroupLeBase K (SeparableClosure K)
        (finiteGaloisFieldRange K L))).index =
      Module.finrank K L

Module documentation

Finite local reciprocity: realizing finite Galois extensions in a separable closure

Realization relative to an explicit embedding

The chosen realization

Declarations