NYLL
Module

FiniteGaloisPrimeDegreeReduction.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.FiniteGaloisPrimeDegreeReduction
3 declarations indexed from sourceView source ↗

Module documentation

Reducing finite Galois faithfulness to prime degree

Prime-degree detection yields faithful mod-prime abelianization actions for finite Galois extensions by passing to fixed fields of prime-order subgroups in a hypothetical kernel.

Imports6
Imported by2

Declarations

def

relativeModPowerAction

L30 ↗
Yamaguchi26AbfaithfulGalois.relativeModPowerAction
Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
open ValuationTheory.DiscreteValuationField
universe u v
Lean source · full declaration
def relativeModPowerAction
    (K L : Type u) [Field K] [Field L] [Algebra K L] (p : ℕ) :
    Gal(L/K) →* MulAut (abelianModPower Gal(AlgebraicClosure L/L) p) where
  toFun τ := powerQuotientAction p (absoluteGaloisAbelianizationAction τ.toRingEquiv)
  map_one' := by
    change powerQuotientAction p (absoluteGaloisAbelianizationAction 1) = 1
    rw [map_one, map_one]
  map_mul' τ σ := by
    change powerQuotientAction p
      (absoluteGaloisAbelianizationAction (τ.toRingEquiv * σ.toRingEquiv)) = _
    rw [map_mul, map_mul]
theorem

relativeModPowerAction_apply

L42 ↗
Yamaguchi26AbfaithfulGalois.relativeModPowerAction_apply
Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
open ValuationTheory.DiscreteValuationField
universe u v
Lean source · statement
theorem relativeModPowerAction_apply
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    (p : ℕ) (τ : Gal(L/K)) (z : abelianModPower Gal(AlgebraicClosure L/L) p) :
    relativeModPowerAction K L p τ z =
      relativeGaloisAbelianModPowerTransform K L p τ z
theorem

relativeGaloisAbelianModPowerTransform_faithful_of_primeDegree_detection

L58 ↗
Yamaguchi26AbfaithfulGalois.relativeGaloisAbelianModPowerTransform_faithful_of_primeDegree_detection
Documentation

Prime-degree detection makes the actual mod-p action faithful for every finite Galois extension. A prime-order subgroup of the kernel would give a prime-degree extension over its fixed field, contradicting detection there.

Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
open ValuationTheory.DiscreteValuationField
universe u v
Lean source · statement
theorem relativeGaloisAbelianModPowerTransform_faithful_of_primeDegree_detection
    (p : ℕ) [Fact p.Prime]
    (hdetect : ∀ (F E : Type u) [Field F] [Field E] [Algebra F E]
      [IsGalois F E] [CharZero F]
      (base : DVF.{u, v} F) [CharP base.residueField p]
      (r : ℕ) [Fact r.Prime], Module.finrank F E = r →
        ∃ τ : Gal(E/F), τ ≠ 1 ∧
          ∃ z : abelianModPower Gal(AlgebraicClosure E/E) p,
            relativeGaloisAbelianModPowerTransform F E p τ z ≠ z)
    {K : Type u} [Field K] [CharZero K]
    (base : DVF.{u, v} K) [CharP base.residueField p]
    (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] :
    ∀ τ : Gal(L/K),
      (∀ z : abelianModPower Gal(AlgebraicClosure L/L) p,
        relativeGaloisAbelianModPowerTransform K L p τ z = z) → τ = 1

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