Open subsets of schemes

This file records general-purpose facts about open subsets of schemes.

Main declarations

• TauCeti.AlgebraicGeometry.Scheme.instNonemptyTop states that the whole space is a nonempty open subset of any nonempty scheme.
• AlgebraicGeometry.IsAffineOpen.presheaf_map_fromSpec_appIso_hom identifies restriction of structure-sheaf sections along the affine chart Spec Γ(X, U).
• AlgebraicGeometry.Scheme.Hom.appLE_eq_id_of_eq_id identifies the restriction maps of a scheme endomorphism equal to the identity.

theorem AlgebraicGeometry.Scheme.Hom.appLE_eq_id_of_eq_id {X : Scheme} {f : X ⟶ X} (hf : f = CategoryTheory.CategoryStruct.id X) (U : X.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj U) : appLE f U U e = CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op U))

If an endomorphism f of X equals the identity, then so does each of its restriction maps Γ(X, U) ⟶ Γ(X, U).

theorem AlgebraicGeometry.IsAffineOpen.presheaf_map_fromSpec_appIso_hom {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (V : (Spec (X.presheaf.obj (Opposite.op U))).Opens) : CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) (Scheme.Hom.appIso hU.fromSpec V).hom = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv ((Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (TopologicalSpace.Opens.leTop V).op)

Along the open immersion hU.fromSpec : Spec Γ(X, U) ⟶ X onto an affine open U, restricting a section of 𝒪_X from U to the image of an open V and transporting it to V gives the restriction to V of the corresponding global section of Spec Γ(X, U).

theorem AlgebraicGeometry.IsAffineOpen.presheaf_map_fromSpec_appIso_hom_assoc {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (V : (Spec (X.presheaf.obj (Opposite.op U))).Opens) {Z : CommRingCat} (h : (Spec (X.presheaf.obj (Opposite.op U))).presheaf.obj (Opposite.op V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.homOfLE ⋯).op) (CategoryTheory.CategoryStruct.comp (Scheme.Hom.appIso hU.fromSpec V).hom h) = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv (CategoryTheory.CategoryStruct.comp ((Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (TopologicalSpace.Opens.leTop V).op) h)

Along the open immersion hU.fromSpec : Spec Γ(X, U) ⟶ X onto an affine open U, restricting a section of 𝒪_X from U to the image of an open V and transporting it to V gives the restriction to V of the corresponding global section of Spec Γ(X, U).

instance TauCeti.AlgebraicGeometry.Scheme.instNonemptyTop {X : AlgebraicGeometry.Scheme} [Nonempty ↥X] : Nonempty ↥↑⊤

The whole space is a nonempty open subset of a nonempty scheme.