NYLL
Module

Theorem6Dot6AbsoluteCenter.lean

Nyll.Yamaguchi26AbfaithfulGalois.Theorem6Dot6AbsoluteCenter
2 declarations indexed from sourceView source ↗

Module documentation

Center-freeness and slimness for absolute Galois groups

Yamaguchi, arXiv:2610.05634v1, Corollary 6.6. Cyclotomic and trivial orientations supply formal Hilbert 90; no orientation or cohomology hypothesis is added to the field statement.

Imports6
Imported by1

Declarations

theorem

absoluteGalois_finiteStepSolvable_centerfree

L30 ↗
Yamaguchi26AbfaithfulGalois.absoluteGalois_finiteStepSolvable_centerfree
Documentation

Corollary 6.6: ab-faithfulness implies center-free finite-step solvable quotients in every characteristic.

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_centerfree
    (K : Type u) [Field K]
    (hG : IsAbFaithful Gal(AlgebraicClosure K/K)) :
    ∀ m : ℕ, 2 ≤ m →
      Subgroup.center (MaxSolvQuot Gal(AlgebraicClosure K/K) m) = ⊥
theorem

absoluteGalois_finiteStepSolvable_slim_of_cyclotomic_and_cyclic_extensions

L50 ↗
Yamaguchi26AbfaithfulGalois.absoluteGalois_finiteStepSolvable_slim_of_cyclotomic_and_cyclic_extensions
Documentation

The slimness assertion of Corollary 6.6, with the current manuscript's infinite cyclotomic extensions and cyclic degree-p extensions as 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_cyclotomic_and_cyclic_extensions
    (K : Type u) [Field K]
    (hG : IsAbFaithful Gal(AlgebraicClosure K/K))
    (hCyclotomic : ∀ p : ℕ, p.Prime → ringChar K ≠ p →
      ¬ FiniteDimensional K (primaryCyclotomicExtension K p))
    (hCyclic : ∀ p : ℕ, p.Prime → ringChar K = p →
      ∃ L : IntermediateField K (SeparableClosure K),
        IsGalois K L ∧ Module.finrank K L = p) :
    ∀ 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.