NYLL
Module

ProperIdempotentSectionLift.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperIdempotentSectionLift
1 declaration indexed from sourceView source ↗

Module documentation

Proper idempotent-section lifting over a Noetherian affine base

An idempotent on a closed fibre lifts through every infinitesimal thickening because the thickenings have the same underlying space. The proper-cohomology stabilization theorem then produces a global section with that restriction. The global section need not be idempotent.

This is the Noetherian supplier for Stacks Project Tag 0G7X. Extending it to an arbitrary finitely presented proper family still requires descending the family and the finite idempotent relation to a Noetherian model.

Imports4
Imported by2

Declarations

theorem

exists_appTop_eq_of_isProper_of_isIdempotentElem

L35 ↗
AlgebraicGeometry.exists_appTop_eq_of_isProper_of_isIdempotentElem
Documentation

An idempotent section on any closed fibre of a proper morphism over a Noetherian affine base is the restriction of a 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_isIdempotentElem
    {A : Type u} [CommRing A] [IsNoetherianRing A]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A)) [IsProper f]
    (I : Ideal A) :
    ∀ e : Γ(pullback f (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I))), ⊤),
      IsIdempotentElem e → ∃ a : Γ(X, ⊤),
        (pullback.fst f (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))).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.