Module

Theorem6Dot7FieldSlimExamples.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot7FieldSlimExamples

7 declarations indexed from sourceView source ↗

Module documentation

Applications of the field slimness criterion

Example 6.7 of Yamaguchi, arXiv:2610.05634v1. The toral Kummer condition is imposed on actual units of every finite extension. The higher-local-field Artin--Schreier condition follows directly from the first discrete valuation, using a reciprocal uniformizer.

Imports11

Imported by1

Nyll.Yamaguchi26AbfaithfulGalois.All

def

IsTorallyKummerFaithful

L37 ↗

Yamaguchi26AbfaithfulGalois.IsTorallyKummerFaithful

Documentation

The unit formulation of toral Kummer-faithfulness: no finite extension has a nonidentity unit in every positive-power subgroup. The characteristic-zero hypothesis of Example 6.7(1) is imposed in the application below.

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

def IsTorallyKummerFaithful (K : Type u) [Field K] : Prop

theorem

finite_primaryComponent

L43 ↗

Yamaguchi26AbfaithfulGalois.IsTorallyKummerFaithful.finite_primaryComponent

Documentation

The roots-of-unity hypothesis in Corollary 6.6 follows from the toral Kummer condition on the actual finite extension.

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 IsTorallyKummerFaithful.finite_primaryComponent
    {K : Type u} [Field K] (hK : IsTorallyKummerFaithful K)
    (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L]
    (p : ℕ) [Fact p.Prime] :
    Finite (CommGroup.primaryComponent Lˣ p)

theorem

torallyKummerFaithful_finiteStepSolvable_slim

L52 ↗

Yamaguchi26AbfaithfulGalois.torallyKummerFaithful_finiteStepSolvable_slim

Documentation

Example 6.7(1): an ab-faithful torally Kummer-faithful field of characteristic zero has slim finite-step solvable Galois quotients.

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 torallyKummerFaithful_finiteStepSolvable_slim
    (K : Type u) [Field K] [CharZero K]
    (hK : IsTorallyKummerFaithful K)
    (hG : IsAbFaithful Gal(AlgebraicClosure K/K)) :
    ∀ m : ℕ, 2 ≤ m →
      IsSlim (MaxSolvQuot Gal(AlgebraicClosure K/K) m)

theorem

subpadic_finiteStepSolvable_slim

L68 ↗

Yamaguchi26AbfaithfulGalois.subpadic_finiteStepSolvable_slim

Documentation

Example 6.7(2): every field embedding into a finitely generated extension of Q_p has slim finite-step solvable absolute Galois quotients.

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 subpadic_finiteStepSolvable_slim
    (p : ℕ) [Fact p.Prime] (K : Type u) (E : Type v)
    [Field K] [Field E] [Algebra (Padic p) E] [Algebra.EssFiniteType (Padic p) E]
    (f : K →+* E) :
    ∀ m : ℕ, 2 ≤ m → IsSlim (MaxSolvQuot Gal(AlgebraicClosure K/K) m)

theorem

finitelyGenerated_finiteStepSolvable_slim

L88 ↗

Yamaguchi26AbfaithfulGalois.finitelyGenerated_finiteStepSolvable_slim

Documentation

An earlier application: every infinite field finitely generated over its prime field has slim finite-step solvable absolute Galois quotients.

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 finitelyGenerated_finiteStepSolvable_slim
    (K : Type u) [Field K] [Infinite K] (hfg : Field.FG K) :
    ∀ m : ℕ, 2 ≤ m → IsSlim (MaxSolvQuot Gal(AlgebraicClosure K/K) m)

theorem

higherLocalField_exists_not_artinSchreier

L102 ↗

Yamaguchi26AbfaithfulGalois.higherLocalField_exists_not_artinSchreier

Documentation

A positive-dimensional higher local field satisfies the Artin--Schreier condition needed for the field criterion, in positive characteristic.

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 higherLocalField_exists_not_artinSchreier
    (n : ℕ) (K : Type u) [Field K]
    (hK : ValuationTheory.IsHigherLocalField.{u, v} n K) (hn : 0 < n)
    (hchar : ringChar K ≠ 0) :
    ∃ a : K, ∀ x : K, x ^ ringChar K - x ≠ a

theorem

higherLocalField_finiteStepSolvable_slim

L114 ↗

Yamaguchi26AbfaithfulGalois.higherLocalField_finiteStepSolvable_slim

Documentation

Example 6.7(3): positive-dimensional higher local fields have slim finite-step solvable absolute Galois quotients.

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 higherLocalField_finiteStepSolvable_slim
    (n : ℕ) (K : Type u) [Field K]
    (hK : ValuationTheory.IsHigherLocalField.{u, v} n K) (hn : 0 < n) :
    ∀ m : ℕ, 2 ≤ m →
      IsSlim (MaxSolvQuot Gal(AlgebraicClosure K/K) m)

Module documentation

Applications of the field slimness criterion

Declarations

IsTorallyKummerFaithful

finite_primaryComponent

torallyKummerFaithful_finiteStepSolvable_slim

subpadic_finiteStepSolvable_slim

finitelyGenerated_finiteStepSolvable_slim

higherLocalField_exists_not_artinSchreier

higherLocalField_finiteStepSolvable_slim