Module

HomeomorphismIdempotentSections.lean

Nyll.SchemeTheory.Affine.HomeomorphismIdempotentSections

1 declaration indexed from sourceView source ↗

Module documentation

Lifting idempotent sections through a scheme homeomorphism

An idempotent section is locally zero or one. Its two open pieces transport through a homeomorphism and the constant sections glue there. In particular, an idempotent on a closed fibre lifts to every infinitesimal thickening.

Imports3

Mathlib.AlgebraicGeometry.Scheme
Mathlib.Algebra.Ring.Idempotent
Mathlib.Topology.Homeomorph.Defs

Imported by3

theorem

exists_appTop_eq_of_isHomeomorph_of_isIdempotentElem

L29 ↗

AlgebraicGeometry.Scheme.Hom.exists_appTop_eq_of_isHomeomorph_of_isIdempotentElem

Documentation

A morphism inducing a homeomorphism lifts every idempotent global section. The lift is constructed by gluing its zero and one pieces.

Source context 4 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry.Scheme.Hom
universe u

Lean source · statement

theorem exists_appTop_eq_of_isHomeomorph_of_isIdempotentElem
    {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : IsHomeomorph f)
    (e : Γ(X, ⊤)) (he : IsIdempotentElem e) :
    ∃ a : Γ(Y, ⊤), f.appTop a = e

Module documentation

Lifting idempotent sections through a scheme homeomorphism

Declarations

exists_appTop_eq_of_isHomeomorph_of_isIdempotentElem