AlgebraicGeometry.exists_idempotent_appTop_eq_of_isLimit
Every idempotent global section on an affine-transition limit is the pullback of an actual idempotent at a stage.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe uLean source · statement
theorem exists_idempotent_appTop_eq_of_isLimit
{I : Type u} [Category.{u} I] [IsCofiltered I]
(D : I ⥤ Scheme.{u}) (c : Cone D) (hc : IsLimit c)
[∀ {i k} (f : i ⟶ k), IsAffineHom (D.map f)]
[∀ i, CompactSpace (D.obj i)] [∀ i, QuasiSeparatedSpace (D.obj i)]
(e : Γ(c.pt, ⊤)) (he : IsIdempotentElem e) :
∃ (i : I) (t : Γ(D.obj i, ⊤)), IsIdempotentElem t ∧ (c.π.app i).appTop t = e