# Documentation

Mathlib.AlgebraicGeometry.Properties

# 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.

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

Instances
theorem AlgebraicGeometry.isReducedOfStalkIsReduced [∀ (x : X.toPresheafedSpace), IsReduced ↑(TopCat.Presheaf.stalk X.presheaf x)] :
instance AlgebraicGeometry.stalk_isReduced_of_reduced (x : X.toPresheafedSpace) :
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 : ], U V hU hV, P X { carrier := U, is_open' := (_ : ) }P Y { carrier := V, is_open' := (_ : ) }) (h₃ : (R : CommRingCat) → P () ) (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 () 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 ())) (hs : ) :
s = 0
@[simp]
theorem AlgebraicGeometry.basicOpen_eq_bot_iff {U : TopologicalSpace.Opens X.toPresheafedSpace} (s : ↑(X.presheaf.obj ())) :
s = 0

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

Instances
theorem AlgebraicGeometry.isIntegralOfOpenImmersion (f : X Y) [Nonempty X.toPresheafedSpace] :
theorem AlgebraicGeometry.isIntegralOfIsAffineIsDomain [Nonempty X.toPresheafedSpace] [h : IsDomain ↑(X.presheaf.obj ())] :
theorem AlgebraicGeometry.map_injective_of_isIntegral {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)