Module

ResidueZeroFaithfulness.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.ResidueZeroFaithfulness

2 declarations indexed from sourceView source ↗

Module documentation

Ab-faithfulness over residue-zero Henselian valuations

Ab-faithfulness of the residue Galois group and finite primary root groups in its finite field extensions imply ab-faithfulness of the absolute Galois group of the Henselian discretely valued field.

Imports6

Imported by3

theorem

residueZero_openLayer_prime_index_faithful

L29 ↗

Yamaguchi26AbfaithfulGalois.residueZero_openLayer_prime_index_faithful

Source context 4 commands

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

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

Lean source · statement

theorem residueZero_openLayer_prime_index_faithful
    {K Ω : Type u} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K]
    (D : HenselianDVF.{u, v} K) [CharZero D.residueField]
    (hres : IsAbFaithful Gal(AlgebraicClosure D.residueField/D.residueField))
    (hroots : ∀ (E : Type u) [Field E] [Algebra D.residueField E]
      [FiniteDimensional D.residueField E] (p : ℕ), p.Prime →
      Finite (CommGroup.primaryComponent Eˣ p))
    (H : OpenSubgroup Gal(Ω/K))
    (N : OpenNormalSubgroup (H : Subgroup Gal(Ω/K)))
    (hprime : (N : Subgroup (H : Subgroup Gal(Ω/K))).index.Prime) :
    Function.Injective (quotientConjugationTopologicalAbelianizationMap
      (N : Subgroup (H : Subgroup Gal(Ω/K))))

theorem

residueZero_abFaithful_of_finitePrimePowerRoots

L89 ↗

Yamaguchi26AbfaithfulGalois.residueZero_abFaithful_of_finitePrimePowerRoots

Documentation

Finite primary root groups in every finite residue extension imply ab-faithfulness over a residue-zero Henselian discrete valuation.