# mathlib3documentation

algebraic_geometry.properties

# Basic properties of schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 (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 {carrier := U, is_open' := _} P Y {carrier := V, is_open' := _}) (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 x P Y ((f.val.base) x))  :
P X x
@[simp]
@[class]
structure algebraic_geometry.is_integral  :
Prop
• nonempty : . "apply_instance"
• component_integral : . "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]
@[protected, instance]