NYLL
Module

PrimeDegreeReduction.lean

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

Module documentation

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

Fixed-field comparison transports the actual mod-prime action to conjugation on the residual abelianization. Discrete prolongations supply the hypothesis on each open layer without completeness or Henselianity assumptions.

Imports11
Imported by3

Declarations

theorem

fixingSubgroup_residualAbelianization_ne_one_of_moved_mod_prime

L36 ↗
Yamaguchi26AbfaithfulGalois.fixingSubgroup_residualAbelianization_ne_one_of_moved_mod_prime
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
    {F Ω : Type u} [Field F] [Field Ω] [Algebra F Ω] [IsAlgClosure F Ω] [CharZero 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_openSubgroup_residualAbelianization_faithful

L81 ↗
Yamaguchi26AbfaithfulGalois.primeDegree_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 ValuationTheory.DiscreteValuationField ProCGroups.FiniteStepSolvableQuotients
Lean source · statement
theorem primeDegree_openSubgroup_residualAbelianization_faithful
    {F Ω : Type u} [Field F] [Field Ω] [Algebra F Ω] [IsAlgClosure F Ω] [CharZero 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_openLayer_residual_faithful

L115 ↗
Yamaguchi26AbfaithfulGalois.primeDegree_openLayer_residual_faithful
Source context 6 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 ValuationTheory.DiscreteValuationField ProCGroups.FiniteStepSolvableQuotients
universe v
Lean source · statement
theorem primeDegree_openLayer_residual_faithful
    (p : ℕ) [Fact p.Prime]
    (hdetect : ∀ (F E : Type u) [Field F] [Field E] [Algebra F E]
      [IsGalois F E] [CharZero F]
      (base : DVF.{u, v} F) [CharP base.residueField p]
      (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 Ω] [IsAlgClosure K Ω] [CharZero K]
    (base : DVF.{u, v} K) [CharP base.residueField p]
    (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

L170 ↗
Yamaguchi26AbfaithfulGalois.isSigmaAbFaithful_of_primeDegree_detection
Documentation

Prime-degree field detection gives Sigma-ab-faithfulness on every open layer.

Source context 6 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 ValuationTheory.DiscreteValuationField ProCGroups.FiniteStepSolvableQuotients
universe v
Lean source · statement
theorem isSigmaAbFaithful_of_primeDegree_detection
    (p : ℕ) [Fact p.Prime]
    (hdetect : ∀ (F E : Type u) [Field F] [Field E] [Algebra F E]
      [IsGalois F E] [CharZero F]
      (base : DVF.{u, v} F) [CharP base.residueField p]
      (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] [CharZero K]
    (base : DVF.{u, v} K) [CharP base.residueField p] :
    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.