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

instance AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat (X : Scheme) : QuasiSober ↥X

instance AlgebraicGeometry.instPrespectralSpaceCarrierCarrierCommRingCat {X : Scheme} : PrespectralSpace ↥X

instance AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms fun (x : Scheme) => IrreducibleSpace ↥x

instance AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeConnectedSpaceCarrierCarrierCommRingCat : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms fun (x : Scheme) => ConnectedSpace ↥x

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), _root_.IsReduced ↑(X.presheaf.stalk x)] : IsReduced X

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

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

instance AlgebraicGeometry.instIsReducedToScheme {X : Scheme} {U : X.Opens} [IsReduced X] : IsReduced ↑U

instance AlgebraicGeometry.instIsReducedXScheme (X : Scheme) {𝒰 : X.OpenCover} [IsReduced X] (i : 𝒰.I₀) : IsReduced (𝒰.X i)

instance AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIsReduced : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms fun (x : Scheme) => 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.IsReduced.of_openCover (X : Scheme) (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), IsReduced (𝒰.X i)] : IsReduced X

theorem AlgebraicGeometry.IsReduced.iff_of_openCover (X : Scheme) (𝒰 : X.OpenCover) : IsReduced X ↔ ∀ (i : 𝒰.I₀), IsReduced (𝒰.X i)

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 immersion 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 → Prop) (h₁ : ∀ (R : CommRingCat) (x : ↥(Spec R)), P (Spec R) x) (h₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] (x : ↥X), P X x → P Y (f x)) (X : Scheme) (x : ↥X) : 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

theorem AlgebraicGeometry.isField_stalk_of_closure_mem_irreducibleComponents (X : Scheme) (x : ↥X) (hx : closure {x} ∈ irreducibleComponents ↥X) [IsReduced X] : IsField ↑(X.presheaf.stalk x)

If X is reduced and has finitely many irreducible components, then the stalks at the generic points of the irreducible components are fields.

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
• component_integral (U : X.Opens) [Nonempty ↥↑U] : 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] : Nontrivial ↑(X.presheaf.obj (Opposite.op U))

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

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

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

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

theorem AlgebraicGeometry.IsIntegral.of_isIso {X Y : Scheme} [h : IsIntegral X] (f : X ⟶ Y) [CategoryTheory.IsIso f] : IsIntegral Y

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

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] [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] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op))

@[instance_reducible]

noncomputable instance AlgebraicGeometry.instOrderTopCarrierCarrierCommRingCatOfIsIntegral (X : Scheme) [IsIntegral X] : OrderTop ↥X

Equations

• AlgebraicGeometry.instOrderTopCarrierCarrierCommRingCatOfIsIntegral X = { top := genericPoint ↥X, le_top := ⋯ }

theorem AlgebraicGeometry.coheight_eq_of_isOpenImmersion {U X : Scheme} {x : ↥U} (f : U ⟶ X) [IsOpenImmersion f] : Order.coheight (f x) = Order.coheight x

Stacks Tag 02I4

theorem AlgebraicGeometry.idealHeight_eq_coheight (R : CommRingCat) (x : ↥(Spec R)) : x.asIdeal.height = Order.coheight x

theorem AlgebraicGeometry.ringKrullDim_stalk_eq_coheight {X : Scheme} (x : ↥X) : ringKrullDim ↑(X.presheaf.stalk x) = ↑(Order.coheight x)

Stacks Tag 02IZ

theorem AlgebraicGeometry.krullDimLE_of_coheight_le {X : Scheme} {z : ↥X} {n : ℕ} (hz : Order.coheight z ≤ ↑n) : Ring.KrullDimLE n ↑(X.presheaf.stalk z)

theorem AlgebraicGeometry.isField_of_isIntegral_of_subsingleton (X : Scheme) [IsIntegral X] [Subsingleton ↥X] : IsField ↑(X.presheaf.obj (Opposite.op ⊤))