NYLL
Module

RegularLocalPrimePair.lean

Nyll.EtaleFundamentalGroups.Purity.Local.RegularLocalPrimePair
2 declarations indexed from sourceView source ↗

Module documentation

A pair of prime parameters

A regular local ring of dimension at least two supplies two parameters for the prime-away intersection argument. The nondivisibility is derived from regularity in the quotient by the first parameter.

Imports2
Imported by2

Declarations

theorem

primePair_of_regularSystem_cons_cons

L25 ↗
EtaleFundamentalGroups.primePair_of_regularSystem_cons_cons
Documentation

The first two entries of a regular system are nonassociated prime parameters.

Source context 3 commands

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

namespace EtaleFundamentalGroups
open IsLocalRing RingTheory.Sequence
universe u
Lean source · statement
theorem primePair_of_regularSystem_cons_cons
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {x y : R} {ps : List R}
    (hreg : IsRegular R (x :: y :: ps))
    (hgen : Ideal.ofList (x :: y :: ps) = maximalIdeal R) :
    Prime x ∧ y ≠ 0 ∧ ¬ x ∣ y
theorem

exists_primePair_of_isRegularLocalRing

L56 ↗
EtaleFundamentalGroups.exists_primePair_of_isRegularLocalRing
Documentation

Bare regular-local hypotheses of dimension at least two supply actual parameters for the flat Hartogs equalizer.

Source context 3 commands

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

namespace EtaleFundamentalGroups
open IsLocalRing RingTheory.Sequence
universe u
Lean source · statement
theorem exists_primePair_of_isRegularLocalRing
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (hdim : 2 ≤ ringKrullDim R) :
    ∃ x y : R, x ∈ maximalIdeal R ∧ y ∈ maximalIdeal R ∧
      Prime x ∧ y ≠ 0 ∧ ¬ x ∣ y

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