Module

NoetherianProperFiberSections.lean

Nyll.SchemeTheory.Morphisms.NoetherianProperFiberSections

4 declarations indexed from sourceView source ↗

Module documentation

Lifting idempotent sections of proper closed fibres

Over a Noetherian ring, every idempotent section on a closed base change of a proper scheme is the restriction of an actual global section. The lift need not be idempotent. Its existence follows from the already constructed proper formal-functions approximation: the idempotent lifts through the homeomorphism from the closed base change to an infinitesimal thickening, and a sufficiently thick such lift comes from a global section.

Imports6

Nyll.SchemeTheory.Morphisms.exists_appTop_pullback_map_eq_appTop_pullback_fst_of_isProper
Nyll.SchemeTheory.Affine.HomeomorphismIdempotentSections
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Spectrum.Prime.Topology

Imported by2

theorem

range_specMap_quotient

L33 ↗

AlgebraicGeometry.range_specMap_quotient

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem range_specMap_quotient
    {A : Type u} [CommRing A] (I : Ideal A) :
    Set.range (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))) =
      PrimeSpectrum.zeroLocus (I : Set A)

theorem

exists_appTop_eq_on_pow_one

L40 ↗

AlgebraicGeometry.exists_appTop_eq_on_pow_one

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem exists_appTop_eq_on_pow_one
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {P : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of A)) [IsProper q]
    (I : Ideal A) :
    ∀ (e : Γ(pullback q (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I ^ 1)))), ⊤)),
      IsIdempotentElem e → ∃ a : Γ(P, ⊤),
        (pullback.fst q
          (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I ^ 1))))).appTop a = e

theorem

exists_appTop_eq_of_isProper_of_isNoetherianRing_of_isIdempotentElem

L103 ↗

AlgebraicGeometry.exists_appTop_eq_of_isProper_of_isNoetherianRing_of_isIdempotentElem

Documentation

An idempotent section on any closed base change of a proper scheme over a Noetherian ring is the restriction of an actual global section.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem exists_appTop_eq_of_isProper_of_isNoetherianRing_of_isIdempotentElem
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {P : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of A)) [IsProper q]
    (I : Ideal A)
    (e : Γ(pullback q (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))), ⊤))
    (he : IsIdempotentElem e) :
    ∃ a : Γ(P, ⊤),
      (pullback.fst q (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))).appTop a = e

theorem

exists_appTop_eq_of_isProper_of_surjective_of_isIdempotentElem

L122 ↗

AlgebraicGeometry.exists_appTop_eq_of_isProper_of_surjective_of_isIdempotentElem

Documentation

The same lift for an actual surjective base-ring map, using the constructed quotient-by-kernel isomorphism and its pullback. In particular, this applies directly to the residue map of a Noetherian local ring.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem exists_appTop_eq_of_isProper_of_surjective_of_isIdempotentElem
    {A K : Type u} [CommRing A] [IsNoetherianRing A] [CommRing K]
    {P : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of A)) [IsProper q]
    (φ : A →+* K) (hφ : Function.Surjective φ)
    (e : Γ(pullback q (Spec.map (CommRingCat.ofHom φ)), ⊤))
    (he : IsIdempotentElem e) :
    ∃ a : Γ(P, ⊤),
      (pullback.fst q (Spec.map (CommRingCat.ofHom φ))).appTop a = e

Module documentation

Lifting idempotent sections of proper closed fibres

Declarations

range_specMap_quotient

exists_appTop_eq_on_pow_one

exists_appTop_eq_of_isProper_of_isNoetherianRing_of_isIdempotentElem

exists_appTop_eq_of_isProper_of_surjective_of_isIdempotentElem