Module

ResidueZeroUnramifiedFaithfulness.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.ResidueZeroUnramifiedFaithfulness

2 declarations indexed from sourceView source ↗

Module documentation

Detection through the actual residue Galois quotient

Residue ab-faithfulness detects quotient conjugation on every open normal subgroup that contains the actual inertia kernel.

Imports6

Imported by2

theorem

henselian_openNormal_faithful_of_inertia_le

L32 ↗

Yamaguchi26AbfaithfulGalois.henselian_openNormal_faithful_of_inertia_le

Documentation

An open normal subgroup containing the inertia kernel has faithful quotient conjugation whenever the actual residue Galois group is ab-faithful.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open IsLocalRing KummerTheory ValuationTheory.DiscreteValuationField
open ProCGroups.Abelian ProCGroups.FiniteStepSolvableQuotients
open RamificationTheory.HilbertRamification.ValuationSubring
universe u v w x

Lean source · statement

theorem henselian_openNormal_faithful_of_inertia_le
    {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
    (D : HenselianDVF.{u, w} K)
    {Γ : Type x} [LinearOrderedCommGroupWithZero Γ]
    (vΩ : _root_.Valuation Ω Γ) [D.valuation.HasExtension vΩ]
    (hres : IsAbFaithful Gal(ResidueField vΩ.valuationSubring/D.residueField))
    (N : OpenNormalSubgroup Gal(Ω/K))
    (hI : (henselianResidueAction D.valuation vΩ).ker ≤ (N : Subgroup Gal(Ω/K))) :
    Function.Injective (quotientConjugationTopologicalAbelianizationMap
      (N : Subgroup Gal(Ω/K)))

theorem

residueZero_openNormal_faithful_of_inertia_le

L54 ↗

Yamaguchi26AbfaithfulGalois.residueZero_openNormal_faithful_of_inertia_le