NYLL
Module

Explicit.lean

Nyll.EtaleFundamentalGroups.Kummer.Radicals.Explicit
7 declarations indexed from sourceView source ↗

Module documentation

The explicit one-component Kummer algebra

This file records the first concrete algebra facts for the Kummer equation X ^ n - a. After the boundary parameter has been inverted, its adjoined root is a unit. Consequently the derivative at that root is a unit exactly when the exponent is a unit in the localized base ring.

No etaleness or derivative-unit conclusion is assumed here. The remaining geometric input is a producer that turns etaleness of the explicit Kummer algebra into the derivative-unit side of the final equivalence.

Imports3
  • Mathlib.RingTheory.AdjoinRoot
  • Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
  • Mathlib.RingTheory.Localization.Away.Basic
Imported by10

Declarations

theorem

adjoinRoot_root_pow

L31 ↗
EtaleFundamentalGroups.Kummer.adjoinRoot_root_pow
Documentation

The defining equation of AdjoinRoot (X ^ n - C a), over any commutative ring.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v
Lean source · statement
theorem adjoinRoot_root_pow
    {A : Type u} [CommRing A] (n : ℕ) (a : A) :
    (AdjoinRoot.root (X ^ n - C a)) ^ n =
      AdjoinRoot.of (X ^ n - C a) a
theorem

isUnit_adjoinRoot_root_of_isUnit

L38 ↗
EtaleFundamentalGroups.Kummer.isUnit_adjoinRoot_root_of_isUnit
Documentation

A root of X ^ n - a is a unit when a is a unit and n is positive.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v
Lean source · statement
theorem isUnit_adjoinRoot_root_of_isUnit
    {A : Type u} [CommRing A] {n : ℕ} (hn : 0 < n) {a : A}
    (ha : IsUnit a) :
    IsUnit (AdjoinRoot.root (X ^ n - C a))
theorem

aeval_derivative_X_pow_sub_C

L47 ↗
EtaleFundamentalGroups.Kummer.aeval_derivative_X_pow_sub_C
Documentation

Evaluation of the derivative of the explicit Kummer polynomial at its adjoined root.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v
Lean source · statement
theorem aeval_derivative_X_pow_sub_C
    {A : Type u} [CommRing A] (n : ℕ) (a : A) :
    aeval (AdjoinRoot.root (X ^ n - C a)) (X ^ n - C a).derivative =
      algebraMap A (AdjoinRoot (X ^ n - C a)) (n : A) *
        AdjoinRoot.root (X ^ n - C a) ^ (n - 1)
theorem

faithfullyFlat_adjoinRoot_X_pow_sub_C

L61 ↗
EtaleFundamentalGroups.Kummer.faithfullyFlat_adjoinRoot_X_pow_sub_C
Documentation

The positive-degree monic Kummer algebra is faithfully flat over a nontrivial base ring.

Indeed the monic quotient is free. Positive degree makes it nontrivial over a nontrivial base, hence free-module faithful flatness applies.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v
Lean source · statement
theorem faithfullyFlat_adjoinRoot_X_pow_sub_C
    {A : Type u} [CommRing A] [Nontrivial A] {n : ℕ} (hn : 0 < n)
    (a : A) :
    Module.FaithfullyFlat A (AdjoinRoot (X ^ n - C a))
theorem

isUnit_algebraMap_adjoinRoot_X_pow_sub_C_iff

L81 ↗
EtaleFundamentalGroups.Kummer.isUnit_algebraMap_adjoinRoot_X_pow_sub_C_iff
Documentation

The base ring detects units inside the positive-degree monic Kummer algebra.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v
Lean source · statement
theorem isUnit_algebraMap_adjoinRoot_X_pow_sub_C_iff
    {A : Type u} [CommRing A] [Nontrivial A] {n : ℕ} (hn : 0 < n)
    (a b : A) :
    IsUnit (algebraMap A (AdjoinRoot (X ^ n - C a)) b) ↔ IsUnit b
theorem

isUnit_aeval_derivative_iff_isUnit_natCast

L93 ↗
EtaleFundamentalGroups.Kummer.isUnit_aeval_derivative_iff_isUnit_natCast
Documentation

For a Kummer polynomial with invertible constant term, its formal derivative at the adjoined root is a unit exactly when the exponent is a unit in the base.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v
Lean source · statement
theorem isUnit_aeval_derivative_iff_isUnit_natCast
    {A : Type u} [CommRing A] [Nontrivial A] {n : ℕ} (hn : 0 < n)
    {a : A} (ha : IsUnit a) :
    IsUnit (aeval (AdjoinRoot.root (X ^ n - C a))
      (X ^ n - C a).derivative) ↔ IsUnit (n : A)
theorem

isUnit_aeval_derivative_iff_isUnit_algebraMap_natCast_away

L117 ↗
EtaleFundamentalGroups.Kummer.isUnit_aeval_derivative_iff_isUnit_algebraMap_natCast_away
Documentation

On the complement of a prime boundary parameter t, derivative invertibility for X ^ n - t is equivalent to invertibility of the localized exponent.

The right side is exactly the input consumed by the unit-descent lemma for the map R → R[1/t].

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v
Lean source · statement
theorem isUnit_aeval_derivative_iff_isUnit_algebraMap_natCast_away
    {R : Type u} {S : Type v} [CommRing R] [IsDomain R]
    [CommRing S] [Algebra R S] {t : R} [IsLocalization.Away t S]
    (ht : Prime t) {n : ℕ} (hn : 0 < n) :
    IsUnit (aeval
      (AdjoinRoot.root (X ^ n - C (algebraMap R S t)))
      (X ^ n - C (algebraMap R S t)).derivative) ↔
      IsUnit (algebraMap R S (n : R))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.