Module

Unit.lean

Nyll.EtaleFundamentalGroups.Kummer.Descent.Unit

3 declarations indexed from sourceView source ↗

Module documentation

Unit descent from a boundary complement

The explicit Kummer calculation takes place after inverting a boundary parameter t. This file proves the descent step needed afterwards: an element not divisible by the prime element t was already a unit before the localization if its image is a unit after inverting t.

Imports4

Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Ideal.Quotient.Basic
Mathlib.Algebra.CharP.Defs
Mathlib.Algebra.CharZero.Defs

Imported by3

theorem

not_dvd_natCast_of_charZero_quotient

L33 ↗

EtaleFundamentalGroups.Kummer.not_dvd_natCast_of_charZero_quotient

Documentation

On a horizontal prime component of characteristic zero, its defining parameter cannot divide a positive natural number.

This is the arithmetic input needed by unit descent. It is produced directly from the quotient characteristic rather than being exposed as a hypothesis of the Kummer obstruction.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v

Lean source · statement

theorem not_dvd_natCast_of_charZero_quotient
    {R : Type u} [CommRing R] {t : R}
    [CharZero (R ⧸ Ideal.span {t})] (n : ℕ) (hn : 0 < n) :
    ¬ t ∣ (n : R)

theorem

isUnit_of_isUnit_algebraMap_away_of_prime_of_not_dvd

L54 ↗

EtaleFundamentalGroups.Kummer.isUnit_of_isUnit_algebraMap_away_of_prime_of_not_dvd

Documentation

Let S be the localization of a domain R obtained by inverting a prime element t. If t does not divide a, then invertibility of a in S already implies invertibility in R.

In the Kummer application, a is the exponent. Its nondivisibility by the horizontal boundary parameter comes from characteristic zero on that component; invertibility after localization is produced by the derivative of the Kummer polynomial.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v

Lean source · statement

theorem isUnit_of_isUnit_algebraMap_away_of_prime_of_not_dvd
    {R : Type u} {S : Type v} [CommRing R] [IsDomain R]
    [CommRing S] [Algebra R S] {t a : R} [IsLocalization.Away t S]
    (ht : Prime t) (hta : ¬ t ∣ a)
    (ha : IsUnit (algebraMap R S a)) : IsUnit a

theorem

natCast_not_isUnit_algebraMap_away_of_dvd_char

L77 ↗

EtaleFundamentalGroups.Kummer.natCast_not_isUnit_algebraMap_away_of_dvd_char

Documentation

Wild Kummer exponents cannot become units on the complement of a horizontal prime boundary.

The quotient R ⧸ (t) having characteristic zero says that the horizontal parameter t cannot divide a positive natural number. If a characteristic p specialization of R exists and p ∣ n, then n cannot be a unit in R[1/t]: otherwise unit descent would make n a unit in R, and hence in the characteristic-p target, where it is zero.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Kummer
universe u v

Lean source · statement

theorem natCast_not_isUnit_algebraMap_away_of_dvd_char
    {R : Type u} {S : Type v} {k : Type*}
    [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 (algebraMap R S (n : R))

Module documentation

Unit descent from a boundary complement

Declarations

not_dvd_natCast_of_charZero_quotient

isUnit_of_isUnit_algebraMap_away_of_prime_of_not_dvd

natCast_not_isUnit_algebraMap_away_of_dvd_char