Module

MixedCharacteristicMovedValuation.lean

Nyll.Yamaguchi26AbfaithfulGalois.Kummer.MixedCharacteristicMovedValuation

1 declaration indexed from sourceView source ↗

Module documentation

Detecting an automorphism which moves a discrete valuation

A nonzero residue-prime character of one completion and the zero character of its inequivalent conjugate extend simultaneously by weak approximation. Their different values detect the relative action on abelianization modulo the residue prime.

Imports3

Imported by2

theorem

exists_moved_mod_prime_of_moved_valuation

L28 ↗

Yamaguchi26AbfaithfulGalois.exists_moved_mod_prime_of_moved_valuation

Documentation

Moving a mixed-characteristic discrete valuation forces a nontrivial action on the absolute Galois abelianization modulo the residue prime.

Source context 4 commands

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

namespace Yamaguchi26AbfaithfulGalois
open KummerTheory ValuationTheory.DiscreteValuationField ProCGroups.Abelian
open Field.absoluteGaloisGroup
universe u v

Lean source · statement

theorem exists_moved_mod_prime_of_moved_valuation
    {K L : Type u} [Field K] [Field L] [Algebra K L] [CharZero L]
    (target : DVF.{u, v} L) (p : ℕ) [Fact p.Prime] [CharP target.residueField 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

Module documentation

Detecting an automorphism which moves a discrete valuation

Declarations

exists_moved_mod_prime_of_moved_valuation