Module

PositiveCharacteristic.lean

Nyll.Yamaguchi26AbfaithfulGalois.HigherLocalField.PositiveCharacteristic

2 declarations indexed from sourceView source ↗

Module documentation

Positive-characteristic ab-faithfulness of higher local fields

Finite extensions inherit the higher local field structure. On every open Galois layer, prime-degree detection follows from Artin--Schreier classes over the complete discrete valuation at the first level. No embedding-problem solvability result is used.

Imports6

Imported by2

theorem

higherLocal_openLayer_residual_faithful

L32 ↗

Yamaguchi26AbfaithfulGalois.higherLocal_openLayer_residual_faithful

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups ProCGroups.ProC ProCGroups.Abelian
open ProCGroups.FiniteStepSolvableQuotients
universe u v
attribute [local instance] KummerTheory.fixingSubgroup_normal

Lean source · statement

theorem higherLocal_openLayer_residual_faithful
    (n : ℕ) {K Ω : Type u} [Field K] [Field Ω] [Algebra K Ω] [IsSepClosure K Ω]
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (hK : ValuationTheory.IsHigherLocalField.{u, v} n K) (hn : 0 < n)
    (H : OpenSubgroup Gal(Ω/K))
    [CompactSpace (H : Subgroup Gal(Ω/K))]
    (N : OpenNormalSubgroup (H : Subgroup Gal(Ω/K)))
    (hprime : (N : Subgroup (H : Subgroup Gal(Ω/K))).index.Prime) :
    Function.Injective (residualAbelianizationQuotientConjugation
      (FiniteGroupClass.sigmaGroup_fullFormation {p})
      (N : Subgroup (H : Subgroup Gal(Ω/K))) N.isClosed)

theorem

higher_local_field_abFaithful_of_charP

L88 ↗

Yamaguchi26AbfaithfulGalois.higher_local_field_abFaithful_of_charP

Documentation

Every positive-dimensional higher local field of positive characteristic is ab-faithful. The proof detects every prime-order residual action directly.