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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.obj { unop := U })

theorem AlgebraicGeometry.IsReduced.component_reduced {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsReduced X] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) : IsReduced ↑(X.presheaf.obj { unop := U })

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

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

Equations

• ⋯ = ⋯

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

instance AlgebraicGeometry.instIsReducedSpecOfIsReducedαCommRing {R : CommRingCat} [H : IsReduced ↑R] : AlgebraicGeometry.IsReduced (AlgebraicGeometry.Spec R)

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.isReduced_of_isAffine_isReduced (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] [IsReduced ↑(X.presheaf.obj { unop := ⊤ })] : AlgebraicGeometry.IsReduced X

theorem AlgebraicGeometry.reduce_to_affine_global (P : {X : AlgebraicGeometry.Scheme} → TopologicalSpace.Opens ↑↑X.toPresheafedSpace → Prop) {X : AlgebraicGeometry.Scheme} (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (h₁ : ∀ (X : AlgebraicGeometry.Scheme) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace), (∀ (x : ↥U), ∃ (V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) (_ : ↑x ∈ V) (x : V ⟶ U), P V) → P 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 { carrier := U, is_open' := ⋯ } → P { carrier := V, is_open' := ⋯ }) (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 : AlgebraicGeometry.Scheme) → ↑↑X.toPresheafedSpace → Prop) (h₁ : ∀ (R : CommRingCat) (x : ↑↑(AlgebraicGeometry.Spec R).toPresheafedSpace), P (AlgebraicGeometry.Spec 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 { unop := 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.obj { unop := U })) : X.basicOpen s = ⊥ ↔ s = 0

class AlgebraicGeometry.IsIntegral (X : AlgebraicGeometry.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 : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [inst : Nonempty ↥U], IsDomain ↑(X.presheaf.obj { unop := U })

theorem AlgebraicGeometry.IsIntegral.nonempty {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsIntegral X] : Nonempty ↑↑X.toPresheafedSpace

theorem AlgebraicGeometry.IsIntegral.component_integral {X : AlgebraicGeometry.Scheme} [self : AlgebraicGeometry.IsIntegral X] (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [Nonempty ↥U] : IsDomain ↑(X.presheaf.obj { unop := U })

instance AlgebraicGeometry.instIsDomainαCommRingObjOppositeOpensTopologicalSpaceCarrierCommRingCatPresheafOpTopOfIsIntegral (X : AlgebraicGeometry.Scheme) [h : AlgebraicGeometry.IsIntegral X] : IsDomain ↑(X.presheaf.obj { unop := ⊤ })

Equations

• ⋯ = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

theorem AlgebraicGeometry.isIntegral_of_isOpenImmersion {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αTopologicalSpaceCarrierCommRingCatSpecOfIsDomainCommRing {R : CommRingCat} [IsDomain ↑R] : IrreducibleSpace ↑↑(AlgebraicGeometry.Spec R).toPresheafedSpace

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

theorem AlgebraicGeometry.isIntegral_of_isAffine_of_isDomain (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] [Nonempty ↑↑X.toPresheafedSpace] [IsDomain ↑(X.presheaf.obj { unop := ⊤ })] : 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.map i.op)