Module

Basic.lean

Nyll.EtaleFundamentalGroups.Kummer.SelectedRoot.Prime.Basic

6 declarations indexed from sourceView source ↗

Module documentation

Primality of the selected Kummer root

For a prime element a, the root of X ^ n - a is again prime. The proof uses the canonical map to R ⧸ (a) which sends the adjoined root to zero and identifies its kernel with the principal ideal generated by that root.

Imports3

Nyll.EtaleFundamentalGroups.Kummer.Radicals.Explicit
Mathlib.Algebra.Polynomial.Eval.Coeff
Mathlib.RingTheory.Ideal.Quotient.Operations

Imported by5

def

adjoinRootToQuotient

L29 ↗

EtaleFundamentalGroups.Kummer.adjoinRootToQuotient

Documentation

The canonical map from a positive Kummer root cover to the quotient by its radicand, sending the adjoined root to zero.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

def adjoinRootToQuotient
    {R : Type u} [CommRing R] {n : ℕ} (hn : 0 < n) (a : R) :
    AdjoinRoot (X ^ n - C a) →+* (R ⧸ Ideal.span {a})

theorem

adjoinRootToQuotient_surjective

L36 ↗

EtaleFundamentalGroups.Kummer.adjoinRootToQuotient_surjective

Documentation

The canonical root-to-zero map is surjective.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem adjoinRootToQuotient_surjective
    {R : Type u} [CommRing R] {n : ℕ} (hn : 0 < n) (a : R) :
    Function.Surjective (adjoinRootToQuotient hn a)

theorem

ker_adjoinRootToQuotient

L45 ↗

EtaleFundamentalGroups.Kummer.ker_adjoinRootToQuotient

Documentation

The kernel of the root-to-zero map is generated by the adjoined root.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem ker_adjoinRootToQuotient
    {R : Type u} [CommRing R] {n : ℕ} (hn : 0 < n) (a : R) :
    RingHom.ker (adjoinRootToQuotient hn a) =
      Ideal.span ({AdjoinRoot.root (X ^ n - C a)} :
        Set (AdjoinRoot (X ^ n - C a)))

def

adjoinRootQuotientRootEquiv

L92 ↗

EtaleFundamentalGroups.Kummer.adjoinRootQuotientRootEquiv

Documentation

Quotienting a positive Kummer root cover by its root recovers the base quotient by the radicand.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

def adjoinRootQuotientRootEquiv
    {R : Type u} [CommRing R] {n : ℕ} (hn : 0 < n) (a : R) :
    AdjoinRoot (X ^ n - C a) ⧸
        Ideal.span ({AdjoinRoot.root (X ^ n - C a)} :
          Set (AdjoinRoot (X ^ n - C a))) ≃+*
      R ⧸ Ideal.span {a}

theorem

adjoinRootQuotientRootEquiv_mk_of

L103 ↗

EtaleFundamentalGroups.Kummer.adjoinRootQuotientRootEquiv_mk_of

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem adjoinRootQuotientRootEquiv_mk_of
    {R : Type u} [CommRing R] {n : ℕ} (hn : 0 < n) (a r : R) :
    adjoinRootQuotientRootEquiv hn a
        (Ideal.Quotient.mk
          (Ideal.span ({AdjoinRoot.root (X ^ n - C a)} :
            Set (AdjoinRoot (X ^ n - C a))))
          (AdjoinRoot.of (X ^ n - C a) r)) =
      Ideal.Quotient.mk (Ideal.span {a}) r

theorem

prime_adjoinRoot_root_of_prime

L117 ↗

EtaleFundamentalGroups.Kummer.prime_adjoinRoot_root_of_prime

Documentation

A positive-degree Kummer root of a prime element is prime.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem prime_adjoinRoot_root_of_prime
    {R : Type u} [CommRing R] [IsDomain R]
    {n : ℕ} (hn : 0 < n) {a : R} (ha : Prime a) :
    Prime (AdjoinRoot.root (X ^ n - C a))

Module documentation

Primality of the selected Kummer root

Declarations

adjoinRootToQuotient

adjoinRootToQuotient_surjective

ker_adjoinRootToQuotient

adjoinRootQuotientRootEquiv

adjoinRootQuotientRootEquiv_mk_of

prime_adjoinRoot_root_of_prime