NYLL
Module

MixedCharacteristicFaithfulness.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicFaithfulness
3 declarations indexed from sourceView source ↗

Module documentation

Sigma-ab-faithfulness in mixed characteristic

Each open absolute Galois subgroup is the absolute group of its actual finite fixed field. Its Henselian discrete valuation and residue prime are constructed from the base. Prime-index detection, including primes distinct from the residue characteristic, therefore applies on every open layer. The unrestricted prime-order criterion gives the full singleton-p property.

Imports13
Imported by3

Declarations

theorem

mixedChar_openLayer_prime_index_faithful

L40 ↗
Yamaguchi26AbfaithfulGalois.mixedChar_openLayer_prime_index_faithful
Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField KummerTheory
open ClassFieldTower.Martinet.Shafarevich
open ProCGroups ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
universe u v

-- The fixed field need only be finite: no normality of this open layer is used.
Lean source · statement
theorem mixedChar_openLayer_prime_index_faithful
    {K Ω : Type u} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K]
    (base : HenselianDVF.{u, v} K) (p : ℕ) [Fact p.Prime] [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.pGroup_fullFormation p)
      (N : Subgroup (H : Subgroup Gal(Ω/K))) N.isClosed)
theorem

isSigmaAbFaithful_absoluteGaloisGroup_singleton_of_henselian_mixedChar

L87 ↗
Yamaguchi26AbfaithfulGalois.isSigmaAbFaithful_absoluteGaloisGroup_singleton_of_henselian_mixedChar
Documentation

A Henselian discrete valuation field of mixed characteristic (0,p) is singleton-p-ab-faithful, including all finite relative quotient orders.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField KummerTheory
open ClassFieldTower.Martinet.Shafarevich
open ProCGroups ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
universe u v

-- The fixed field need only be finite: no normality of this open layer is used.
Lean source · statement
theorem isSigmaAbFaithful_absoluteGaloisGroup_singleton_of_henselian_mixedChar
    {K : Type u} [Field K] [CharZero K]
    (base : HenselianDVF.{u, v} K) (p : ℕ) [Fact p.Prime] [CharP base.residueField p] :
    IsSigmaAbFaithful {p} Gal(AlgebraicClosure K/K)
theorem

isSigmaAbFaithful_absoluteGaloisGroup_and_maximalProSigma_of_henselian_mixedChar

L108 ↗
Yamaguchi26AbfaithfulGalois.isSigmaAbFaithful_absoluteGaloisGroup_and_maximalProSigma_of_henselian_mixedChar
Documentation

Every Sigma containing the residue prime gives full Sigma-ab-faithfulness, ordinary ab-faithfulness, and ordinary ab-faithfulness of the actual maximal pro-Sigma quotient.

Source context 5 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField KummerTheory
open ClassFieldTower.Martinet.Shafarevich
open ProCGroups ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
universe u v

-- The fixed field need only be finite: no normality of this open layer is used.
Lean source · statement
theorem isSigmaAbFaithful_absoluteGaloisGroup_and_maximalProSigma_of_henselian_mixedChar
    {K : Type u} [Field K] [CharZero K]
    (base : HenselianDVF.{u, v} K) (p : ℕ) [Fact p.Prime] [CharP base.residueField p]
    {sigma : Set ℕ} (hp : p ∈ sigma) :
    IsSigmaAbFaithful sigma Gal(AlgebraicClosure K/K) ∧
      IsAbFaithful Gal(AlgebraicClosure K/K) ∧
        IsAbFaithful (Gal(AlgebraicClosure K/K) ⧸
          proCResidualCore (FiniteGroupClass.sigmaGroup sigma) 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.