Module

NonunitLocalization.lean

Nyll.SchemeTheory.LocalGeometry.HeightTwo.NonunitLocalization

1 declaration indexed from sourceView source ↗

Module documentation

A height-two localization detected by a nonunit integer

Let t generate a prime divisor in a Noetherian local domain. If a positive integer e is nonzero but noninvertible modulo t, then a minimal prime over (t, e) has height exactly two. At that prime, e remains a nonunit.

This is the codimension-two reduction used in the local-purity part of the one-point inertia argument. Its hypotheses are only the source-side divisor and residue-characteristic data; no height-two prime is supplied as input.

Imports2

Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Mathlib.RingTheory.Localization.AtPrime.Basic

Imported by3

theorem

exists_heightTwo_prime_of_nonunit_natCast_mod_prime

L30 ↗

EtaleFundamentalGroups.exists_heightTwo_prime_of_nonunit_natCast_mod_prime

Documentation

A positive nonunit integer modulo a prime parameter produces a height-two prime at which that integer is still a nonunit.

Source context 3 commands

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

namespace EtaleFundamentalGroups
open IsLocalRing
universe u

Lean source · statement

theorem exists_heightTwo_prime_of_nonunit_natCast_mod_prime
    {A : Type u} [CommRing A] [IsDomain A] [IsNoetherianRing A]
    [IsLocalRing A]
    (t : A) (ht : Prime t) (e : ℕ) (he : 0 < e)
    [CharZero (A ⧸ Ideal.span {t})]
    (he_nonunit : ¬ IsUnit (e : A ⧸ Ideal.span {t})) :
    ∃ (P : Ideal A) (_ : P.IsPrime),
      P ∈ (Ideal.span {t, (e : A)}).minimalPrimes ∧
      Ideal.span {t} < P ∧
      P.height = 2 ∧
      ¬ IsUnit
        (algebraMap A (Localization.AtPrime P) (e : A))

Module documentation

A height-two localization detected by a nonunit integer

Declarations

exists_heightTwo_prime_of_nonunit_natCast_mod_prime