Module

Theorem3Dot6MixedCharacteristic.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem3Dot6MixedCharacteristic

1 declaration indexed from sourceView source ↗

Module documentation

Mixed-characteristic discrete valuations

Theorem 3.6 of Yamaguchi, arXiv:2610.05634v1. Its first assertion is stated on the actual quotient G_Lᵃᵇ/p.

Imports10

Imported by3

theorem

mixed_characteristic_properties_3_6

L37 ↗

Yamaguchi26AbfaithfulGalois.mixed_characteristic_properties_3_6

Documentation

For each finite Galois extension of a mixed-characteristic discretely valued field, the conjugation action on the mod-p abelianization is faithful. Consequently its absolute Galois group is p-ab-faithful.

Source context 4 commands

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

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

Lean source · statement

theorem mixed_characteristic_properties_3_6
    (K : Type u) [Field K] [CharZero K]
    (base : DVF.{u, v} K) (p : ℕ) [Fact p.Prime]
    [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) ∧
      IsSigmaAbFaithful {p} Gal(AlgebraicClosure K/K)

Module documentation

Mixed-characteristic discrete valuations

Declarations

mixed_characteristic_properties_3_6