NYLL
Module

MixedCharPrimeToCompleteDetection.lean

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

Module documentation

Faithful mod-p action outside the dyadic quadratic case

The cyclotomic field and its complete discrete valuation are constructed from the base field. The logarithmic detection theorem then applies with no auxiliary field or representation data in the public statement.

Imports8
Imported by3

Declarations

theorem

exists_nontrivial_primeDegree_H1Action_in_closure

L30 ↗
ClassFieldTower.Martinet.Shafarevich.exists_nontrivial_primeDegree_H1Action_in_closure
Source context 2 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ValuationTheory.DiscreteValuationField

-- Abstracting the closure keeps a single F-algebra on the chosen intermediate
-- field. The only new algebra is the composite F/K/E structure.
Lean source · statement
theorem exists_nontrivial_primeDegree_H1Action_in_closure
    {F K Ω : Type*} [Field F] [Field K] [Field Ω]
    [Algebra F K] [Algebra K Ω] [IsAlgClosure K Ω] [IsGalois F K] [CharZero F]
    (vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete vF]
    (p r : ℕ) [Fact p.Prime] [Fact r.Prime]
    [CharP (IsLocalRing.ResidueField vF.valuationSubring) p]
    (hprime : r ≠ p ∨ p ≠ 2) (hdegree : Module.finrank F K = r) :
    ∃ τ : Gal(K/F), relativeGaloisH1Action (n := p) F K τ ≠ 1
theorem

faithful_relativeH1Action_of_complete_mixedChar_prime_degree

L60 ↗
ClassFieldTower.Martinet.Shafarevich.faithful_relativeH1Action_of_complete_mixedChar_prime_degree
Documentation

A prime-degree Galois extension of a complete discretely valued field of mixed characteristic has faithful mod-p action outside the dyadic quadratic case. No finite generation or residue-field finiteness assumption is required.

Source context 2 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ValuationTheory.DiscreteValuationField

-- Abstracting the closure keeps a single F-algebra on the chosen intermediate
-- field. The only new algebra is the composite F/K/E structure.
Lean source · statement
theorem faithful_relativeH1Action_of_complete_mixedChar_prime_degree
    {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 r : ℕ) [Fact p.Prime] [Fact r.Prime]
    [CharP (IsLocalRing.ResidueField vF.valuationSubring) p]
    (hprime : r ≠ p ∨ p ≠ 2) (hdegree : Module.finrank F K = r) :
    Function.Injective (relativeGaloisH1Action (n := p) F K)
theorem

faithful_relativeH1Action_of_complete_mixedChar_primeTo_degree

L80 ↗
ClassFieldTower.Martinet.Shafarevich.faithful_relativeH1Action_of_complete_mixedChar_primeTo_degree
Documentation

The original prime-to-p-degree theorem is a specialization.

Source context 2 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory ValuationTheory.DiscreteValuationField

-- Abstracting the closure keeps a single F-algebra on the chosen intermediate
-- field. The only new algebra is the composite F/K/E structure.
Lean source · statement
theorem faithful_relativeH1Action_of_complete_mixedChar_primeTo_degree
    {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 r : ℕ) [Fact p.Prime] [Fact r.Prime]
    [CharP (IsLocalRing.ResidueField vF.valuationSubring) p]
    (hrp : r ≠ p) (hdegree : Module.finrank F K = r) :
    Function.Injective (relativeGaloisH1Action (n := p) F K)

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