Module

RegularSection.lean

Nyll.SchemeTheory.Affine.RegularSection

2 declarations indexed from sourceView source ↗

Module documentation

Restricting a regular global section

A non-zero-divisor on an affine scheme remains a non-zero-divisor on the sections of every open subset. This follows by testing at the actual localized stalks and is valid without reducedness or Noetherianity.

Imports6

Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.RingTheory.Localization.Defs
Mathlib.RingTheory.Regular.IsSMulRegular
Mathlib.Topology.Sheaves.CommRingCat
Mathlib.Topology.Sheaves.Stalks

Imported by2

theorem

isSMulRegular_restrict_of_affine

L32 ↗

AlgebraicGeometry.isSMulRegular_restrict_of_affine

Documentation

A regular global section of an affine scheme acts injectively on sections of every open subset.

Source context 4 commands

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

open CategoryTheory TopologicalSpace
open scoped nonZeroDivisors
namespace AlgebraicGeometry
universe u

Lean source · full declaration

theorem isSMulRegular_restrict_of_affine
    (X : Scheme.{u}) [IsAffine X] (U : X.Opens)
    (r : Γ(X, ⊤)) (hr : r ∈ nonZeroDivisors Γ(X, ⊤)) :
    IsSMulRegular Γ(X, U)
      ((X.presheaf.map (homOfLE (show U ≤ ⊤ from le_top)).op) r) := by
  apply IsSMulRegular.of_right_eq_zero_of_smul
  intro s hs
  apply TopCat.Presheaf.section_ext X.sheaf U s 0
  intro p hp
  let htop := isAffineOpen_top X
  let : Algebra Γ(X, ⊤) (X.presheaf.stalk p) :=
    TopCat.Presheaf.algebra_section_stalk X.presheaf (U := ⊤) ⟨p, trivial⟩
  let : IsLocalization.AtPrime (X.presheaf.stalk p)
      (htop.primeIdealOf ⟨p, trivial⟩).asIdeal :=
    htop.isLocalization_stalk ⟨p, trivial⟩
  have hrp : X.presheaf.germ ⊤ p trivial r ∈
      nonZeroDivisors (X.presheaf.stalk p) :=
    IsLocalization.nonZeroDivisors_le_comap
      (htop.primeIdealOf ⟨p, trivial⟩).asIdeal.primeCompl (X.presheaf.stalk p) hr
  have hz : X.presheaf.germ ⊤ p trivial r *
      X.presheaf.germ U p hp s = 0 := by
    have h := congrArg (X.presheaf.germ U p hp) hs
    simpa only [smul_eq_mul, map_mul, map_zero, X.presheaf.germ_res_apply] using h
  rw [map_zero]
  exact mem_nonZeroDivisors_iff_left.mp hrp _ hz

theorem

restrict_basicOpen_injective_of_affine

L60 ↗

AlgebraicGeometry.restrict_basicOpen_injective_of_affine