NYLL
Module

PositiveCharacteristicCompleteDetection.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.PositiveCharacteristicCompleteDetection
2 declarations indexed from sourceView source ↗

Module documentation

Prime-degree detection over complete discretely valued fields of characteristic p

Artin--Schreier classes are infinite over a discretely valued field. In degree p, finite restriction kernels and additive Hilbert 90 detect the action. In every other prime degree, a norm valuation and a base-field multiple detect it directly.

Imports7
Imported by2

Declarations

theorem

exists_moved_mod_prime_of_artinSchreier_difference

L30 ↗
Yamaguchi26AbfaithfulGalois.exists_moved_mod_prime_of_artinSchreier_difference
Documentation

A moved Artin--Schreier class detects the actual relative action modulo p.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian ValuationTheory.DiscreteValuationField
universe u v
Lean source · statement
theorem exists_moved_mod_prime_of_artinSchreier_difference
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    (p : ℕ) [Fact p.Prime] [CharP L p] (τ : Gal(L/K))
    (x : L) (hx : ∀ y : L, y ^ p - y ≠ τ x - x) :
    ∃ z : abelianModPower Gal(AlgebraicClosure L/L) p,
      relativeGaloisAbelianModPowerTransform K L p τ.symm z ≠ z
theorem

prime_order_detection_of_complete_charP

L52 ↗
Yamaguchi26AbfaithfulGalois.prime_order_detection_of_complete_charP
Documentation

Every prime-degree Galois extension of a complete discretely valued field of characteristic p acts nontrivially on its absolute abelianization modulo p.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ProCGroups.Abelian ValuationTheory.DiscreteValuationField
universe u v
Lean source · statement
theorem prime_order_detection_of_complete_charP
    {K L : Type u} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    (p r : ℕ) [Fact p.Prime] [Fact r.Prime] [CharP K p]
    (D : CompleteDVF.{u, v} K) (hdegree : Module.finrank K L = r) :
    ∃ τ : Gal(L/K), τ ≠ 1 ∧
      ∃ z : abelianModPower Gal(AlgebraicClosure L/L) p,
        relativeGaloisAbelianModPowerTransform K L p τ z ≠ z

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