# Basic properties of schemes #

We provide some basic properties of schemes

## Main definition #

• AlgebraicGeometry.IsIntegral: A scheme is integral if it is nontrivial and all nontrivial components of the structure sheaf are integral domains.
• AlgebraicGeometry.IsReduced: A scheme is reduced if all the components of the structure sheaf are reduced.
Equations
• =

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

Instances
theorem AlgebraicGeometry.IsReduced.component_reduced [self : ] (U : TopologicalSpace.Opens X.toPresheafedSpace) :
IsReduced (X.presheaf.obj { unop := U })
theorem AlgebraicGeometry.isReducedOfStalkIsReduced [∀ (x : X.toPresheafedSpace), IsReduced (X.presheaf.stalk x)] :
instance AlgebraicGeometry.stalk_isReduced_of_reduced (x : X.toPresheafedSpace) :
IsReduced (X.presheaf.stalk x)
Equations
• =
theorem AlgebraicGeometry.isReducedOfIsAffineIsReduced [h : IsReduced (X.presheaf.obj { unop := })] :
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 : ], ∃ (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 ( { unop := R }) ) (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 : ), P ( { unop := R }) x) (h₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X Y) [inst : ] (x : X.toPresheafedSpace), P X xP Y (f.val.base x)) (x : X.toPresheafedSpace) :
P X x
theorem AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot [hX : ] {U : TopologicalSpace.Opens X.toPresheafedSpace} (s : (X.presheaf.obj { unop := U })) (hs : X.basicOpen s = ) :
s = 0
@[simp]
theorem AlgebraicGeometry.basicOpen_eq_bot_iff {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.nonempty [self : ] :
Nonempty X.toPresheafedSpace
theorem AlgebraicGeometry.IsIntegral.component_integral [self : ] (U : TopologicalSpace.Opens X.toPresheafedSpace) [Nonempty U] :
IsDomain (X.presheaf.obj { unop := U })
@[instance 900]
Equations
• =
Equations
• =
theorem AlgebraicGeometry.isIntegralOfOpenImmersion (f : X Y) [Nonempty X.toPresheafedSpace] :
theorem AlgebraicGeometry.isIntegralOfIsAffineIsDomain [Nonempty X.toPresheafedSpace] [h : IsDomain (X.presheaf.obj { unop := })] :
theorem AlgebraicGeometry.map_injective_of_isIntegral {U : TopologicalSpace.Opens X.toPresheafedSpace} {V : TopologicalSpace.Opens X.toPresheafedSpace} (i : U V) [H : Nonempty U] :
Function.Injective (X.presheaf.map i.op)