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.

instance AlgebraicGeometry.instT0SpaceCarrierCarrierCommRingCat (X : Scheme) : T0Space ↑↑X.toPresheafedSpace

instance AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat (X : Scheme) : QuasiSober ↑↑X.toPresheafedSpace

class AlgebraicGeometry.IsReduced (X : Scheme) : Prop

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

• component_reduced (U : X.Opens) : _root_.IsReduced ↑(X.presheaf.obj (Opposite.op U))

theorem AlgebraicGeometry.isReduced_of_isReduced_stalk (X : Scheme) [∀ (x : ↑↑X.toPresheafedSpace), _root_.IsReduced ↑(X.presheaf.stalk x)] : IsReduced X

instance AlgebraicGeometry.isReduced_stalk_of_isReduced (X : Scheme) [IsReduced X] (x : ↑↑X.toPresheafedSpace) : _root_.IsReduced ↑(X.presheaf.stalk x)

theorem AlgebraicGeometry.isReduced_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] [IsReduced Y] : IsReduced X

instance AlgebraicGeometry.instIsReducedSpecOfIsReducedCarrier {R : CommRingCat} [H : _root_.IsReduced ↑R] : IsReduced (Spec R)

theorem AlgebraicGeometry.affine_isReduced_iff (R : CommRingCat) : IsReduced (Spec R) ↔ _root_.IsReduced ↑R

theorem AlgebraicGeometry.isReduced_of_isAffine_isReduced (X : Scheme) [IsAffine X] [_root_.IsReduced ↑(X.presheaf.obj (Opposite.op ⊤))] : IsReduced X

theorem AlgebraicGeometry.reduce_to_affine_global (P : {X : Scheme} → X.Opens → Prop) {X : Scheme} (U : X.Opens) (h₁ : ∀ (X : Scheme) (U : X.Opens), (∀ (x : ↥U), ∃ (V : X.Opens) (_ : ↑x ∈ V) (x : V ⟶ U), P V) → P U) (h₂ : ∀ (X Y : Scheme) (f : X ⟶ Y) [inst : IsOpenImmersion f], ∃ (U : X.Opens) (V : Y.Opens), U = ⊤ ∧ V = Scheme.Hom.opensRange f ∧ (P U → P V)) (h₃ : ∀ (R : CommRingCat), P ⊤) : P 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 : Scheme) → ↑↑X.toPresheafedSpace → Prop) (h₁ : ∀ (R : CommRingCat) (x : ↑↑(Spec R).toPresheafedSpace), P (Spec R) x) (h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsOpenImmersion f] (x : ↑↑X.toPresheafedSpace), P X x → P Y ((CategoryTheory.ConcreteCategory.hom f.base) x)) (X : Scheme) (x : ↑↑X.toPresheafedSpace) : P X x

theorem AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot {X : Scheme} [hX : IsReduced X] {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) (hs : X.basicOpen s = ⊥) : s = 0

@[simp]

theorem AlgebraicGeometry.basicOpen_eq_bot_iff {X : Scheme} [IsReduced X] {U : X.Opens} (s : ↑(X.presheaf.obj (Opposite.op U))) : X.basicOpen s = ⊥ ↔ s = 0

class AlgebraicGeometry.IsIntegral (X : Scheme) : Prop

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

• nonempty : Nonempty ↑↑X.toPresheafedSpace
• component_integral (U : X.Opens) [Nonempty ↑↑(↑U).toPresheafedSpace] : IsDomain ↑(X.presheaf.obj (Opposite.op U))

instance AlgebraicGeometry.instIsDomainCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopOfIsIntegral (X : Scheme) [IsIntegral X] : IsDomain ↑(X.presheaf.obj (Opposite.op ⊤))

@[instance 900]

instance AlgebraicGeometry.isReduced_of_isIntegral (X : Scheme) [IsIntegral X] : IsReduced X

instance AlgebraicGeometry.Scheme.component_nontrivial (X : Scheme) (U : X.Opens) [Nonempty ↑↑(↑U).toPresheafedSpace] : Nontrivial ↑(X.presheaf.obj (Opposite.op U))

instance AlgebraicGeometry.irreducibleSpace_of_isIntegral (X : Scheme) [IsIntegral X] : IrreducibleSpace ↑↑X.toPresheafedSpace

theorem AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced (X : Scheme) [IsReduced X] [H : IrreducibleSpace ↑↑X.toPresheafedSpace] : IsIntegral X

theorem AlgebraicGeometry.isIntegral_iff_irreducibleSpace_and_isReduced (X : Scheme) : IsIntegral X ↔ IrreducibleSpace ↑↑X.toPresheafedSpace ∧ IsReduced X

theorem AlgebraicGeometry.isIntegral_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f] [IsIntegral Y] [Nonempty ↑↑X.toPresheafedSpace] : IsIntegral X

instance AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatSpecOfIsDomainCarrier {R : CommRingCat} [IsDomain ↑R] : IrreducibleSpace ↑↑(Spec R).toPresheafedSpace

instance AlgebraicGeometry.instIsIntegralSpecOfIsDomainCarrier {R : CommRingCat} [IsDomain ↑R] : IsIntegral (Spec R)

theorem AlgebraicGeometry.affine_isIntegral_iff (R : CommRingCat) : IsIntegral (Spec R) ↔ IsDomain ↑R

theorem AlgebraicGeometry.isIntegral_of_isAffine_of_isDomain (X : Scheme) [IsAffine X] [Nonempty ↑↑X.toPresheafedSpace] [IsDomain ↑(X.presheaf.obj (Opposite.op ⊤))] : IsIntegral X

theorem AlgebraicGeometry.map_injective_of_isIntegral (X : Scheme) [IsIntegral X] {U V : X.Opens} (i : U ⟶ V) [H : Nonempty ↑↑(↑U).toPresheafedSpace] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op))