NYLL
Module

MixedCharHenselianFaithfulness.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.MixedCharHenselianFaithfulness
3 declarations indexed from sourceView source ↗

Module documentation

Henselian mixed-characteristic faithfulness

The actual completion Galois equivalence carries an open normal subgroup to an open normal subgroup of the same index. Completion preserves the residue characteristic, and transport of residual conjugation returns faithfulness to the original Henselian field.

Imports10
Imported by3

Declarations

theorem

residualFaithfulness_of_complete_galois_equiv

L37 ↗
ClassFieldTower.Martinet.Shafarevich.residualFaithfulness_of_complete_galois_equiv
Source context 4 commands

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

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

-- Keep the complete target abstract so valuation-ring scalar towers are not
-- searched while transporting group actions. The completion equivalence is
-- constructed below before this helper is applied.
Lean source · statement
theorem residualFaithfulness_of_complete_galois_equiv
    {K D : Type u} [Field K] [Field D] [CharZero K] [CharZero D]
    (w : _root_.Valuation D (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete w] (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField w.valuationSubring) p]
    (e : Gal(AlgebraicClosure K/K) ≃ₜ* Gal(AlgebraicClosure D/D))
    (N : Subgroup Gal(AlgebraicClosure K/K)) [hNormal : N.Normal]
    (hN : IsOpen (N : Set Gal(AlgebraicClosure K/K))) {r : ℕ} [Fact r.Prime]
    (hindex : N.index = r) :
    Function.Injective (residualAbelianizationQuotientConjugation
      (FiniteGroupClass.pGroup_fullFormation p) N (N.isClosed_of_isOpen hN))
theorem

mixedChar_henselian_openSubgroup_faithful_of_integerValuation

L58 ↗
ClassFieldTower.Martinet.Shafarevich.mixedChar_henselian_openSubgroup_faithful_of_integerValuation
Documentation

Prime-order quotient conjugation is faithful over a Henselian DVF; no completeness assumption is required.

Source context 4 commands

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

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

-- Keep the complete target abstract so valuation-ring scalar towers are not
-- searched while transporting group actions. The completion equivalence is
-- constructed below before this helper is applied.
Lean source · statement
theorem mixedChar_henselian_openSubgroup_faithful_of_integerValuation
    {K : Type*} [Field K] [CharZero K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) [v.IsRankOneDiscrete]
    [HenselianRing v.valuationSubring (IsLocalRing.maximalIdeal v.valuationSubring)]
    (p : ℕ) [Fact p.Prime]
    [hres : CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (N : Subgroup Gal(AlgebraicClosure K/K)) [hNormal : N.Normal]
    (hN : IsOpen (N : Set Gal(AlgebraicClosure K/K))) {r : ℕ} [Fact r.Prime]
    (hindex : N.index = r) :
    Function.Injective (residualAbelianizationQuotientConjugation
      (FiniteGroupClass.pGroup_fullFormation p) N (N.isClosed_of_isOpen hN))
theorem

mixedChar_henselian_openSubgroup_residualAbelianization_faithful

L90 ↗
ClassFieldTower.Martinet.Shafarevich.mixedChar_henselian_openSubgroup_residualAbelianization_faithful
Documentation

The prime-order quotient action is faithful for an arbitrary value-group presentation of a Henselian DVF. Integer normalization preserves the actual valuation subring, hence its Henselian property and residue characteristic.

Source context 4 commands

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

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

-- Keep the complete target abstract so valuation-ring scalar towers are not
-- searched while transporting group actions. The completion equivalence is
-- constructed below before this helper is applied.
Lean source · statement
theorem mixedChar_henselian_openSubgroup_residualAbelianization_faithful
    {K Ω : Type u} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosure K Ω] [CharZero K]
    (base : HenselianDVF.{u, v} K) (p : ℕ) [Fact p.Prime] [hres : CharP base.residueField p]
    (N : Subgroup Gal(Ω/K)) [hNormal : N.Normal]
    (hN : IsOpen (N : Set Gal(Ω/K))) {r : ℕ} [Fact r.Prime]
    (hindex : N.index = r) :
    Function.Injective (residualAbelianizationQuotientConjugation
      (FiniteGroupClass.pGroup_fullFormation p) N (N.isClosed_of_isOpen hN))

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