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.IsReduced.component_reduced {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsReduced X] (U : TopologicalSpace.Opens X.toPresheafedSpace) :
    IsReduced (X.presheaf.obj { unop := U })
    theorem AlgebraicGeometry.isReducedOfStalkIsReduced (X : AlgebraicGeometry.Scheme) [∀ (x : X.toPresheafedSpace), IsReduced (X.presheaf.stalk x)] :
    instance AlgebraicGeometry.stalk_isReduced_of_reduced (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsReduced X] (x : X.toPresheafedSpace) :
    IsReduced (X.presheaf.stalk x)
    Equations
    • =
    theorem AlgebraicGeometry.reduce_to_affine_global (P : (X : AlgebraicGeometry.Scheme) → TopologicalSpace.Opens X.toPresheafedSpaceProp) (h₁ : ∀ (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens X.toPresheafedSpace), (∀ (x : U), ∃ (V : TopologicalSpace.Opens X.toPresheafedSpace) (_ : x V) (x : V U), P X V)P X U) (h₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) [hf : AlgebraicGeometry.IsOpenImmersion f], ∃ (U : Set X.toPresheafedSpace) (V : Set Y.toPresheafedSpace) (hU : U = ) (hV : V = Set.range f.val.base), P X { carrier := U, is_open' := }P Y { carrier := V, is_open' := }) (h₃ : ∀ (R : CommRingCat), P (AlgebraicGeometry.Scheme.Spec.obj { unop := 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 { unop := 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
    theorem AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot {X : AlgebraicGeometry.Scheme} [hX : AlgebraicGeometry.IsReduced X] {U : TopologicalSpace.Opens X.toPresheafedSpace} (s : (X.presheaf.obj { unop := U })) (hs : X.basicOpen s = ) :
    s = 0
    @[simp]
    theorem AlgebraicGeometry.basicOpen_eq_bot_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {U : TopologicalSpace.Opens X.toPresheafedSpace} (s : (X.presheaf.obj { unop := U })) :
    X.basicOpen s = s = 0

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

    Instances
      theorem AlgebraicGeometry.IsIntegral.component_integral {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsIntegral X] (U : TopologicalSpace.Opens X.toPresheafedSpace) [Nonempty U] :
      IsDomain (X.presheaf.obj { unop := U })
      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 U] :
      Function.Injective (X.presheaf.map i.op)