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.instT0SpaceαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceInstTopologicalSpaceαCarrierToPresheafedSpace (X : AlgebraicGeometry.Scheme) : T0Space ↑↑X.toPresheafedSpace

instance AlgebraicGeometry.instQuasiSoberαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceInstTopologicalSpaceαCarrierToPresheafedSpace (X : AlgebraicGeometry.Scheme) : QuasiSober ↑↑X.toPresheafedSpace

class AlgebraicGeometry.IsReduced (X : AlgebraicGeometry.Scheme) : Prop

• component_reduced : ∀ (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), IsReduced ↑(X.presheaf.obj (Opposite.op U))

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

theorem AlgebraicGeometry.isReducedOfStalkIsReduced (X : AlgebraicGeometry.Scheme) [∀ (x : ↑↑X.toPresheafedSpace), IsReduced ↑(TopCat.Presheaf.stalk X.presheaf x)] : AlgebraicGeometry.IsReduced X

instance AlgebraicGeometry.stalk_isReduced_of_reduced (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsReduced X] (x : ↑↑X.toPresheafedSpace) : IsReduced ↑(TopCat.Presheaf.stalk X.presheaf x)

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

instance AlgebraicGeometry.instIsReducedObjOppositeCommRingCatToQuiverToCategoryStructOppositeInstCommRingCatLargeCategorySchemeInstCategorySchemeToPrefunctorSpecOp {R : CommRingCat} [H : IsReduced ↑R] : AlgebraicGeometry.IsReduced (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R))

theorem AlgebraicGeometry.affine_isReduced_iff (R : CommRingCat) : AlgebraicGeometry.IsReduced (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) ↔ IsReduced ↑R

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

theorem AlgebraicGeometry.reduce_to_affine_global (P : (X : AlgebraicGeometry.Scheme) → TopologicalSpace.Opens ↑↑X.toPresheafedSpace → Prop) (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 : AlgebraicGeometry.IsOpenImmersion f], ∃ U V hU hV, P X { carrier := U, is_open' := (_ : IsOpen U) } → P Y { carrier := V, is_open' := (_ : IsOpen V) }) (h₃ : (R : CommRingCat) → P (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) ⊤) (X : AlgebraicGeometry.Scheme) (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.toPresheafedSpace → Prop) (h₁ : (R : CommRingCat) → (x : PrimeSpectrum ↑R) → P (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) x) (h₂ : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → [inst : AlgebraicGeometry.IsOpenImmersion f] → (x : ↑↑X.toPresheafedSpace) → P X x → P Y (↑f.val.base x)) (X : AlgebraicGeometry.Scheme) (x : ↑↑X.toPresheafedSpace) : P X x

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

@[simp]

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

class AlgebraicGeometry.IsIntegral (X : AlgebraicGeometry.Scheme) : Prop

• nonempty : Nonempty ↑↑X.toPresheafedSpace
• component_integral : ∀ (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [inst : Nonempty { x // x ∈ U }], IsDomain ↑(X.presheaf.obj (Opposite.op U))

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

instance AlgebraicGeometry.instIsDomainαCommRingObjOppositeOpensTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceTopologicalSpace_coeToQuiverToCategoryStructOppositeSmallCategoryToPreorderToPartialOrderToCompleteSemilatticeInfInstCompleteLatticeOpensToQuiverToCategoryStructToPrefunctorPresheafOpTopToTopToSemiringToCommSemiringInstCommRingα (X : AlgebraicGeometry.Scheme) [h : AlgebraicGeometry.IsIntegral X] : IsDomain ↑(X.presheaf.obj (Opposite.op ⊤))

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

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

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

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

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

instance AlgebraicGeometry.instIrreducibleSpaceαTopologicalSpaceCarrierCommRingCatInstCommRingCatLargeCategoryToPresheafedSpaceToSheafedSpaceToLocallyRingedSpaceObjOppositeToQuiverToCategoryStructOppositeSchemeInstCategorySchemeToPrefunctorSpecOpInstTopologicalSpaceαCarrierToPresheafedSpace {R : CommRingCat} [H : IsDomain ↑R] : IrreducibleSpace ↑↑(AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)).toPresheafedSpace

instance AlgebraicGeometry.instIsIntegralObjOppositeCommRingCatToQuiverToCategoryStructOppositeInstCommRingCatLargeCategorySchemeInstCategorySchemeToPrefunctorSpecOp {R : CommRingCat} [IsDomain ↑R] : AlgebraicGeometry.IsIntegral (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R))

theorem AlgebraicGeometry.affine_isIntegral_iff (R : CommRingCat) : AlgebraicGeometry.IsIntegral (AlgebraicGeometry.Scheme.Spec.obj (Opposite.op R)) ↔ IsDomain ↑R

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

theorem AlgebraicGeometry.map_injective_of_isIntegral (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsIntegral X] {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)