NYLL
Module

MixedCharAllPrimeCompleteDetection.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.Concrete.MixedCharAllPrimeCompleteDetection
1 declaration indexed from sourceView source ↗

Module documentation

Faithful p-power cohomology for every prime extension degree

The residue prime controls the coefficients. The Galois extension degree can be any prime: residue-prime degree uses wild detection, while a different prime degree is already detected at the first p-power level.

Imports2
Imported by2

Declarations

theorem

exists_faithful_relativeH1Action_of_complete_mixedChar_prime_order

L25 ↗
ClassFieldTower.Martinet.Shafarevich.exists_faithful_relativeH1Action_of_complete_mixedChar_prime_order
Documentation

Every prime-degree Galois extension of a complete mixed-characteristic DVF has faithful action on its absolute H¹ at some positive p-power level. The extension degree and the residue prime need not agree.

Source context 2 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ValuationTheory.DiscreteValuationField
Lean source · statement
theorem exists_faithful_relativeH1Action_of_complete_mixedChar_prime_order
    {F K : Type*} [Field F] [Field K] [Algebra F K] [IsGalois F K] [CharZero F]
    (vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete vF]
    (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField vF.valuationSubring) p]
    {r : ℕ} [Fact r.Prime] (hdegree : Module.finrank F K = r) :
    ∃ s : ℕ, 1 ≤ s ∧ Function.Injective (relativeGaloisH1Action (n := p ^ s) F K)

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