Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicCompletionDetection

Module documentation

Detecting prime-degree automorphisms through a stable completion

When a prolongation is invariant under the Galois group, its completion has the same Galois degree. The complete-field detection theorem detects an automorphism there, and the injective weak-approximation map transports the detection to the original field.

theorem

prime_order_detection_of_stable_valuation

L30 ↗

Yamaguchi26AbfaithfulGalois.prime_order_detection_of_stable_valuation

Documentation

A prime-degree extension with invariant prolongation is detected by its completed extension and the injection on mod-prime abelianizations.

Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ValuationTheory.DiscreteValuationField ProCGroups.Abelian
open Field.absoluteGaloisGroup
universe u v

Lean source · statement

theorem prime_order_detection_of_stable_valuation
    {K L : Type u} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    [CharZero K] (base : DVF.{u, v} K) (target : DVF.{u, v} L)
    [base.valuation.HasExtension target.valuation]
    (p r : ℕ) [Fact p.Prime] [Fact r.Prime]
    [CharP base.residueField p]
    (hdegree : Module.finrank K L = r)
    (hstable : ∀ τ : Gal(L/K),
      target.valuation.IsEquiv (target.valuation.comap τ.toRingEquiv.toRingHom)) :
    ∃ τ : Gal(L/K), τ ≠ 1 ∧
      ∃ z : abelianModPower Gal(AlgebraicClosure L/L) p,
        relativeGaloisAbelianModPowerTransform K L p τ z ≠ z

Module documentation

Detecting prime-degree automorphisms through a stable completion

Declarations

prime_order_detection_of_stable_valuation