Yamaguchi26AbfaithfulGalois.residueZero_abFaithful_slim_iff_finitePrimePowerRoots
Lemma 4.1: ab-faithfulness, slimness, and finiteness of every primary root group in every finite residue extension are equivalent.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
open ValuationTheory.DiscreteValuationField
universe u vLean source · statement
theorem residueZero_abFaithful_slim_iff_finitePrimePowerRoots
{K : Type u} [Field K] (D : HenselianDVF.{u, v} K)
[CharZero D.residueField]
(hres : IsAbFaithful Gal(AlgebraicClosure D.residueField/D.residueField)) :
(IsAbFaithful Gal(AlgebraicClosure K/K) ↔ IsSlim Gal(AlgebraicClosure K/K)) ∧
(IsSlim Gal(AlgebraicClosure K/K) ↔
∀ (E : Type u) [Field E] [Algebra D.residueField E]
[FiniteDimensional D.residueField E] (ℓ : ℕ),
ℓ.Prime → Finite (CommGroup.primaryComponent Eˣ ℓ))