mathlib3 documentation

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]

def algebraic_geometry.Scheme.carrier.t0_space (X : algebraic_geometry.Scheme) :

t0_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

@[protected, instance]

def algebraic_geometry.Scheme.carrier.quasi_sober (X : algebraic_geometry.Scheme) :

quasi_sober ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

@[class]

structure algebraic_geometry.is_reduced (X : algebraic_geometry.Scheme) :

Prop

component_reduced : (∀ (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), is_reduced ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) . "apply_instance"

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

Instances of this typeclass

theorem algebraic_geometry.is_reduced_of_stalk_is_reduced (X : algebraic_geometry.Scheme) [∀ (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), is_reduced ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x)] :

algebraic_geometry.is_reduced X

@[protected, instance]

def algebraic_geometry.stalk_is_reduced_of_reduced (X : algebraic_geometry.Scheme) [algebraic_geometry.is_reduced X] (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

is_reduced ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.stalk x)

theorem algebraic_geometry.is_reduced_of_open_immersion {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [H : algebraic_geometry.is_open_immersion f] [algebraic_geometry.is_reduced Y] :

algebraic_geometry.is_reduced X

@[protected, instance]

def algebraic_geometry.obj.is_reduced {R : CommRing} [H : is_reduced ↥R] :

algebraic_geometry.is_reduced (algebraic_geometry.Scheme.Spec.obj (opposite.op R))

theorem algebraic_geometry.affine_is_reduced_iff (R : CommRing) :

algebraic_geometry.is_reduced (algebraic_geometry.Scheme.Spec.obj (opposite.op R)) ↔ is_reduced ↥R

theorem algebraic_geometry.is_reduced_of_is_affine_is_reduced (X : algebraic_geometry.Scheme) [algebraic_geometry.is_affine X] [h : is_reduced ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))] :

algebraic_geometry.is_reduced X

theorem algebraic_geometry.reduce_to_affine_global (P : Π (X : algebraic_geometry.Scheme), topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) → Prop) (h₁ : ∀ (X : algebraic_geometry.Scheme) (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), (∀ (x : ↥U), ∃ {V : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (h : x.val ∈ V) (i : V ⟶ U), P X V) → P X U) (h₂ : ∀ {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [hf : algebraic_geometry.is_open_immersion f], ∃ {U : set ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} {V : set ↥(Y.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (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 (algebraic_geometry.Scheme.Spec.obj (opposite.op R)) ⊤) (X : algebraic_geometry.Scheme) (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

P X U

To show that a statement P holds for all open subsets of all schemes, it suffices to show that

In any scheme X, if P holds for an open cover of U, then P holds for U.
For an open immerison f : X ⟶ Y, if P holds for the entire space of X, then P holds for the image of f.
P holds for the entire space of an affine scheme.

theorem algebraic_geometry.reduce_to_affine_nbhd (P : Π (X : algebraic_geometry.Scheme), ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) → Prop) (h₁ : ∀ (R : CommRing) (x : prime_spectrum ↥R), P (algebraic_geometry.Scheme.Spec.obj (opposite.op R)) x) (h₂ : ∀ {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [_inst_1 : algebraic_geometry.is_open_immersion f] (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)), P X x → P Y (⇑(f.val.base) x)) (X : algebraic_geometry.Scheme) (x : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) :

P X x

theorem algebraic_geometry.eq_zero_of_basic_open_eq_bot {X : algebraic_geometry.Scheme} [hX : algebraic_geometry.is_reduced X] {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (s : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) (hs : X.basic_open s = ⊥) :

s = 0

@[simp]

theorem algebraic_geometry.basic_open_eq_bot_iff {X : algebraic_geometry.Scheme} [algebraic_geometry.is_reduced X] {U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)} (s : ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) :

X.basic_open s = ⊥ ↔ s = 0

@[class]

structure algebraic_geometry.is_integral (X : algebraic_geometry.Scheme) :

Prop

nonempty : nonempty ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) . "apply_instance"
component_integral : (∀ (U : topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)) [_inst_1 : nonempty ↥U], is_domain ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op U))) . "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]

def algebraic_geometry.obj.is_domain (X : algebraic_geometry.Scheme) [h : algebraic_geometry.is_integral X] :

is_domain ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.presheaf.obj (opposite.op ⊤))

@[protected, instance]

def algebraic_geometry.is_reduced_of_is_integral (X : algebraic_geometry.Scheme) [algebraic_geometry.is_integral X] :

algebraic_geometry.is_reduced X

@[protected, instance]

def algebraic_geometry.is_irreducible_of_is_integral (X : algebraic_geometry.Scheme) [algebraic_geometry.is_integral X] :

irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

theorem algebraic_geometry.is_integral_of_is_irreducible_is_reduced (X : algebraic_geometry.Scheme) [algebraic_geometry.is_reduced X] [H : irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

algebraic_geometry.is_integral X

theorem algebraic_geometry.is_integral_iff_is_irreducible_and_is_reduced (X : algebraic_geometry.Scheme) :

algebraic_geometry.is_integral X ↔ irreducible_space ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) ∧ algebraic_geometry.is_reduced X

theorem algebraic_geometry.is_integral_of_open_immersion {X Y : algebraic_geometry.Scheme} (f : X ⟶ Y) [H : algebraic_geometry.is_open_immersion f] [algebraic_geometry.is_integral Y] [nonempty ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)] :

algebraic_geometry.is_integral X

@[protected, instance]

def algebraic_geometry.carrier.irreducible_space {R : CommRing} [H : is_domain ↥R] :

irreducible_space ↥((algebraic_geometry.Scheme.Spec.obj (opposite.op R)).to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier)

@[protected, instance]

def algebraic_geometry.obj.is_integral {R : CommRing} [is_domain ↥R] :

algebraic_geometry.is_integral (algebraic_geometry.Scheme.Spec.obj (opposite.op R))

theorem algebraic_geometry.affine_is_integral_iff (R : CommRing) :

algebraic_geometry.is_integral (algebraic_geometry.Scheme.Spec.obj (opposite.op R)) ↔ is_domain ↥R