Module

Properties.lean

Nyll.Yamaguchi26AbfaithfulGalois.HigherLocalField.Properties

3 declarations indexed from sourceView source ↗

Module documentation

Prime-power roots of unity and ab-faithfulness in higher local fields

The stronger joint root-finiteness and ab-faithfulness statement supporting Theorem 4.2 of Yamaguchi, arXiv:2610.05634v1.

Imports10

Nyll.Yamaguchi26AbfaithfulGalois.HigherLocalField.Basic
Nyll.Yamaguchi26AbfaithfulGalois.HigherLocalField.PositiveCharacteristic
Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.Faithful
Nyll.Yamaguchi26AbfaithfulGalois.GroupTheory.SigmaOrdinary
Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicFaithfulness
Nyll.Yamaguchi26AbfaithfulGalois.Kummer.ResidueZeroFaithfulness
Mathlib.Algebra.CharP.Defs
Mathlib.FieldTheory.AbsoluteGaloisGroup
Mathlib.FieldTheory.Galois.Profinite
Mathlib.GroupTheory.Torsion

Imported by3

theorem

finite_primaryComponent_of_higherLocalField

L32 ↗

Yamaguchi26AbfaithfulGalois.finite_primaryComponent_of_higherLocalField

Documentation

Every primary root group of a higher local field is finite.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u v

Lean source · statement

theorem finite_primaryComponent_of_higherLocalField
    (n : ℕ) (K : Type u) [Field K]
    (hK : ValuationTheory.IsHigherLocalField.{u, v} n K) :
    ∀ (ℓ : ℕ), ℓ.Prime → Finite (CommGroup.primaryComponent Kˣ ℓ)

theorem

higher_local_field_abFaithful_of_charZero

L53 ↗

Yamaguchi26AbfaithfulGalois.higher_local_field_abFaithful_of_charZero

Documentation

The characteristic-zero induction uses mixed-characteristic faithfulness at the first positive residue characteristic and the residue-zero lifting theorem at each preceding level.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u v

Lean source · statement

theorem higher_local_field_abFaithful_of_charZero
    (n : ℕ) (K : Type u) [Field K] [CharZero K]
    (hK : ValuationTheory.IsHigherLocalField.{u, v} n K) (hn : 0 < n) :
    IsAbFaithful Gal(AlgebraicClosure K/K)

theorem

higher_local_field_roots_and_abFaithful

L83 ↗

Yamaguchi26AbfaithfulGalois.higher_local_field_roots_and_abFaithful

Documentation

Every higher local field has finitely many roots of ℓ-power order for each prime ℓ. In positive dimension its absolute Galois group is ab-faithful.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u v

Lean source · statement

theorem higher_local_field_roots_and_abFaithful
    (n : ℕ) (K : Type u) [Field K]
    (hK : ValuationTheory.IsHigherLocalField.{u, v} n K) :
    (∀ (ℓ : ℕ), ℓ.Prime → Finite (CommGroup.primaryComponent Kˣ ℓ)) ∧
      (0 < n → IsAbFaithful Gal(AlgebraicClosure K/K))

Module documentation

Prime-power roots of unity and ab-faithfulness in higher local fields

Declarations

finite_primaryComponent_of_higherLocalField

higher_local_field_abFaithful_of_charZero

higher_local_field_roots_and_abFaithful