Module

ReducedCartierDivisor.lean

Nyll.SchemeTheory.RingTheory.ReducedCartierDivisor

3 declarations indexed from sourceView source ↗

Module documentation

The generic local rings of a reduced Cartier divisor

Let f be a nonzerodivisor in a Noetherian ring A, with A / (f) reduced. At every minimal prime over (f), the local ring of A is a DVR and the image of f generates its maximal ideal. The ambient ring need not be a domain, and (f) need not be prime.

This supplies the local-ring assertion preceding the Kummer construction in Stacks Project, Example 58.31.4 (tag 0EYF): https://stacks.math.columbia.edu/tag/0EYF

Imports12

Mathlib.Algebra.GroupWithZero.Action.Regular
Mathlib.LinearAlgebra.Span.Defs
Mathlib.RingTheory.DiscreteValuationRing.TFAE
Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Mathlib.RingTheory.Ideal.Quotient.Nilpotent
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.Defs
Mathlib.RingTheory.Localization.Ideal
Mathlib.RingTheory.Localization.Submodule
Mathlib.RingTheory.RegularLocalRing.Defs
Nyll.SchemeTheory.RingTheory.RegularLocalDomain
Nyll.SchemeTheory.RingTheory.RegularLocalQuotientLift

Imported by2

theorem

maximalIdeal_localizationAtPrime_eq_span_of_reduced_quotient

L39 ↗

SchemeTheory.maximalIdeal_localizationAtPrime_eq_span_of_reduced_quotient

Documentation

A reduced principal divisor is generated by the same element at each of its generic points. No Noetherian hypothesis is needed for this equality.

Source context 2 commands

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

namespace SchemeTheory
universe u

Lean source · statement

theorem maximalIdeal_localizationAtPrime_eq_span_of_reduced_quotient
    {A : Type u} [CommRing A] (f : A)
    [IsReduced (A ⧸ Ideal.span ({f} : Set A))]
    (P : Ideal A) [P.IsPrime]
    (hP : P ∈ (Ideal.span ({f} : Set A)).minimalPrimes) :
    IsLocalRing.maximalIdeal (Localization.AtPrime P) =
      Ideal.span ({algebraMap A (Localization.AtPrime P) f} :
        Set (Localization.AtPrime P))

theorem

isRegularLocalRing_localizationAtPrime_of_reduced_quotient

L68 ↗

SchemeTheory.isRegularLocalRing_localizationAtPrime_of_reduced_quotient

Documentation

The ambient local ring at a generic point of a reduced Cartier divisor is regular. The quotient by the displayed nonzerodivisor is a field.

Source context 2 commands

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

namespace SchemeTheory
universe u

Lean source · statement

theorem isRegularLocalRing_localizationAtPrime_of_reduced_quotient
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (f : A) (hf : f ∈ nonZeroDivisors A)
    [IsReduced (A ⧸ Ideal.span ({f} : Set A))]
    (P : Ideal A) [P.IsPrime]
    (hP : P ∈ (Ideal.span ({f} : Set A)).minimalPrimes) :
    IsRegularLocalRing (Localization.AtPrime P)

theorem

isDiscreteValuationRing_localizationAtPrime_of_reduced_quotient

L97 ↗

SchemeTheory.isDiscreteValuationRing_localizationAtPrime_of_reduced_quotient

Documentation

At a generic point of a reduced Cartier divisor, the ambient local ring is a DVR. Its domain structure is produced from the hypotheses and retained in the statement, rather than supplied as an additional assumption.

Source context 2 commands

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

namespace SchemeTheory
universe u

Lean source · full declaration

theorem isDiscreteValuationRing_localizationAtPrime_of_reduced_quotient
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    (f : A) (hf : f ∈ nonZeroDivisors A)
    [IsReduced (A ⧸ Ideal.span ({f} : Set A))]
    (P : Ideal A) [P.IsPrime]
    (hP : P ∈ (Ideal.span ({f} : Set A)).minimalPrimes) :
    let : IsRegularLocalRing (Localization.AtPrime P) :=
      isRegularLocalRing_localizationAtPrime_of_reduced_quotient f hf P hP
    let : IsDomain (Localization.AtPrime P) :=
      IsRegularLocalRing.isDomain (Localization.AtPrime P)
    IsDiscreteValuationRing (Localization.AtPrime P) := by
  intro hregular hdomain
  let S := Localization.AtPrime P
  let x : S := algebraMap A S f
  have hmax : IsLocalRing.maximalIdeal S = Ideal.span ({x} : Set S) :=
    maximalIdeal_localizationAtPrime_eq_span_of_reduced_quotient f P hP
  have hxregular : x ∈ nonZeroDivisors S :=
    IsLocalization.nonZeroDivisors_le_comap P.primeCompl S hf
  have hxne : x ≠ 0 := nonZeroDivisors.ne_zero hxregular
  have hnotfield : ¬ IsField S := by
    intro hfield
    have hzero : IsLocalRing.maximalIdeal S = ⊥ :=
      IsLocalRing.isField_iff_maximalIdeal_eq.mp hfield
    apply hxne
    apply Ideal.mem_bot.mp
    rw [← hzero, hmax]
    exact Ideal.mem_span_singleton_self x
  have hprincipal : (IsLocalRing.maximalIdeal S).IsPrincipal := ⟨x, hmax⟩
  exact ((IsDiscreteValuationRing.TFAE S hnotfield).out 5 1).mp hprincipal

Module documentation

The generic local rings of a reduced Cartier divisor

Declarations

maximalIdeal_localizationAtPrime_eq_span_of_reduced_quotient

isRegularLocalRing_localizationAtPrime_of_reduced_quotient

isDiscreteValuationRing_localizationAtPrime_of_reduced_quotient