Module

RamificationPrimeToResidueTorsion.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RamificationPrimeToResidueTorsion

1 declaration indexed from sourceView source ↗

Module documentation

Prime-to-residue torsion in the actual ramification group

A ramification automorphism whose order is nonzero in the residue field is trivial. For a moved element, divide its successive conjugate differences by the first nonzero difference. Ramification makes every resulting quotient a principal unit, whereas their sum vanishes by telescoping. Reduction would then send the number of terms to zero.

The argument uses the existing ramification subgroup and its principal-unit condition. It requires no discreteness, Henselianity, or finite extension.

Imports2

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.ValuationSubring
Mathlib.Algebra.BigOperators.Field

Imported by2

theorem

ramificationGroup_eq_one_of_pow_eq_one_of_residue_natCast_ne_zero

L34 ↗

RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup_eq_one_of_pow_eq_one_of_residue_natCast_ne_zero

Documentation

An element of the actual ramification group killed by an integer which is nonzero in the residue field is the identity.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
open scoped BigOperators
universe u v
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem ramificationGroup_eq_one_of_pow_eq_one_of_residue_natCast_ne_zero
    (A : _root_.ValuationSubring L) (σ : ramificationGroup K A)
    (n : ℕ) (hn : (n : IsLocalRing.ResidueField A) ≠ 0)
    (hσ : σ ^ n = 1) : σ = 1

Module documentation

Prime-to-residue torsion in the actual ramification group

Declarations

ramificationGroup_eq_one_of_pow_eq_one_of_residue_natCast_ne_zero