NYLL
Module

RootDivisor.lean

Nyll.EtaleFundamentalGroups.Kummer.AdjoinRoot.RootDivisor
2 declarations indexed from sourceView source ↗

Module documentation

The reduced Cartier divisor in a Kummer cover

For a positive exponent, the root of X ^ n - f is a nonzerodivisor if f is. If A / (f) is reduced, the ideal of that root is radical. Thus the root defines a reduced Cartier divisor on the Kummer cover, even when the ambient base is not a domain and the divisor is reducible.

These are algebraic inputs to the local ramification analysis of Stacks Project, Example 58.31.4 (tag 0EYF): https://stacks.math.columbia.edu/tag/0EYF

Imports5
Imported by1

Declarations

theorem

adjoinRoot_root_mem_nonZeroDivisors

L34 ↗
EtaleFundamentalGroups.Kummer.adjoinRoot_root_mem_nonZeroDivisors
Documentation

Adjoining a positive root preserves regularity of the boundary parameter: the new root is a nonzerodivisor in the actual monic quotient.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · statement
theorem adjoinRoot_root_mem_nonZeroDivisors
    {A : Type u} [CommRing A] {n : ℕ} (hn : 0 < n)
    (f : A) (hf : f ∈ nonZeroDivisors A) :
    AdjoinRoot.root (X ^ n - C f) ∈
      nonZeroDivisors (AdjoinRoot (X ^ n - C f))
theorem

isRadical_span_adjoinRoot_root_iff_reduced_quotient

L58 ↗
EtaleFundamentalGroups.Kummer.isRadical_span_adjoinRoot_root_iff_reduced_quotient
Documentation

The root ideal is radical precisely when the original principal divisor is reduced; no primality of the radicand is required.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
Lean source · statement
theorem isRadical_span_adjoinRoot_root_iff_reduced_quotient
    {A : Type u} [CommRing A] {n : ℕ} (hn : 0 < n) (f : A) :
    (Ideal.span ({AdjoinRoot.root (X ^ n - C f)} :
      Set (AdjoinRoot (X ^ n - C f)))).IsRadical ↔
      IsReduced (A ⧸ Ideal.span ({f} : Set A))

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