NYLL
Module

FinitelyGeneratedPositiveCharacteristicDetection.lean

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

Module documentation

Detecting Galois automorphisms over finitely generated fields of positive characteristic

Nontrivial finite-order automorphisms move discrete valuations. A local Artin--Schreier character and weak approximation detect their action modulo the characteristic, including over imperfect fields.

Imports4
Imported by2

Declarations

theorem

exists_moved_mod_prime_of_moved_valuation_posChar

L27 ↗
Yamaguchi26AbfaithfulGalois.exists_moved_mod_prime_of_moved_valuation_posChar
Documentation

Moving a discrete valuation in characteristic p forces a nontrivial modulo-p action on absolute Galois abelianization.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField ProCGroups.Abelian
universe u v
Lean source · statement
theorem exists_moved_mod_prime_of_moved_valuation_posChar
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    (target : DVF.{u, v} L) (p : ℕ) [Fact p.Prime] [CharP L p]
    (τ : Gal(L/K))
    (hτ : ¬ target.valuation.IsEquiv (target.valuation.comap τ.toRingEquiv.toRingHom)) :
    ∃ z : abelianModPower Gal(AlgebraicClosure L/L) p,
      relativeGaloisAbelianModPowerTransform K L p τ.symm z ≠ z
theorem

prime_order_detection_of_fg_posChar

L57 ↗
Yamaguchi26AbfaithfulGalois.prime_order_detection_of_fg_posChar
Documentation

Prime-degree Galois extensions of infinite finitely generated fields in positive characteristic act nontrivially on absolute abelianization modulo that characteristic.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField ProCGroups.Abelian
universe u v
Lean source · statement
theorem prime_order_detection_of_fg_posChar
    {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] [Infinite K]
    (hfg : Field.FG 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.