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_of_isReduced_stalk (X : AlgebraicGeometry.Scheme) [∀ (x : X.toPresheafedSpace), IsReduced (X.presheaf.stalk x)] :
    instance AlgebraicGeometry.isReduced_stalk_of_isReduced (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} → X.OpensProp) {X : AlgebraicGeometry.Scheme} (U : X.Opens) (h₁ : ∀ (X : AlgebraicGeometry.Scheme) (U : X.Opens), (∀ (x : U), ∃ (V : X.Opens) (_ : x V) (x : V U), P V)P 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 { carrier := U, is_open' := }P { carrier := V, is_open' := }) (h₃ : ∀ (R : CommRingCat), P ) :
    P 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 : (AlgebraicGeometry.Spec R).toPresheafedSpace), P (AlgebraicGeometry.Spec 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 : X.Opens} (s : (X.presheaf.obj (Opposite.op U))) (hs : X.basicOpen s = ) :
    s = 0
    @[simp]
    theorem AlgebraicGeometry.basicOpen_eq_bot_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {U : X.Opens} (s : (X.presheaf.obj (Opposite.op U))) :
    X.basicOpen s = s = 0

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

    • nonempty : Nonempty X.toPresheafedSpace
    • component_integral : ∀ (U : X.Opens) [inst : Nonempty (U).toPresheafedSpace], IsDomain (X.presheaf.obj (Opposite.op U))
    Instances
      theorem AlgebraicGeometry.IsIntegral.component_integral {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsIntegral X] (U : X.Opens) [Nonempty (U).toPresheafedSpace] :
      IsDomain (X.presheaf.obj (Opposite.op U))
      instance AlgebraicGeometry.Scheme.component_nontrivial (X : AlgebraicGeometry.Scheme) (U : X.Opens) [Nonempty (U).toPresheafedSpace] :
      Nontrivial (X.presheaf.obj (Opposite.op U))
      Equations
      • =
      theorem AlgebraicGeometry.map_injective_of_isIntegral (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] {U : X.Opens} {V : X.Opens} (i : U V) [H : Nonempty (U).toPresheafedSpace] :
      Function.Injective (X.presheaf.map i.op)