NYLL
Module

NoetherianImageIdempotentLift.lean

Nyll.SchemeTheory.Descent.NoetherianImageIdempotentLift
2 declarations indexed from sourceView source ↗

Module documentation

Lifting closed-fiber idempotents from actual Noetherian image stages

An idempotent on the original fiber descends to an actual Noetherian image stage. Localizing that stage at the contracted closed point permits the Noetherian proper-section theorem to lift it. Pullback of that section gives an actual global section on the original closed subscheme.

Imports5
Imported by2

Declarations

theorem

exists_appTop_eq_of_isIdempotentElem

L39 ↗
AlgebraicGeometry.LocalStageResidue.exists_appTop_eq_of_isIdempotentElem
Documentation

A stage-fiber idempotent lifts to a section on the original scheme by localizing the actual Noetherian stage at the contracted closed point.

Source context 9 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A) {P X : Scheme.{u}}
variable (q : P ⟶ Spec (CommRingCat.of B))
variable (f : X ⟶ Spec (CommRingCat.of A)) (t : X ⟶ P)
variable (w : t ≫ q = f ≫ Spec.map (CommRingCat.ofHom φ))
Lean source · statement
theorem exists_appTop_eq_of_isIdempotentElem [IsNoetherianRing B] [IsProper q]
    (e : Γ(pullback q (stageResidueSpec φ), ⊤)) (he : IsIdempotentElem e) :
    ∃ a : Γ(X, ⊤),
      (pullback.fst f (topResidueSpec (A := A))).appTop a =
        (topFiberMap φ q f t w).appTop e
theorem

exists_appTop_eq_of_closedFiber_isIdempotentElem

L76 ↗
AlgebraicGeometry.NoetherianImageApproximation.exists_appTop_eq_of_closedFiber_isIdempotentElem
Documentation

A closed-fiber idempotent of the original closed subscheme is the restriction of an actual global section, with no Noetherian assumption on the original local base or finite-presentation assumption on the subscheme.

Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.NoetherianImageApproximation
universe u
variable (A₀ A : Type u) [CommRing A₀] [CommRing A] [Algebra A₀ A]
variable [IsNoetherianRing A₀] [IsLocalRing A]
variable {X₀ : Scheme.{u}} (f₀ : X₀ ⟶ Spec (CommRingCat.of A₀)) [IsProper f₀]
variable {Z : Scheme.{u}} (j : Z ⟶ (ambientCone A₀ A f₀).pt) [IsClosedImmersion j]
Lean source · statement
theorem exists_appTop_eq_of_closedFiber_isIdempotentElem
    (e : Γ(originalResidueFiber A₀ A f₀ j (IsLocalRing.maximalIdeal A), ⊤))
    (he : IsIdempotentElem e) :
    ∃ a : Γ(Z, ⊤),
      (pullback.fst (originalBaseMap A₀ A f₀ j)
        (SubalgebraStages.residueSpecBaseTop (IsLocalRing.maximalIdeal A))).appTop a = e

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