NYLL
Module

PositiveCharacteristicPrimeDegreeReduction.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.PositiveCharacteristicPrimeDegreeReduction
4 declarations indexed from sourceView source ↗

Module documentation

From prime-degree field detection to Sigma-ab-faithfulness

Fixed fields in a separable closure give finite extensions even over imperfect fields. The actual comparison with the algebraic-closure absolute action transports prime-degree detection to every open Galois layer.

Imports13
Imported by3

Declarations

theorem

fixingSubgroup_residualAbelianization_ne_one_of_moved_mod_prime_separable

L39 ↗
Yamaguchi26AbfaithfulGalois.fixingSubgroup_residualAbelianization_ne_one_of_moved_mod_prime_separable
Documentation

A moved mod-prime class detects nontrivial residual conjugation on the fixing subgroup.

Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
attribute [local instance] KummerTheory.fixingSubgroup_normal
Lean source · statement
theorem fixingSubgroup_residualAbelianization_ne_one_of_moved_mod_prime_separable
    {F Ω : Type u} [Field F] [Field Ω] [Algebra F Ω] [IsSepClosure F Ω]
    (S : IntermediateField F Ω) [FiniteDimensional F S] [IsGalois F S]
    (p : ℕ) [Fact p.Prime] (τ : Gal(S/F))
    (z : abelianModPower Gal(AlgebraicClosure S/S) p)
    (hz : relativeGaloisAbelianModPowerTransform F S p τ z ≠ z) :
    residualAbelianizationQuotientConjugation
      (FiniteGroupClass.sigmaGroup_fullFormation {p}) S.fixingSubgroup
        (InfiniteGalois.fixingSubgroup_isClosed S) ≠ 1
theorem

primeDegree_separable_openSubgroup_residualAbelianization_faithful

L84 ↗
Yamaguchi26AbfaithfulGalois.primeDegree_separable_openSubgroup_residualAbelianization_faithful
Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
attribute [local instance] KummerTheory.fixingSubgroup_normal
open ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
theorem primeDegree_separable_openSubgroup_residualAbelianization_faithful
    {F Ω : Type u} [Field F] [Field Ω] [Algebra F Ω] [IsSepClosure F Ω]
    (p : ℕ) [Fact p.Prime] {r : ℕ} [Fact r.Prime]
    (hdetect : ∀ (S : IntermediateField F Ω) [IsGalois F S],
      Module.finrank F S = r →
        ∃ τ : Gal(S/F), ∃ z : abelianModPower Gal(AlgebraicClosure S/S) p,
          relativeGaloisAbelianModPowerTransform F S p τ z ≠ z)
    (N : Subgroup Gal(Ω/F)) [N.Normal]
    (hN : IsOpen (N : Set Gal(Ω/F))) (hindex : N.index = r) :
    Function.Injective (residualAbelianizationQuotientConjugation
      (FiniteGroupClass.sigmaGroup_fullFormation {p}) N (N.isClosed_of_isOpen hN))
theorem

primeDegree_separable_openLayer_residual_faithful

L117 ↗
Yamaguchi26AbfaithfulGalois.primeDegree_separable_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
universe u
attribute [local instance] KummerTheory.fixingSubgroup_normal
open ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
theorem primeDegree_separable_openLayer_residual_faithful
    (p : ℕ) [Fact p.Prime]
    (hdetect : ∀ (F E : Type u) [Field F] [Field E] [Algebra F E]
      [IsGalois F E] [CharP F p] [Infinite F], Field.FG F →
      ∀ (r : ℕ) [Fact r.Prime], Module.finrank F E = r →
        ∃ τ : Gal(E/F), τ ≠ 1 ∧
          ∃ z : abelianModPower Gal(AlgebraicClosure E/E) p,
            relativeGaloisAbelianModPowerTransform F E p τ z ≠ z)
    {K Ω : Type u} [Field K] [Field Ω] [Algebra K Ω] [IsSepClosure K Ω] [CharP K p] [Infinite K]
    (hfg : Field.FG K)
    (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

isSigmaAbFaithful_of_primeDegree_detection_fg_charP

L173 ↗
Yamaguchi26AbfaithfulGalois.isSigmaAbFaithful_of_primeDegree_detection_fg_charP
Documentation

Prime-degree detection on infinite finitely generated fields of characteristic p implies full singleton-p ab-faithfulness of their absolute Galois groups.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups ProCGroups.ProC ProCGroups.Abelian
universe u
attribute [local instance] KummerTheory.fixingSubgroup_normal
open ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
theorem isSigmaAbFaithful_of_primeDegree_detection_fg_charP
    (p : ℕ) [Fact p.Prime]
    (hdetect : ∀ (F E : Type u) [Field F] [Field E] [Algebra F E]
      [IsGalois F E] [CharP F p] [Infinite F], Field.FG F →
      ∀ (r : ℕ) [Fact r.Prime], Module.finrank F E = r →
        ∃ τ : Gal(E/F), τ ≠ 1 ∧
          ∃ z : abelianModPower Gal(AlgebraicClosure E/E) p,
            relativeGaloisAbelianModPowerTransform F E p τ z ≠ z)
    {K : Type u} [Field K] [CharP K p] [Infinite K] (hfg : Field.FG K) :
    IsSigmaAbFaithful {p} Gal(AlgebraicClosure K/K)

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