Module

ResidueZeroFiniteRoots.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.ResidueZeroFiniteRoots

2 declarations indexed from sourceView source ↗

Module documentation

Finite residue root groups from slimness

Slimness over a residue-zero Henselian discrete valuation forces finite primary root groups in every finite residue extension. Ab-faithfulness provides the corresponding specialization.

Imports8

Imported by2

theorem

finitePrimePowerRoots_of_residueZero_slim

L34 ↗

Yamaguchi26AbfaithfulGalois.finitePrimePowerRoots_of_residueZero_slim

Documentation

Slimness over a residue-zero Henselian DVF forces finite primary root groups in every finite residue extension.

Source context 4 commands

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

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

Lean source · statement

theorem finitePrimePowerRoots_of_residueZero_slim
    {K : Type u} [Field K] (D : HenselianDVF.{u, v} K) [CharZero D.residueField]
    (hK : IsSlim Gal(AlgebraicClosure K/K))
    (E : Type u) [Field E] [Algebra D.residueField E] [FiniteDimensional D.residueField E]
    (p : ℕ) (hp : p.Prime) : Finite (CommGroup.primaryComponent Eˣ p)

theorem

finitePrimePowerRoots_of_residueZero_abFaithful

L75 ↗

Yamaguchi26AbfaithfulGalois.finitePrimePowerRoots_of_residueZero_abFaithful