Nyll.EtaleFundamentalGroups.Kummer.Obstructions.WildDerivative

Module documentation

The wild-exponent obstruction for an explicit Kummer equation

For the equation X ^ n - t on the complement of the prime parameter t, the derivative at the adjoined root cannot be a unit when the residue characteristic divides n. The proof combines the explicit derivative calculation with unit descent from the boundary complement.

theorem

not_isUnit_aeval_derivative_X_pow_sub_C_away_of_dvd_char

L29 ↗

EtaleFundamentalGroups.Kummer.not_isUnit_aeval_derivative_X_pow_sub_C_away_of_dvd_char

Documentation

The derivative of the explicit Kummer equation is not a unit for a wild exponent along a horizontal prime boundary.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v w

Lean source · statement

theorem not_isUnit_aeval_derivative_X_pow_sub_C_away_of_dvd_char
    {R : Type u} {S : Type v} {k : Type w}
    [CommRing R] [IsDomain R] [CommRing S] [Algebra R S]
    [CommRing k] [Nontrivial k] {t : R} [IsLocalization.Away t S]
    (ht : Prime t) [CharZero (R ⧸ Ideal.span {t})]
    (φ : R →+* k) (p n : ℕ) [CharP k p]
    (hn : 0 < n) (hpn : p ∣ n) :
    ¬ IsUnit (aeval
      (AdjoinRoot.root (X ^ n - C (algebraMap R S t)))
      (X ^ n - C (algebraMap R S t)).derivative)

Module documentation

The wild-exponent obstruction for an explicit Kummer equation

Declarations

not_isUnit_aeval_derivative_X_pow_sub_C_away_of_dvd_char