Module

DVRPrimeBelowCoordinate.lean

Nyll.SchemeTheory.Normalization.Products.DVRPrimeBelowCoordinate

1 declaration indexed from sourceView source ↗

Module documentation

Generic primes below a selected DVR product factor

In a product of local rings, fix the maximal prime selected by one coordinate. If that coordinate is a DVR, the only strictly smaller prime is the kernel of coordinate evaluation. This identifies a selected generic component with the generic point of the specified DVR factor.

Imports2

Mathlib.RingTheory.DiscreteValuationRing.TFAE
Nyll.SchemeTheory.Normalization.Products.LocalRingFactor

Imported by2

theorem

prime_eq_ker_coordinateEval_of_le_of_ne

L31 ↗

EtaleFundamentalGroups.prime_eq_ker_coordinateEval_of_le_of_ne

Documentation

A prime strictly below the maximal prime selected by a DVR coordinate is exactly the kernel of coordinate evaluation.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uι uA
variable {ι : Type uι} (A : ι → Type uA)
variable [∀ j, CommRing (A j)] [∀ j, IsDomain (A j)]
variable [∀ j, IsDiscreteValuationRing (A j)]

Lean source · statement

theorem prime_eq_ker_coordinateEval_of_le_of_ne
    (i : ι) (N : Ideal (∀ j, A j)) [N.IsPrime]
    (hNP : N ≤ productCoordinatePrime A i)
    (hNne : N ≠ productCoordinatePrime A i) :
    N = RingHom.ker (Pi.evalRingHom A i)

Module documentation

Generic primes below a selected DVR product factor

Declarations

prime_eq_ker_coordinateEval_of_le_of_ne