Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicReduction

Module documentation

Prime-degree reduction for mixed-characteristic valuations

An unnumbered auxiliary reduction for Section 3 of Yamaguchi, arXiv:2610.05634v1. The hypothesis is made on the actual quotient G_Lᵃᵇ/p for every mixed-characteristic discretely valued field and every prime-degree Galois extension. Finite extensions preserve discreteness and residue characteristic, allowing the prime-order test to be applied on every open layer.

theorem

mixed_characteristic_reduction

L43 ↗

Yamaguchi26AbfaithfulGalois.mixed_characteristic_reduction

Documentation

A finite extension with any prolongation of a mixed-characteristic discrete valuation remains discretely valued of the same residue characteristic. Prime-degree nontriviality then suffices for singleton-p-ab-faithfulness over all such fields.

Source context 5 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ValuationTheory.DiscreteValuationField ProCGroups.Abelian
open ProCGroups.FiniteStepSolvableQuotients
universe u v w

Lean source · statement

theorem mixed_characteristic_reduction
    (p : ℕ) [Fact p.Prime] :
    (∀ (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]
        (Γ : Type w) [LinearOrderedCommGroupWithZero Γ]
        (vL : Valuation L Γ),
        base.valuation.HasExtension vL →
          ringChar L = 0 ∧ vL.IsRankOneDiscrete ∧
            CharP (IsLocalRing.ResidueField vL.valuationSubring) p) ∧
      ((∀ (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],
          IsSigmaAbFaithful {p} Gal(AlgebraicClosure K/K))

Module documentation

Prime-degree reduction for mixed-characteristic valuations

Declarations

mixed_characteristic_reduction