NYLL
Module

CompletionComparison.lean

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

Module documentation

Absolute Galois groups and their pro-p quotients across completion

The maximal pro-p quotient is the actual quotient by the pro-p residual core. The absolute Galois comparison carries this core onto the corresponding core of the completion, giving a continuous group isomorphism and preserving ab-faithfulness in every characteristic.

Imports6
Imported by1

Declarations

def

completionMaximalProPGaloisEquiv

L34 ↗
Yamaguchi26AbfaithfulGalois.completionMaximalProPGaloisEquiv
Documentation

Completion identifies the actual maximal pro-p quotients of the absolute Galois groups. The prime need not equal the residue characteristic.

Source context 5 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField
open ProCGroups ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
universe u
Lean source · statement
def completionMaximalProPGaloisEquiv
    {K : Type u} [Field K] (base : HenselianDVF K) (p : ℕ) [Fact p.Prime] :
    (Field.absoluteGaloisGroup K ⧸
      proCResidualCore (FiniteGroupClass.pGroup p) (Field.absoluteGaloisGroup K)) ≃ₜ*
    (Field.absoluteGaloisGroup base.valuation.Completion ⧸
      proCResidualCore (FiniteGroupClass.pGroup p)
        (Field.absoluteGaloisGroup base.valuation.Completion))
theorem

isAbFaithful_maximalProPGaloisGroup_iff_completion

L60 ↗
Yamaguchi26AbfaithfulGalois.isAbFaithful_maximalProPGaloisGroup_iff_completion
Documentation

Ab-faithfulness of the maximal pro-p absolute Galois quotient of a Henselian DVF is equivalent to that of its actual completion.

Source context 5 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField
open ProCGroups ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
universe u
Lean source · statement
theorem isAbFaithful_maximalProPGaloisGroup_iff_completion
    {K : Type u} [Field K] (base : HenselianDVF K) (p : ℕ) [Fact p.Prime] :
    IsAbFaithful (Field.absoluteGaloisGroup K ⧸
      proCResidualCore (FiniteGroupClass.pGroup p) (Field.absoluteGaloisGroup K)) ↔
    IsAbFaithful (Field.absoluteGaloisGroup base.valuation.Completion ⧸
      proCResidualCore (FiniteGroupClass.pGroup p)
        (Field.absoluteGaloisGroup base.valuation.Completion))
theorem

isAbFaithful_absoluteGaloisGroup_iff_completion

L71 ↗
Yamaguchi26AbfaithfulGalois.isAbFaithful_absoluteGaloisGroup_iff_completion
Documentation

Ab-faithfulness of the absolute Galois group of a Henselian DVF is equivalent to that of its completion, in every characteristic.

Source context 5 commands

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

noncomputable section
namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField
open ProCGroups ProCGroups.ProC ProCGroups.FiniteStepSolvableQuotients
universe u
Lean source · statement
theorem isAbFaithful_absoluteGaloisGroup_iff_completion
    {K : Type u} [Field K] (base : HenselianDVF K) :
    IsAbFaithful (Field.absoluteGaloisGroup K) ↔
      IsAbFaithful (Field.absoluteGaloisGroup base.valuation.Completion)

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