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

Equations

• (_ : T0Space ↑↑X.toPresheafedSpace) = (_ : T0Space ↑↑X.toPresheafedSpace)

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

Equations

• (_ : QuasiSober ↑↑X.toPresheafedSpace) = (_ : QuasiSober ((CategoryTheory.forget TopCat).toPrefunctor.obj ↑X.toPresheafedSpace))

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

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

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

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)

Equations

• (_ : IsReduced ↑(TopCat.Presheaf.stalk X.presheaf x)) = (_ : 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.toPrefunctor.obj (Opposite.op R))

Equations

• One or more equations did not get rendered due to their size.

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

theorem AlgebraicGeometry.isReducedOfIsAffineIsReduced (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] [h : IsReduced ↑(X.presheaf.toPrefunctor.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 : ↥U), ∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : ↑x ∈ V) (x : V ⟶ U), P X V) → P X U) (h₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [hf : AlgebraicGeometry.IsOpenImmersion f], ∃ (U : Set ↑↑X.toPresheafedSpace) (V : Set ↑↑Y.toPresheafedSpace) (hU : U = ⊤) (hV : V = Set.range ⇑f.val.base), P X { carrier := U, is_open' := (_ : IsOpen U) } → P Y { carrier := V, is_open' := (_ : IsOpen V) }) (h₃ : ∀ (R : CommRingCat), P (AlgebraicGeometry.Scheme.Spec.toPrefunctor.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.toPrefunctor.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.toPrefunctor.obj (Opposite.op U))) (hs : X.basicOpen s = ⊥) : s = 0

@[simp]

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

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

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

• nonempty : Nonempty ↑↑X.toPresheafedSpace
• component_integral : ∀ (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [inst : Nonempty ↥U], IsDomain ↑(X.presheaf.toPrefunctor.obj (Opposite.op U))

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

Equations

• (_ : IsDomain ↑(X.presheaf.toPrefunctor.obj (Opposite.op ⊤))) = (_ : IsDomain ↑(X.presheaf.toPrefunctor.obj (Opposite.op ⊤)))

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

Equations

• (_ : AlgebraicGeometry.IsReduced X) = (_ : AlgebraicGeometry.IsReduced X)

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

Equations

• (_ : IrreducibleSpace ↑↑X.toPresheafedSpace) = (_ : 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.toPrefunctor.obj (Opposite.op R)).toPresheafedSpace

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

theorem AlgebraicGeometry.isIntegralOfIsAffineIsDomain (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] [Nonempty ↑↑X.toPresheafedSpace] [h : IsDomain ↑(X.presheaf.toPrefunctor.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 ↥U] : Function.Injective ⇑(X.presheaf.toPrefunctor.map i.op)