NYLL
Module

FieldSlim.lean

Nyll.Yamaguchi26AbfaithfulGalois.FormalHilbert90.FieldSlim
1 declaration indexed from sourceView source ↗

Module documentation

A field criterion for slim finite-step solvable quotients

The earlier roots-of-unity / Artin–Schreier form of the field criterion. The current extension-based statement is in Theorem6Dot6AbsoluteCenter.lean. The roots-of-unity condition concerns every finite extension inside the chosen algebraic closure and each prime distinct from the characteristic. The positive-characteristic condition states that the Artin--Schreier map is not surjective.

Imports6
Imported by2

Declarations

theorem

absoluteGalois_finiteStepSolvable_slim_of_roots_and_artinSchreier

L32 ↗
Yamaguchi26AbfaithfulGalois.absoluteGalois_finiteStepSolvable_slim_of_roots_and_artinSchreier
Documentation

Field slimness under finite-root and Artin--Schreier hypotheses.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ProCGroups.FiniteStepSolvableQuotients
universe u
Lean source · statement
theorem absoluteGalois_finiteStepSolvable_slim_of_roots_and_artinSchreier
    (K : Type u) [Field K]
    (hG : IsAbFaithful Gal(AlgebraicClosure K/K))
    (hRoots : ∀ (L : IntermediateField K (AlgebraicClosure K)),
      FiniteDimensional K L →
      ∀ (ℓ : ℕ), ℓ.Prime → ringChar K ≠ ℓ →
        Finite (CommGroup.primaryComponent Lˣ ℓ))
    (hAS : ringChar K ≠ 0 →
      ∃ a : K, ∀ x : K, x ^ ringChar K - x ≠ a) :
    ∀ m : ℕ, 2 ≤ m →
      IsSlim (MaxSolvQuot Gal(AlgebraicClosure K/K) m)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.