# mathlibdocumentation

algebraic_geometry.properties

# Basic properties of schemes #

We provide some basic properties of schemes

## Main definition #

• algebraic_geometry.is_integral: A scheme is integral if it is nontrivial and all nontrivial components of the structure sheaf are integral domains.
• algebraic_geometry.is_reduced: A scheme is reduced if all the components of the structure sheaf is reduced.
@[protected, instance]
@[protected, instance]
@[class]
structure algebraic_geometry.is_reduced  :
Prop
• component_reduced : . "apply_instance"

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]
theorem algebraic_geometry.reduce_to_affine_global (P : Π (X : algebraic_geometry.Scheme), ) (h₁ : ∀ (X : algebraic_geometry.Scheme) (U : , (∀ (x : U), ∃ {V : (h : x.val V) (i : V U), P X V)P X U) (h₂ : ∀ {X Y : algebraic_geometry.Scheme} (f : X Y) [hf : , ∃ {U : {V : (hU : U = ) (hV : V = set.range (f.val.base)), P X U, _⟩P Y V, _⟩) (h₃ : ∀ (R : CommRing), )  :
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 algebraic_geometry.reduce_to_affine_nbhd (P : Π (X : algebraic_geometry.Scheme), ) (h₁ : ∀ (R : CommRing) (x : , x) (h₂ : ∀ {X Y : algebraic_geometry.Scheme} (f : X Y) [_inst_1 : (x : (X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), P X xP Y ((f.val.base) x))  :
P X x
@[simp]
@[class]
structure algebraic_geometry.is_integral  :
Prop
• nonempty : . "apply_instance"
• component_integral : (∀ (U : [_inst_1 : , . "apply_instance"

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]