Documentation

Mathlib.AlgebraicGeometry.Properties

Basic properties of schemes #

We provide some basic properties of schemes

Main definition #

A scheme X is reduced if all 𝒪ₓ(U) are reduced.

Instances
    theorem AlgebraicGeometry.reduce_to_affine_global (P : (X : AlgebraicGeometry.Scheme) → TopologicalSpace.Opens X.toPresheafedSpaceProp) (h₁ : (X : AlgebraicGeometry.Scheme) → (U : TopologicalSpace.Opens X.toPresheafedSpace) → (∀ (x : { x // x U }), V x x, P X V) → P X U) (h₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) [hf : AlgebraicGeometry.IsOpenImmersion f], U V hU hV, P X { carrier := U, is_open' := (_ : IsOpen U) }P Y { carrier := V, is_open' := (_ : IsOpen V) }) (h₃ : (R : CommRingCat) → P (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) ) (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace) :
    P X U

    To show that a statement P holds for all open subsets of all schemes, it suffices to show that

    1. In any scheme X, if P holds for an open cover of U, then P holds for U.
    2. For an open immerison f : X ⟶ Y, if P holds for the entire space of X, then P holds for the image of f.
    3. P holds for the entire space of an affine scheme.
    theorem AlgebraicGeometry.reduce_to_affine_nbhd (P : (X : AlgebraicGeometry.Scheme) → X.toPresheafedSpaceProp) (h₁ : (R : CommRingCat) → (x : PrimeSpectrum R) → P (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) x) (h₂ : {X Y : AlgebraicGeometry.Scheme} → (f : X Y) → [inst : AlgebraicGeometry.IsOpenImmersion f] → (x : X.toPresheafedSpace) → P X xP Y (f.val.base x)) (X : AlgebraicGeometry.Scheme) (x : X.toPresheafedSpace) :
    P X x

    A scheme X is integral if its carrier is nonempty, and 𝒪ₓ(U) is an integral domain for each U ≠ ∅.

    Instances
      theorem AlgebraicGeometry.map_injective_of_isIntegral (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (i : U V) [H : Nonempty { x // x U }] :
      Function.Injective ↑(X.presheaf.map i.op)