Module

FinitelyGeneratedMovingValuation.lean

Nyll.AlgebraicCurves.Valuations.FinitelyGeneratedMovingValuation

1 declaration indexed from sourceView source ↗

Module documentation

Discrete valuations moved by finite-order automorphisms

A nontrivial finite-order automorphism of an infinite finitely generated field of positive characteristic moves a discrete valuation class.

Imports4

Imported by2

theorem

exists_moved_DVF_of_fg_posChar

L26 ↗

FieldTheory.exists_moved_DVF_of_fg_posChar

Documentation

A nontrivial finite-order automorphism of an infinite finitely generated field of positive characteristic moves some discrete valuation class.

Source context 3 commands

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

namespace FieldTheory
open ValuationTheory.DiscreteValuationField
universe u

Lean source · statement

theorem exists_moved_DVF_of_fg_posChar
    (K : Type u) [Field K] [Infinite K] (hfg : Field.FG K)
    (hchar : ringChar K ≠ 0) (τ : K ≃+* K) (hne : τ ≠ 1)
    (n : ℕ) (hn : 0 < n) (hpow : τ ^ n = 1) :
    ∃ D : DVF.{u,0} K, ¬ D.valuation.IsEquiv (D.valuation.comap τ.toRingHom)

Module documentation

Discrete valuations moved by finite-order automorphisms

Declarations

exists_moved_DVF_of_fg_posChar