Module

ExplicitEtale.lean

Nyll.EtaleFundamentalGroups.Kummer.Obstructions.ExplicitEtale

1 declaration indexed from sourceView source ↗

Module documentation

Failure of etaleness for an explicit wild Kummer equation

For the Kummer equation X ^ n - t on the complement of the prime parameter t, etaleness would force the derivative at the distinguished root to be a unit. When the residue characteristic divides n, unit descent from the boundary says that the same derivative is not a unit.

Imports3

Mathlib.RingTheory.Etale.Basic
Nyll.EtaleFundamentalGroups.Kummer.Obstructions.EtaleDerivative
Nyll.EtaleFundamentalGroups.Kummer.Obstructions.WildDerivative

Imported by1

Nyll.EtaleFundamentalGroups.Kummer.Obstructions.All

theorem

not_etale_adjoinRoot_X_pow_sub_C_away_of_dvd_char

L30 ↗

EtaleFundamentalGroups.Kummer.not_etale_adjoinRoot_X_pow_sub_C_away_of_dvd_char

Documentation

The explicit Kummer algebra with wild exponent is not etale on the complement of its prime parameter.

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_etale_adjoinRoot_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) :
    ¬ Algebra.Etale S
      (AdjoinRoot (X ^ n - C (algebraMap R S t)))

Module documentation

Failure of etaleness for an explicit wild Kummer equation

Declarations

not_etale_adjoinRoot_X_pow_sub_C_away_of_dvd_char