The category of schemes

A scheme is a locally ringed space such that every point is contained in some open set where there is an isomorphism of presheaves between the restriction to that open set, and the structure sheaf of Spec R, for some commutative ring R.

A morphism of schemes is just a morphism of the underlying locally ringed spaces.

structure AlgebraicGeometry.Schemeextends AlgebraicGeometry.LocallyRingedSpace : Type (u_1 + 1)

We define Scheme as an X : LocallyRingedSpace, along with a proof that every point has an open neighbourhood U so that the restriction of X to U is isomorphic, as a locally ringed space, to Spec.toLocallyRingedSpace.obj (op R) for some R : CommRingCat.

• carrier : TopCat
• presheaf : TopCat.Presheaf CommRingCat ↑self.toPresheafedSpace
• IsSheaf : self.presheaf.IsSheaf
• isLocalRing (x : ↥self) : IsLocalRing ↑(self.presheaf.stalk x)
• local_affine (x : ↑self.toTopCat) : ∃ (U : TopologicalSpace.OpenNhds x) (R : CommRingCat), Nonempty (self.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (Opposite.op R))

instance AlgebraicGeometry.Scheme.instCoeSortType : CoeSort Scheme (Type u_1)

def AlgebraicGeometry.Scheme.delabAdjoinNotation : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer for coercing schemes to types.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Opens (X : Scheme) : Type u_1

The type of open sets of a scheme.

structure AlgebraicGeometry.Scheme.Hom (X Y : Scheme) extends X.Hom Y.toLocallyRingedSpace : Type u_1

A morphism between schemes is a morphism between the underlying locally ringed spaces.

• base : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
• c : Y.presheaf ⟶ (TopCat.Presheaf.pushforward CommRingCat self.base).obj X.presheaf
• prop (x : ↥X) : IsLocalHom (CommRingCat.Hom.hom (self.stalkMap x))

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Hom.toLRSHom {X Y : Scheme} (f : X.Hom Y) : X.toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace

Cast a morphism of schemes into morphisms of local ringed spaces.

def AlgebraicGeometry.Scheme.Hom.Simps.toLRSHom {X Y : Scheme} (f : X.Hom Y) : X.toLocallyRingedSpace ⟶ Y.toLocallyRingedSpace

See Note [custom simps projection]

instance AlgebraicGeometry.Scheme.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} Scheme

Schemes are a full subcategory of locally ringed spaces.

def AlgebraicGeometry.«term_⁻¹ᵁ_» : Lean.TrailingParserDescr

f ⁻¹ᵁ U is notation for (Opens.map f.base).obj U, the preimage of an open set U under f. The preferred name in lemmas is preimage and it should be treated as an infix.

def AlgebraicGeometry.«termΓ(_,_)» : Lean.ParserDescr

Γ(X, U) is notation for X.presheaf.obj (op U).

instance AlgebraicGeometry.Scheme.instCoeFunHomForallCarrierCarrierCommRingCat {X Y : Scheme} : CoeFun (X ⟶ Y) fun (x : X ⟶ Y) => ↥X → ↥Y

def AlgebraicGeometry.Scheme.delabCoeFunNotation : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer for coercing morphisms between schemes to functions.

def AlgebraicGeometry.Scheme.delabCoeFunAppNotation : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer for applying morphisms of schemes to set-theoretic points.

instance AlgebraicGeometry.Scheme.instSubsingletonCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensBot {X : Scheme} : Subsingleton ↑(X.presheaf.obj (Opposite.op ⊥))

theorem AlgebraicGeometry.Scheme.Hom.continuous {X Y : Scheme} (f : X ⟶ Y) : Continuous ⇑f

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.sheaf (X : Scheme) : TopCat.Sheaf CommRingCat ↑X.toPresheafedSpace

The structure sheaf of a scheme.

instance AlgebraicGeometry.Scheme.instPreorderCarrierCarrierCommRingCat {X : Scheme} : Preorder ↥X

We give schemes the specialization preorder by default.

theorem AlgebraicGeometry.Scheme.le_iff_specializes {X : Scheme} {a b : ↥X} : a ≤ b ↔ b ⤳ a

theorem AlgebraicGeometry.Scheme.height_of_isClosed {X : Scheme} {x : ↥X} (hx : IsClosed {x}) : Order.height x = 0

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Hom.app {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) : Y.presheaf.obj (Opposite.op U) ⟶ X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U))

Given a morphism of schemes f : X ⟶ Y, and open U ⊆ Y, this is the induced map Γ(Y, U) ⟶ Γ(X, f ⁻¹ᵁ U).

This is treated as a suffix in lemma names.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Hom.appTop {X Y : Scheme} (f : X ⟶ Y) : Y.presheaf.obj (Opposite.op ⊤) ⟶ X.presheaf.obj (Opposite.op ⊤)

Given a morphism of schemes f : X ⟶ Y, this is the induced map Γ(Y, ⊤) ⟶ Γ(X, ⊤). This is treated as a suffix in lemma names.

theorem AlgebraicGeometry.Scheme.Hom.naturality {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} (i : Opposite.op U' ⟶ Opposite.op U) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map i) (app f U) = CategoryTheory.CategoryStruct.comp (app f U') (X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op)

theorem AlgebraicGeometry.Scheme.Hom.naturality_assoc {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} (i : Opposite.op U' ⟶ Opposite.op U) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map i) (CategoryTheory.CategoryStruct.comp (app f U) h) = CategoryTheory.CategoryStruct.comp (app f U') (CategoryTheory.CategoryStruct.comp (X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op) h)

def AlgebraicGeometry.Scheme.Hom.appLE {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : Y.presheaf.obj (Opposite.op U) ⟶ X.presheaf.obj (Opposite.op V)

Given a morphism of schemes f : X ⟶ Y, and open sets U ⊆ Y, V ⊆ f ⁻¹' U, this is the induced map Γ(Y, U) ⟶ Γ(X, V).

This is treated as a suffix in lemma names.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appLE_map {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : Opposite.op V ⟶ Opposite.op V') : CategoryTheory.CategoryStruct.comp (appLE f U V e) (X.presheaf.map i) = appLE f U V' ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appLE_map_assoc {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : Opposite.op V ⟶ Opposite.op V') {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V') ⟶ Z) : CategoryTheory.CategoryStruct.comp (appLE f U V e) (CategoryTheory.CategoryStruct.comp (X.presheaf.map i) h) = CategoryTheory.CategoryStruct.comp (appLE f U V' ⋯) h

theorem AlgebraicGeometry.Scheme.Hom.appLE_map' {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : V = V') : CategoryTheory.CategoryStruct.comp (appLE f U V' ⋯) (X.presheaf.map (CategoryTheory.eqToHom i).op) = appLE f U V e

theorem AlgebraicGeometry.Scheme.Hom.appLE_map'_assoc {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} {V V' : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : V = V') {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (appLE f U V' ⋯) (CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom i).op) h) = CategoryTheory.CategoryStruct.comp (appLE f U V e) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.map_appLE {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : Opposite.op U' ⟶ Opposite.op U) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map i) (appLE f U V e) = appLE f U' V ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.map_appLE_assoc {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : Opposite.op U' ⟶ Opposite.op U) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map i) (CategoryTheory.CategoryStruct.comp (appLE f U V e) h) = CategoryTheory.CategoryStruct.comp (appLE f U' V ⋯) h

theorem AlgebraicGeometry.Scheme.Hom.map_appLE' {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : U' = U) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom i).op) (appLE f U' V ⋯) = appLE f U V e

theorem AlgebraicGeometry.Scheme.Hom.map_appLE'_assoc {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (i : U' = U) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom i).op) (CategoryTheory.CategoryStruct.comp (appLE f U' V ⋯) h) = CategoryTheory.CategoryStruct.comp (appLE f U V e) h

theorem AlgebraicGeometry.Scheme.Hom.app_eq_appLE {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} : app f U = appLE f U ((TopologicalSpace.Opens.map f.base).obj U) ⋯

theorem AlgebraicGeometry.Scheme.Hom.appLE_eq_app {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} : appLE f U ((TopologicalSpace.Opens.map f.base).obj U) ⋯ = app f U

theorem AlgebraicGeometry.Scheme.Hom.appLE_congr {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} {V V' : X.Opens} (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (e₁ : U = U') (e₂ : V = V') (P : {R S : CommRingCat} → (R ⟶ S) → Prop) : P (appLE f U V e) ↔ P (appLE f U' V' ⋯)

def AlgebraicGeometry.Scheme.Hom.stalkMap {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : Y.presheaf.stalk (f x) ⟶ X.presheaf.stalk x

A morphism of schemes f : X ⟶ Y induces a local ring homomorphism from Y.presheaf.stalk (f x) to X.presheaf.stalk x for any x : X.

theorem AlgebraicGeometry.Scheme.Hom.ext {X Y : Scheme} {f g : X ⟶ Y} (h_base : f.base = g.base) (h_app : ∀ (U : Y.Opens), CategoryTheory.CategoryStruct.comp (app f U) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) = app g U) : f = g

theorem AlgebraicGeometry.Scheme.Hom.ext' {X Y : Scheme} {f g : X ⟶ Y} (h : toLRSHom f = toLRSHom g) : f = g

An alternative ext lemma for scheme morphisms.

theorem AlgebraicGeometry.Scheme.Hom.mem_preimage {X Y : Scheme} (f : X ⟶ Y) {x : ↥X} {U : Y.Opens} : x ∈ (TopologicalSpace.Opens.map f.base).obj U ↔ f x ∈ U

theorem AlgebraicGeometry.Scheme.Hom.coe_preimage {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} : ↑((TopologicalSpace.Opens.map f.base).obj U) = ⇑f ⁻¹' ↑U

theorem AlgebraicGeometry.Scheme.Hom.preimage_sup {X Y : Scheme} (f : X ⟶ Y) {U V : Y.Opens} : (TopologicalSpace.Opens.map f.base).obj (U ⊔ V) = (TopologicalSpace.Opens.map f.base).obj U ⊔ (TopologicalSpace.Opens.map f.base).obj V

theorem AlgebraicGeometry.Scheme.Hom.preimage_inf {X Y : Scheme} (f : X ⟶ Y) {U V : Y.Opens} : (TopologicalSpace.Opens.map f.base).obj (U ⊓ V) = (TopologicalSpace.Opens.map f.base).obj U ⊓ (TopologicalSpace.Opens.map f.base).obj V

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimage_top {X Y : Scheme} (f : X ⟶ Y) : (TopologicalSpace.Opens.map f.base).obj ⊤ = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.preimage_bot {X Y : Scheme} (f : X ⟶ Y) : (TopologicalSpace.Opens.map f.base).obj ⊥ = ⊥

theorem AlgebraicGeometry.Scheme.Hom.preimage_iSup {X Y : Scheme} (f : X ⟶ Y) {ι : Sort u_1} (U : ι → Y.Opens) : (TopologicalSpace.Opens.map f.base).obj (iSup U) = ⨆ (i : ι), (TopologicalSpace.Opens.map f.base).obj (U i)

theorem AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top {X Y : Scheme} (f : X ⟶ Y) {ι : Sort u_1} {U : ι → Y.Opens} (hU : iSup U = ⊤) : ⨆ (i : ι), (TopologicalSpace.Opens.map f.base).obj (U i) = ⊤

@[deprecated AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.Hom.preimage_iSup_eq_top {X Y : Scheme} (f : X ⟶ Y) {ι : Sort u_1} {U : ι → Y.Opens} (hU : iSup U = ⊤) : ⨆ (i : ι), (TopologicalSpace.Opens.map f.base).obj (U i) = ⊤

Alias of AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top.

theorem AlgebraicGeometry.Scheme.Hom.preimage_mono {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} (hUU' : U ≤ U') : (TopologicalSpace.Opens.map f.base).obj U ≤ (TopologicalSpace.Opens.map f.base).obj U'

@[deprecated AlgebraicGeometry.Scheme.Hom.preimage_mono (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.Hom.preimage_le_preimage_of_le {X Y : Scheme} (f : X ⟶ Y) {U U' : Y.Opens} (hUU' : U ≤ U') : (TopologicalSpace.Opens.map f.base).obj U ≤ (TopologicalSpace.Opens.map f.base).obj U'

Alias of AlgebraicGeometry.Scheme.Hom.preimage_mono.

theorem AlgebraicGeometry.Scheme.Hom.id_preimage {X : Scheme} (U : X.Opens) : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X).base).obj U = U

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.comp_preimage {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U = (TopologicalSpace.Opens.map f.base).obj ((TopologicalSpace.Opens.map g.base).obj U)

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_preimage (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.preimage_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) : (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U = (TopologicalSpace.Opens.map f.base).obj ((TopologicalSpace.Opens.map g.base).obj U)

Alias of AlgebraicGeometry.Scheme.Hom.comp_preimage.

def AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace : CategoryTheory.Functor Scheme LocallyRingedSpace

The forgetful functor from Scheme to LocallyRingedSpace.

@[simp]

theorem AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_obj (self : Scheme) : forgetToLocallyRingedSpace.obj self = self.toLocallyRingedSpace

@[simp]

theorem AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace_map {X✝ Y✝ : Scheme} (f : X✝.Hom Y✝) : forgetToLocallyRingedSpace.map f = f.toLRSHom

def AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace : forgetToLocallyRingedSpace.FullyFaithful

The forget functor Scheme ⥤ LocallyRingedSpace is fully faithful.

@[simp]

theorem AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace_preimage_toLRSHom {X✝ Y✝ : Scheme} (toLRSHom' : X✝.Hom Y✝.toLocallyRingedSpace) : Hom.toLRSHom (fullyFaithfulForgetToLocallyRingedSpace.preimage toLRSHom') = toLRSHom'

instance AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace : forgetToLocallyRingedSpace.Full

instance AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace : forgetToLocallyRingedSpace.Faithful

def AlgebraicGeometry.Scheme.forgetToTop : CategoryTheory.Functor Scheme TopCat

The forgetful functor from Scheme to TopCat.

@[simp]

theorem AlgebraicGeometry.Scheme.forgetToTop_obj (X : Scheme) : forgetToTop.obj X = (SheafedSpace.forget CommRingCat).obj X.toSheafedSpace

@[simp]

theorem AlgebraicGeometry.Scheme.forgetToTop_map {X✝ Y✝ : Scheme} (f : X✝ ⟶ Y✝) : forgetToTop.map f = (SheafedSpace.forget CommRingCat).map (CategoryTheory.InducedCategory.homMk (Hom.toLRSHom f).toHom)

noncomputable def AlgebraicGeometry.Scheme.homeoOfIso {X Y : Scheme} (e : X ≅ Y) : ↥X ≃ₜ ↥Y

An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.

@[simp]

theorem AlgebraicGeometry.Scheme.coe_homeoOfIso {X Y : Scheme} (e : X ≅ Y) : ⇑(homeoOfIso e) = ⇑e.hom

@[simp]

theorem AlgebraicGeometry.Scheme.coe_homeoOfIso_symm {X Y : Scheme} (e : X ≅ Y) : ⇑(homeoOfIso e.symm) = ⇑e.inv

@[simp]

theorem AlgebraicGeometry.Scheme.homeoOfIso_symm {X Y : Scheme} (e : X ≅ Y) : (homeoOfIso e).symm = homeoOfIso e.symm

theorem AlgebraicGeometry.Scheme.homeoOfIso_apply {X Y : Scheme} (e : X ≅ Y) (x : ↥X) : (homeoOfIso e) x = e.hom x

def CategoryTheory.Iso.schemeIsoToHomeo {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) : ↥X ≃ₜ ↥Y

Alias of AlgebraicGeometry.Scheme.homeoOfIso.

---

An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.

noncomputable def AlgebraicGeometry.Scheme.Hom.homeomorph {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : ↥X ≃ₜ ↥Y

An isomorphism of schemes induces a homeomorphism of the underlying topological spaces.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.homeomorph_apply {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (x : ↥X) : (homeomorph f) x = f x

instance AlgebraicGeometry.Scheme.hasCoeToTopCat : CoeOut Scheme TopCat

def AlgebraicGeometry.Scheme.forgetToTop_obj_eq_coe (X : Scheme) : Prop

forgetful functor to TopCat is the same as coercion

def AlgebraicGeometry.Scheme.forget : CategoryTheory.Functor Scheme (Type u)

The forgetful functor from Scheme to Type.

def AlgebraicGeometry.Scheme.forget_obj_eq_coe (X : Scheme) : Prop

forgetful functor to Scheme is the same as coercion

@[simp]

theorem AlgebraicGeometry.Scheme.forget_obj (X : Scheme) : forget.obj X = ↥X

@[simp]

theorem AlgebraicGeometry.Scheme.forget_map {X Y : Scheme} (f : X ⟶ Y) : forget.map f = ⇑f

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.id_base (X : Scheme) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.id_app {X : Scheme} (U : X.Opens) : app (CategoryTheory.CategoryStruct.id X) U = CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op U))

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.id_appTop {X : Scheme} : appTop (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op ⊤))

theorem AlgebraicGeometry.Scheme.Hom.comp_toLRSHom {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : toLRSHom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (toLRSHom f) (toLRSHom g)

theorem AlgebraicGeometry.Scheme.Hom.comp_toLRSHom_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : LocallyRingedSpace} (h : Z.toLocallyRingedSpace ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (toLRSHom (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (toLRSHom f) (CategoryTheory.CategoryStruct.comp (toLRSHom g) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.comp_base {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

theorem AlgebraicGeometry.Scheme.Hom.comp_base_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : TopCat} (h : ↑Z.toPresheafedSpace ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).base h = CategoryTheory.CategoryStruct.comp f.base (CategoryTheory.CategoryStruct.comp g.base h)

theorem AlgebraicGeometry.Scheme.Hom.comp_apply {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X) : (CategoryTheory.CategoryStruct.comp f g) x = g (f x)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.comp_app {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) : app (CategoryTheory.CategoryStruct.comp f g) U = CategoryTheory.CategoryStruct.comp (app g U) (app f ((TopologicalSpace.Opens.map g.base).obj U))

theorem AlgebraicGeometry.Scheme.Hom.comp_app_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) {Z✝ : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U)) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (app (CategoryTheory.CategoryStruct.comp f g) U) h = CategoryTheory.CategoryStruct.comp (app g U) (CategoryTheory.CategoryStruct.comp (app f ((TopologicalSpace.Opens.map g.base).obj U)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.comp_appTop {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : appTop (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (appTop g) (appTop f)

theorem AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : CommRingCat} (h : X.presheaf.obj (Opposite.op ⊤) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (appTop (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (appTop g) (CategoryTheory.CategoryStruct.comp (appTop f) h)

theorem AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : Y.Opens) (W : X.Opens) (e₁ : V ≤ (TopologicalSpace.Opens.map g.base).obj U) (e₂ : W ≤ (TopologicalSpace.Opens.map f.base).obj V) : CategoryTheory.CategoryStruct.comp (appLE g U V e₁) (appLE f V W e₂) = appLE (CategoryTheory.CategoryStruct.comp f g) U W ⋯

theorem AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : Y.Opens) (W : X.Opens) (e₁ : V ≤ (TopologicalSpace.Opens.map g.base).obj U) (e₂ : W ≤ (TopologicalSpace.Opens.map f.base).obj V) {Z✝ : CommRingCat} (h : X.presheaf.obj (Opposite.op W) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (appLE g U V e₁) (CategoryTheory.CategoryStruct.comp (appLE f V W e₂) h) = CategoryTheory.CategoryStruct.comp (appLE (CategoryTheory.CategoryStruct.comp f g) U W ⋯) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.comp_appLE {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U) : appLE (CategoryTheory.CategoryStruct.comp f g) U V e = CategoryTheory.CategoryStruct.comp (app g U) (appLE f ((TopologicalSpace.Opens.map g.base).obj U) V e)

theorem AlgebraicGeometry.Scheme.Hom.comp_appLE_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U) {Z✝ : CommRingCat} (h : X.presheaf.obj (Opposite.op V) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (appLE (CategoryTheory.CategoryStruct.comp f g) U V e) h = CategoryTheory.CategoryStruct.comp (app g U) (CategoryTheory.CategoryStruct.comp (appLE f ((TopologicalSpace.Opens.map g.base).obj U) V e) h)

theorem AlgebraicGeometry.Scheme.Hom.congr_app {X Y : Scheme} {f g : X ⟶ Y} (e : f = g) (U : Y.Opens) : app f U = CategoryTheory.CategoryStruct.comp (app g U) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)

theorem AlgebraicGeometry.Scheme.Hom.app_eq {X Y : Scheme} (f : X ⟶ Y) {U V : Y.Opens} (e : U = V) : app f U = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) (CategoryTheory.CategoryStruct.comp (app f V) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))

theorem AlgebraicGeometry.Scheme.Hom.eqToHom_app {X Y : Scheme} (e : X = Y) (U : Y.Opens) : app (CategoryTheory.eqToHom e) U = CategoryTheory.eqToHom ⋯

instance AlgebraicGeometry.Scheme.Hom.isIso_toLRSHom {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (toLRSHom f)

instance AlgebraicGeometry.Scheme.Hom.isIso_toPshHom {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.toPshHom

instance AlgebraicGeometry.Scheme.Hom.isIso_base {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.base

instance AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens) : CategoryTheory.IsIso (app f U)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.inv_app {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : X.Opens) : app (CategoryTheory.inv f) U = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) (CategoryTheory.inv (app f ((TopologicalSpace.Opens.map (CategoryTheory.inv f).base).obj U)))

theorem AlgebraicGeometry.Scheme.Hom.inv_appTop {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : appTop (CategoryTheory.inv f) = CategoryTheory.inv (appTop f)

def AlgebraicGeometry.Scheme.Hom.copyBase {X Y : Scheme} (f : X.Hom Y) (g : ↥X → ↥Y) (h : ⇑f = g) : X ⟶ Y

Copies a morphism with a different underlying map

theorem AlgebraicGeometry.Scheme.Hom.copyBase_eq {X Y : Scheme} (f : X.Hom Y) (g : ↥X → ↥Y) (h : ⇑f = g) : f.copyBase g h = f

@[deprecated AlgebraicGeometry.Scheme.Hom.id_base (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.id.base (X : Scheme) : (CategoryTheory.CategoryStruct.id X).base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

Alias of AlgebraicGeometry.Scheme.Hom.id_base.

@[deprecated AlgebraicGeometry.Scheme.Hom.id_app (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.id_app {X : Scheme} (U : X.Opens) : Hom.app (CategoryTheory.CategoryStruct.id X) U = CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op U))

Alias of AlgebraicGeometry.Scheme.Hom.id_app.

@[deprecated AlgebraicGeometry.Scheme.Hom.id_appTop (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.id_appTop {X : Scheme} : Hom.appTop (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (X.presheaf.obj (Opposite.op ⊤))

Alias of AlgebraicGeometry.Scheme.Hom.id_appTop.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_toLRSHom (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_toLRSHom {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.toLRSHom (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Hom.toLRSHom f) (Hom.toLRSHom g)

Alias of AlgebraicGeometry.Scheme.Hom.comp_toLRSHom.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_toLRSHom_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_toLRSHom_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : LocallyRingedSpace} (h : Z.toLocallyRingedSpace ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (Hom.toLRSHom (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (Hom.toLRSHom f) (CategoryTheory.CategoryStruct.comp (Hom.toLRSHom g) h)

Alias of AlgebraicGeometry.Scheme.Hom.comp_toLRSHom_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_base (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_coeBase {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

Alias of AlgebraicGeometry.Scheme.Hom.comp_base.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_base_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_coeBase_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : TopCat} (h : ↑Z.toPresheafedSpace ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).base h = CategoryTheory.CategoryStruct.comp f.base (CategoryTheory.CategoryStruct.comp g.base h)

Alias of AlgebraicGeometry.Scheme.Hom.comp_base_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_base (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_base {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

Alias of AlgebraicGeometry.Scheme.Hom.comp_base.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_base_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_base_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : TopCat} (h : ↑Z.toPresheafedSpace ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).base h = CategoryTheory.CategoryStruct.comp f.base (CategoryTheory.CategoryStruct.comp g.base h)

Alias of AlgebraicGeometry.Scheme.Hom.comp_base_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_apply (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_base_apply {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X) : (CategoryTheory.CategoryStruct.comp f g) x = g (f x)

Alias of AlgebraicGeometry.Scheme.Hom.comp_apply.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_app (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_app {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) : Hom.app (CategoryTheory.CategoryStruct.comp f g) U = CategoryTheory.CategoryStruct.comp (Hom.app g U) (Hom.app f ((TopologicalSpace.Opens.map g.base).obj U))

Alias of AlgebraicGeometry.Scheme.Hom.comp_app.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_app_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_app_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) {Z✝ : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U)) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (Hom.app (CategoryTheory.CategoryStruct.comp f g) U) h = CategoryTheory.CategoryStruct.comp (Hom.app g U) (CategoryTheory.CategoryStruct.comp (Hom.app f ((TopologicalSpace.Opens.map g.base).obj U)) h)

Alias of AlgebraicGeometry.Scheme.Hom.comp_app_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_appTop (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_appTop {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.appTop (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Hom.appTop g) (Hom.appTop f)

Alias of AlgebraicGeometry.Scheme.Hom.comp_appTop.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_appTop_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : CommRingCat} (h : X.presheaf.obj (Opposite.op ⊤) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (Hom.appTop (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (Hom.appTop g) (CategoryTheory.CategoryStruct.comp (Hom.appTop f) h)

Alias of AlgebraicGeometry.Scheme.Hom.comp_appTop_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.appLE_comp_appLE {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : Y.Opens) (W : X.Opens) (e₁ : V ≤ (TopologicalSpace.Opens.map g.base).obj U) (e₂ : W ≤ (TopologicalSpace.Opens.map f.base).obj V) : CategoryTheory.CategoryStruct.comp (Hom.appLE g U V e₁) (Hom.appLE f V W e₂) = Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U W ⋯

Alias of AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_appLE (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_appLE {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U) : Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U V e = CategoryTheory.CategoryStruct.comp (Hom.app g U) (Hom.appLE f ((TopologicalSpace.Opens.map g.base).obj U) V e)

Alias of AlgebraicGeometry.Scheme.Hom.comp_appLE.

@[deprecated AlgebraicGeometry.Scheme.Hom.comp_appLE_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.comp_appLE_assoc {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens) (V : X.Opens) (e : V ≤ (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U) {Z✝ : CommRingCat} (h : X.presheaf.obj (Opposite.op V) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U V e) h = CategoryTheory.CategoryStruct.comp (Hom.app g U) (CategoryTheory.CategoryStruct.comp (Hom.appLE f ((TopologicalSpace.Opens.map g.base).obj U) V e) h)

Alias of AlgebraicGeometry.Scheme.Hom.comp_appLE_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.congr_app (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.congr_app {X Y : Scheme} {f g : X ⟶ Y} (e : f = g) (U : Y.Opens) : Hom.app f U = CategoryTheory.CategoryStruct.comp (Hom.app g U) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op)

Alias of AlgebraicGeometry.Scheme.Hom.congr_app.

@[deprecated AlgebraicGeometry.Scheme.Hom.app_eq (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.app_eq {X Y : Scheme} (f : X ⟶ Y) {U V : Y.Opens} (e : U = V) : Hom.app f U = CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.eqToHom ⋯).op) (CategoryTheory.CategoryStruct.comp (Hom.app f V) (X.presheaf.map (CategoryTheory.eqToHom ⋯).op))

Alias of AlgebraicGeometry.Scheme.Hom.app_eq.

@[deprecated AlgebraicGeometry.Scheme.Hom.eqToHom_app (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.eqToHom_c_app {X Y : Scheme} (e : X = Y) (U : Y.Opens) : Hom.app (CategoryTheory.eqToHom e) U = CategoryTheory.eqToHom ⋯

Alias of AlgebraicGeometry.Scheme.Hom.eqToHom_app.

@[deprecated AlgebraicGeometry.Scheme.Hom.inv_app (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.inv_app {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : X.Opens) : Hom.app (CategoryTheory.inv f) U = CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) (CategoryTheory.inv (Hom.app f ((TopologicalSpace.Opens.map (CategoryTheory.inv f).base).obj U)))

Alias of AlgebraicGeometry.Scheme.Hom.inv_app.

@[deprecated AlgebraicGeometry.Scheme.Hom.inv_appTop (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.inv_appTop {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : Hom.appTop (CategoryTheory.inv f) = CategoryTheory.inv (Hom.appTop f)

Alias of AlgebraicGeometry.Scheme.Hom.inv_appTop.

@[deprecated CategoryTheory.eqToHom_map (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (p : X = Y) : F.map (CategoryTheory.eqToHom p) = CategoryTheory.eqToHom ⋯

Alias of CategoryTheory.eqToHom_map.

def AlgebraicGeometry.Spec (R : CommRingCat) : Scheme

The spectrum of a commutative ring, as a scheme.

The notation Spec(R) for (R : Type*) [CommRing R] to mean Spec (CommRingCat.of R) is enabled in the scope SpecOfNotation. Please do not use it within Mathlib, but it can be used in downstream projects if desired. To use this, do:

import Mathlib.AlgebraicGeometry.Scheme

variable (R : Type*) [CommRing R]

open scoped SpecOfNotation

#check Spec(R)

def SpecOfNotation.«termSpec(_)» : Lean.ParserDescr

The spectrum of an unbundled ring as a scheme. WARNING: This is potentially confusing as Spec (R) and Spec(R) have different meanings. Hence we avoid using it in mathlib but leave it as a scoped instance for downstream projects.

WARNING: If R is already an element of CommRingCat, you should use Spec R instead of Spec(R), which is secretly Spec(↑R).

theorem AlgebraicGeometry.Spec_toLocallyRingedSpace (R : CommRingCat) : (Spec R).toLocallyRingedSpace = Spec.locallyRingedSpaceObj R

def AlgebraicGeometry.Spec.map {R S : CommRingCat} (f : R ⟶ S) : Spec S ⟶ Spec R

The induced map of a ring homomorphism on the ring spectra, as a morphism of schemes.

@[simp]

theorem AlgebraicGeometry.Spec.map_id (R : CommRingCat) : map (CategoryTheory.CategoryStruct.id R) = CategoryTheory.CategoryStruct.id (Spec R)

@[simp]

theorem AlgebraicGeometry.Spec.map_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) : map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map g) (map f)

theorem AlgebraicGeometry.Spec.map_comp_assoc {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T) {Z : Scheme} (h : Spec R ⟶ Z) : CategoryTheory.CategoryStruct.comp (map (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (map g) (CategoryTheory.CategoryStruct.comp (map f) h)

def AlgebraicGeometry.Scheme.Spec : CategoryTheory.Functor CommRingCatᵒᵖ Scheme

The spectrum, as a contravariant functor from commutative rings to schemes.

@[simp]

theorem AlgebraicGeometry.Scheme.Spec_map {X✝ Y✝ : CommRingCatᵒᵖ} (f : X✝ ⟶ Y✝) : Scheme.Spec.map f = Spec.map f.unop

@[simp]

theorem AlgebraicGeometry.Scheme.Spec_obj (R : CommRingCatᵒᵖ) : Scheme.Spec.obj R = Spec (Opposite.unop R)

theorem AlgebraicGeometry.Spec.map_eqToHom {R S : CommRingCat} (e : R = S) : map (CategoryTheory.eqToHom e) = CategoryTheory.eqToHom ⋯

instance AlgebraicGeometry.instIsIsoSchemeMapOfCommRingCat {R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (Spec.map f)

@[simp]

theorem AlgebraicGeometry.Spec.map_inv {R S : CommRingCat} (f : R ⟶ S) [CategoryTheory.IsIso f] : map (CategoryTheory.inv f) = CategoryTheory.inv (map f)

theorem AlgebraicGeometry.Spec_carrier (R : CommRingCat) : ↥(Spec R) = PrimeSpectrum ↑R

theorem AlgebraicGeometry.Spec_sheaf (R : CommRingCat) : (Spec R).sheaf = Spec.structureSheaf ↑R

theorem AlgebraicGeometry.Spec_presheaf (R : CommRingCat) : (Spec R).presheaf = (Spec.structureSheaf ↑R).val

theorem AlgebraicGeometry.Spec.map_base {R S : CommRingCat} (f : R ⟶ S) : (map f).base = TopCat.ofHom { toFun := PrimeSpectrum.comap (CommRingCat.Hom.hom f), continuous_toFun := ⋯ }

theorem AlgebraicGeometry.Spec.map_apply {R S : CommRingCat} (f : R ⟶ S) (x : ↥(Spec S)) : (map f) x = PrimeSpectrum.comap (CommRingCat.Hom.hom f) x

@[deprecated AlgebraicGeometry.Spec.map_apply (since := "2025-10-07")]

theorem AlgebraicGeometry.Spec.map_base_apply {R S : CommRingCat} (f : R ⟶ S) (x : ↥(Spec S)) : (map f) x = PrimeSpectrum.comap (CommRingCat.Hom.hom f) x

Alias of AlgebraicGeometry.Spec.map_apply.

theorem AlgebraicGeometry.Spec.map_app {R S : CommRingCat} (f : R ⟶ S) (U : (Spec R).Opens) : Scheme.Hom.app (map f) U = CommRingCat.ofHom (StructureSheaf.comap (CommRingCat.Hom.hom f) U ((TopologicalSpace.Opens.map (map f).base).obj U) ⋯)

theorem AlgebraicGeometry.Spec.map_appLE {R S : CommRingCat} (f : R ⟶ S) {U : (Spec S).Opens} {V : (Spec R).Opens} (e : U ≤ (TopologicalSpace.Opens.map (map f).base).obj V) : Scheme.Hom.appLE (map f) V U e = CommRingCat.ofHom (StructureSheaf.comap (CommRingCat.Hom.hom f) V U e)

instance AlgebraicGeometry.instNonemptyCarrierCarrierCommRingCatSpecOfNontrivialCarrier {A : CommRingCat} [Nontrivial ↑A] : Nonempty ↥(Spec A)

theorem AlgebraicGeometry.Scheme.isEmpty_of_commSq {W X Y S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {i : W ⟶ X} {j : W ⟶ Y} (h : CategoryTheory.CommSq i j f g) (H : Disjoint (Set.range ⇑f) (Set.range ⇑g)) : IsEmpty ↥W

def AlgebraicGeometry.Scheme.empty : Scheme

The empty scheme.

@[simp]

theorem AlgebraicGeometry.Scheme.empty_carrier_carrier : ↥empty = PEmpty.{u_1 + 1}

@[simp]

theorem AlgebraicGeometry.Scheme.empty_presheaf : empty.presheaf = (CategoryTheory.Functor.const (TopologicalSpace.Opens ↑{ carrier := PEmpty.{u_1 + 1}, str := instTopologicalSpacePEmpty })ᵒᵖ).obj { carrier := PUnit.{u_1 + 1}, commRing := PUnit.commRing }

instance AlgebraicGeometry.Scheme.instEmptyCollection : EmptyCollection Scheme

def AlgebraicGeometry.Scheme.Γ : CategoryTheory.Functor Schemeᵒᵖ CommRingCat

The global sections as a functor. For the global section themselves, use Γ(X, ⊤) instead.

theorem AlgebraicGeometry.Scheme.Γ_def : Γ = forgetToLocallyRingedSpace.op.comp LocallyRingedSpace.Γ

@[simp]

theorem AlgebraicGeometry.Scheme.Γ_obj (X : Schemeᵒᵖ) : Γ.obj X = (Opposite.unop X).presheaf.obj (Opposite.op ⊤)

theorem AlgebraicGeometry.Scheme.Γ_obj_op (X : Scheme) : Γ.obj (Opposite.op X) = X.presheaf.obj (Opposite.op ⊤)

@[simp]

theorem AlgebraicGeometry.Scheme.Γ_map {X Y : Schemeᵒᵖ} (f : X ⟶ Y) : Γ.map f = Hom.appTop f.unop

theorem AlgebraicGeometry.Scheme.Γ_map_op {X Y : Scheme} (f : X ⟶ Y) : Γ.map f.op = Hom.appTop f

def AlgebraicGeometry.Scheme.SpecΓIdentity : Scheme.Spec.rightOp.comp Γ ≅ CategoryTheory.Functor.id CommRingCat

The counit (SpecΓIdentity.inv.op) of the adjunction Γ ⊣ Spec as a natural isomorphism. This is almost never needed in practical use cases. Use ΓSpecIso instead.

def AlgebraicGeometry.Scheme.ΓSpecIso (R : CommRingCat) : (Spec R).presheaf.obj (Opposite.op ⊤) ≅ R

The global sections of Spec R is isomorphic to R.

@[simp]

theorem AlgebraicGeometry.Scheme.SpecΓIdentity_app (R : CommRingCat) : SpecΓIdentity.app R = ΓSpecIso R

@[simp]

theorem AlgebraicGeometry.Scheme.SpecΓIdentity_hom_app (R : CommRingCat) : SpecΓIdentity.hom.app R = (ΓSpecIso R).hom

@[simp]

theorem AlgebraicGeometry.Scheme.SpecΓIdentity_inv_app (R : CommRingCat) : SpecΓIdentity.inv.app R = (ΓSpecIso R).inv

@[simp]

theorem AlgebraicGeometry.Scheme.ΓSpecIso_naturality {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.CategoryStruct.comp (Hom.appTop (Spec.map f)) (ΓSpecIso S).hom = CategoryTheory.CategoryStruct.comp (ΓSpecIso R).hom f

@[simp]

theorem AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc {R S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat} (h : S ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.appTop (Spec.map f)) (CategoryTheory.CategoryStruct.comp (ΓSpecIso S).hom h) = CategoryTheory.CategoryStruct.comp (ΓSpecIso R).hom (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.CategoryStruct.comp f (ΓSpecIso S).inv = CategoryTheory.CategoryStruct.comp (ΓSpecIso R).inv (Hom.appTop (Spec.map f))

@[simp]

theorem AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc {R S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat} (h : (Spec S).presheaf.obj (Opposite.op ⊤) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (ΓSpecIso S).inv h) = CategoryTheory.CategoryStruct.comp (ΓSpecIso R).inv (CategoryTheory.CategoryStruct.comp (Hom.appTop (Spec.map f)) h)

theorem AlgebraicGeometry.Scheme.ΓSpecIso_inv (R : CommRingCat) : (ΓSpecIso R).inv = CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).val.obj (Opposite.op ⊤)))

theorem AlgebraicGeometry.Scheme.toOpen_eq (R : CommRingCat) (U : TopologicalSpace.Opens ↑(PrimeSpectrum.Top ↑R)) : CommRingCat.ofHom (algebraMap ↑R ↑((Spec.structureSheaf ↑R).presheaf.obj (Opposite.op U))) = CategoryTheory.CategoryStruct.comp (ΓSpecIso R).inv ((Spec R).presheaf.map (CategoryTheory.homOfLE ⋯).op)

instance AlgebraicGeometry.Scheme.instUniqueCarrierCarrierCommRingCatSpecOf {K : Type u_1} [Field K] : Unique ↥(Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })

@[simp]

theorem AlgebraicGeometry.Scheme.default_asIdeal {K : Type u_1} [Field K] : default.asIdeal = ⊥

def AlgebraicGeometry.Scheme.basicOpen (X : Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) : X.Opens

The subset of the underlying space where the given section does not vanish.

theorem AlgebraicGeometry.Scheme.mem_basicOpen (X : Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥X) (hx : x ∈ U) : x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)

@[simp]

theorem AlgebraicGeometry.Scheme.mem_basicOpen' (X : Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥U) : ↑x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f)

A variant of mem_basicOpen for bundled x : U.

theorem AlgebraicGeometry.Scheme.mem_basicOpen'' (X : Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥X) : x ∈ X.basicOpen f ↔ ∃ (m : x ∈ U), IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x m)) f)

A variant of mem_basicOpen without the x ∈ U assumption.

theorem AlgebraicGeometry.Scheme.mem_basicOpen_top (X : Scheme) (f : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : ↥X) : x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ⊤ x trivial)) f)

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_res (X : Scheme) {V U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) (i : Opposite.op U ⟶ Opposite.op V) : X.basicOpen ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i)) f) = V ⊓ X.basicOpen f

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_res_eq (X : Scheme) {V U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) (i : Opposite.op U ⟶ Opposite.op V) [CategoryTheory.IsIso i] : X.basicOpen ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map i)) f) = X.basicOpen f

theorem AlgebraicGeometry.Scheme.basicOpen_le (X : Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) : X.basicOpen f ≤ U

theorem AlgebraicGeometry.Scheme.basicOpen_restrict (X : Scheme) {V U : X.Opens} (i : V ⟶ U) (f : ↑(X.presheaf.obj (Opposite.op U))) : X.basicOpen (TopCat.Presheaf.restrict f i) ≤ X.basicOpen f

@[simp]

theorem AlgebraicGeometry.Scheme.preimage_basicOpen {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} (r : ↑(Y.presheaf.obj (Opposite.op U))) : (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r) = X.basicOpen ((CategoryTheory.ConcreteCategory.hom (Hom.app f U)) r)

theorem AlgebraicGeometry.Scheme.Hom.preimage_basicOpen {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} (r : ↑(Y.presheaf.obj (Opposite.op U))) : (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r) = X.basicOpen ((CategoryTheory.ConcreteCategory.hom (app f U)) r)

Alias of AlgebraicGeometry.Scheme.preimage_basicOpen.

theorem AlgebraicGeometry.Scheme.preimage_basicOpen_top {X Y : Scheme} (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r) = X.basicOpen ((CategoryTheory.ConcreteCategory.hom (Hom.appTop f)) r)

theorem AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_top {X Y : Scheme} (f : X ⟶ Y) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen r) = X.basicOpen ((CategoryTheory.ConcreteCategory.hom (appTop f)) r)

Alias of AlgebraicGeometry.Scheme.preimage_basicOpen_top.

theorem AlgebraicGeometry.Scheme.basicOpen_appLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) (s : ↑(Y.presheaf.obj (Opposite.op V))) : X.basicOpen ((CategoryTheory.ConcreteCategory.hom (Hom.appLE f V U e)) s) = U ⊓ (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen s)

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_zero (X : Scheme) (U : X.Opens) : X.basicOpen 0 = ⊥

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_mul (X : Scheme) {U : X.Opens} (f g : ↑(X.presheaf.obj (Opposite.op U))) : X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g

theorem AlgebraicGeometry.Scheme.basicOpen_pow (X : Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) {n : ℕ} (h : 0 < n) : X.basicOpen (f ^ n) = X.basicOpen f

theorem AlgebraicGeometry.Scheme.basicOpen_add_le (X : Scheme) {U : X.Opens} (f g : ↑(X.presheaf.obj (Opposite.op U))) : X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g

theorem AlgebraicGeometry.Scheme.basicOpen_of_isUnit (X : Scheme) {U : X.Opens} {f : ↑(X.presheaf.obj (Opposite.op U))} (hf : IsUnit f) : X.basicOpen f = U

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_one (X : Scheme) {U : X.Opens} : X.basicOpen 1 = U

instance AlgebraicGeometry.Scheme.algebra_section_section_basicOpen {X : Scheme} {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) : Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))

@[simp]

theorem AlgebraicGeometry.SpecMap_preimage_basicOpen {R S : CommRingCat} (f : R ⟶ S) (r : ↑R) : (TopologicalSpace.Opens.map (Spec.map f).base).obj (PrimeSpectrum.basicOpen r) = PrimeSpectrum.basicOpen ((CategoryTheory.ConcreteCategory.hom f) r)

def AlgebraicGeometry.Scheme.zeroLocus (X : Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))) : Set ↥X

The zero locus of a set of sections s over an open set U is the closed set consisting of the complement of U and of all points of U, where all elements of f vanish.

theorem AlgebraicGeometry.Scheme.zeroLocus_def (X : Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus s = ⋂ f ∈ s, (X.basicOpen f).carrierᶜ

theorem AlgebraicGeometry.Scheme.zeroLocus_isClosed (X : Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))) : IsClosed (X.zeroLocus s)

theorem AlgebraicGeometry.Scheme.zeroLocus_singleton (X : Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus {f} = (↑(X.basicOpen f))ᶜ

@[simp]

theorem AlgebraicGeometry.Scheme.zeroLocus_empty_eq_univ (X : Scheme) {U : X.Opens} : X.zeroLocus ∅ = Set.univ

@[simp]

theorem AlgebraicGeometry.Scheme.mem_zeroLocus_iff (X : Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))) (x : ↥X) : x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f

theorem AlgebraicGeometry.Scheme.codisjoint_zeroLocus (X : Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))) : Codisjoint (X.zeroLocus s) ↑U

theorem AlgebraicGeometry.Scheme.zeroLocus_span (X : Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus ↑(Ideal.span s) = X.zeroLocus s

theorem AlgebraicGeometry.Scheme.zeroLocus_setMul (X : Scheme) {U : X.Opens} (s t : Set ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus (s * t) = X.zeroLocus s ∪ X.zeroLocus t

theorem AlgebraicGeometry.Scheme.zeroLocus_mul (X : Scheme) {U : X.Opens} (I J : Ideal ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus ↑(I * J) = X.zeroLocus ↑I ∪ X.zeroLocus ↑J

theorem AlgebraicGeometry.Scheme.zeroLocus_map (X : Scheme) {U V : X.Opens} (i : U ≤ V) (s : Set ↑(X.presheaf.obj (Opposite.op V))) : X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE i).op)) '' s) = X.zeroLocus s ∪ (↑U)ᶜ

theorem AlgebraicGeometry.Scheme.zeroLocus_map_of_eq (X : Scheme) {U V : X.Opens} (i : U = V) (s : Set ↑(X.presheaf.obj (Opposite.op V))) : X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.eqToHom i).op)) '' s) = X.zeroLocus s

theorem AlgebraicGeometry.Scheme.zeroLocus_mono (X : Scheme) {U : X.Opens} {s t : Set ↑(X.presheaf.obj (Opposite.op U))} (h : s ⊆ t) : X.zeroLocus t ⊆ X.zeroLocus s

theorem AlgebraicGeometry.Scheme.preimage_zeroLocus {X Y : Scheme} (f : X ⟶ Y) {U : Y.Opens} (s : Set ↑(Y.presheaf.obj (Opposite.op U))) : ⇑f ⁻¹' Y.zeroLocus s = X.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.app f U)) '' s)

@[simp]

theorem AlgebraicGeometry.Scheme.zeroLocus_univ (X : Scheme) {U : X.Opens} : X.zeroLocus Set.univ = (↑U)ᶜ

theorem AlgebraicGeometry.Scheme.zeroLocus_iUnion (X : Scheme) {U : X.Opens} {ι : Type u_1} (f : ι → Set ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus (⋃ (i : ι), f i) = ⋂ (i : ι), X.zeroLocus (f i)

theorem AlgebraicGeometry.Scheme.zeroLocus_radical (X : Scheme) {U : X.Opens} (I : Ideal ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus ↑I.radical = X.zeroLocus ↑I

theorem AlgebraicGeometry.basicOpen_eq_of_affine {R : CommRingCat} (f : ↑R) : (Spec R).basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f) = PrimeSpectrum.basicOpen f

@[simp]

theorem AlgebraicGeometry.basicOpen_eq_of_affine' {R : CommRingCat} (f : ↑((Spec R).presheaf.obj (Opposite.op ⊤))) : (Spec R).basicOpen f = PrimeSpectrum.basicOpen ((CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) f)

theorem AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom {X : Scheme} {U V : X.Opens} (h : U = V) (W : (Spec (X.presheaf.obj (Opposite.op V))).Opens) : Hom.app (Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op)) W = CategoryTheory.eqToHom ⋯

@[deprecated AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.Spec_map_presheaf_map_eqToHom {X : Scheme} {U V : X.Opens} (h : U = V) (W : (Spec (X.presheaf.obj (Opposite.op V))).Opens) : Hom.app (Spec.map (X.presheaf.map (CategoryTheory.eqToHom h).op)) W = CategoryTheory.eqToHom ⋯

Alias of AlgebraicGeometry.Scheme.SpecMap_presheaf_map_eqToHom.

theorem AlgebraicGeometry.germ_eq_zero_of_pow_mul_eq_zero {X : Scheme} {U : TopologicalSpace.Opens ↥X} (x : ↥U) {f s : ↑(X.presheaf.obj (Opposite.op U))} (hx : ↑x ∈ X.basicOpen s) {n : ℕ} (hf : s ^ n * f = 0) : (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

@[simp]

theorem AlgebraicGeometry.Scheme.hom_base_inv_base {X Y : Scheme} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.hom.base e.inv.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.Scheme.hom_base_inv_base_assoc {X Y : Scheme} (e : X ≅ Y) {Z : TopCat} (h : ↑X.toPresheafedSpace ⟶ Z) : CategoryTheory.CategoryStruct.comp e.hom.base (CategoryTheory.CategoryStruct.comp e.inv.base h) = h

@[deprecated AlgebraicGeometry.Scheme.hom_base_inv_base (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.iso_hom_base_inv_base {X Y : Scheme} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.hom.base e.inv.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace

Alias of AlgebraicGeometry.Scheme.hom_base_inv_base.

@[simp]

theorem AlgebraicGeometry.Scheme.hom_inv_apply {X Y : Scheme} (e : X ≅ Y) (x : ↥X) : e.inv (e.hom x) = x

@[deprecated AlgebraicGeometry.Scheme.hom_inv_apply (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.iso_hom_base_inv_base_apply {X Y : Scheme} (e : X ≅ Y) (x : ↥X) : e.inv (e.hom x) = x

Alias of AlgebraicGeometry.Scheme.hom_inv_apply.

@[simp]

theorem AlgebraicGeometry.Scheme.inv_base_hom_base {X Y : Scheme} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.inv.base e.hom.base = CategoryTheory.CategoryStruct.id ↑Y.toPresheafedSpace

@[simp]

theorem AlgebraicGeometry.Scheme.inv_base_hom_base_assoc {X Y : Scheme} (e : X ≅ Y) {Z : TopCat} (h : ↑Y.toPresheafedSpace ⟶ Z) : CategoryTheory.CategoryStruct.comp e.inv.base (CategoryTheory.CategoryStruct.comp e.hom.base h) = h

@[deprecated AlgebraicGeometry.Scheme.inv_base_hom_base (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.iso_inv_base_hom_base {X Y : Scheme} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.inv.base e.hom.base = CategoryTheory.CategoryStruct.id ↑Y.toPresheafedSpace

Alias of AlgebraicGeometry.Scheme.inv_base_hom_base.

@[simp]

theorem AlgebraicGeometry.Scheme.inv_hom_apply {X Y : Scheme} (e : X ≅ Y) (y : ↥Y) : e.hom (e.inv y) = y

@[deprecated AlgebraicGeometry.Scheme.inv_hom_apply (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.iso_inv_base_hom_base_apply {X Y : Scheme} (e : X ≅ Y) (y : ↥Y) : e.hom (e.inv y) = y

Alias of AlgebraicGeometry.Scheme.inv_hom_apply.

theorem AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus {R : CommRingCat} (s : Set ↑R) : (Spec R).zeroLocus (⇑(CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) = PrimeSpectrum.zeroLocus s

theorem AlgebraicGeometry.Spec_zeroLocus {R : CommRingCat} (s : Set ↑((Spec R).presheaf.obj (Opposite.op ⊤))) : (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(CategoryTheory.ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)

instance AlgebraicGeometry.Scheme.Hom.instIsLocalHomCarrierStalkCommRingCatPresheafCoeContinuousMapCarrierCarrierHomTopCatBaseRingHomHomStalkMap {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : IsLocalHom (CommRingCat.Hom.hom (stalkMap f x))

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_id (X : Scheme) (x : ↥X) : stalkMap (CategoryTheory.CategoryStruct.id X) x = CategoryTheory.CategoryStruct.id (X.presheaf.stalk x)

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X) : stalkMap (CategoryTheory.CategoryStruct.comp f g) x = CategoryTheory.CategoryStruct.comp (stalkMap g (f x)) (stalkMap f x)

theorem AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (stalkMap f x) = CategoryTheory.CategoryStruct.comp (stalkMap f x') (X.presheaf.stalkSpecializes h)

theorem AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') {Z : CommRingCat} (h✝ : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (stalkMap f x) h✝) = CategoryTheory.CategoryStruct.comp (stalkMap f x') (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h✝)

theorem AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') (y : ↑(Y.presheaf.stalk ((TopCat.Hom.hom f.base) x'))) : (CategoryTheory.ConcreteCategory.hom (stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (stalkMap f x')) y)

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_congr {X Y : Scheme} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↥X) (hxx' : x = x') : CategoryTheory.CategoryStruct.comp (stalkMap f x) (X.presheaf.stalkCongr ⋯).hom = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (stalkMap g x')

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc {X Y : Scheme} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↥X) (hxx' : x = x') {Z : CommRingCat} (h : X.presheaf.stalk x' ⟶ Z) : CategoryTheory.CategoryStruct.comp (stalkMap f x) (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (CategoryTheory.CategoryStruct.comp (stalkMap g x') h)

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom {X Y : Scheme} (f g : X ⟶ Y) (hfg : f = g) (x : ↥X) : stalkMap f x = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (stalkMap g x)

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc {X Y : Scheme} (f g : X ⟶ Y) (hfg : f = g) (x : ↥X) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (stalkMap f x) h = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (CategoryTheory.CategoryStruct.comp (stalkMap g x) h)

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (hxx' : x = x') : CategoryTheory.CategoryStruct.comp (stalkMap f x) (X.presheaf.stalkCongr ⋯).hom = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (stalkMap f x')

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (hxx' : x = x') {Z : CommRingCat} (h : X.presheaf.stalk x' ⟶ Z) : CategoryTheory.CategoryStruct.comp (stalkMap f x) (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (CategoryTheory.CategoryStruct.comp (stalkMap f x') h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv {X Y : Scheme} (e : X ≅ Y) (y : ↥Y) : CategoryTheory.CategoryStruct.comp (stalkMap e.hom (e.inv y)) (stalkMap e.inv y) = (Y.presheaf.stalkCongr ⋯).hom

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc {X Y : Scheme} (e : X ≅ Y) (y : ↥Y) {Z : CommRingCat} (h : Y.presheaf.stalk y ⟶ Z) : CategoryTheory.CategoryStruct.comp (stalkMap e.hom (e.inv y)) (CategoryTheory.CategoryStruct.comp (stalkMap e.inv y) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply {X Y : Scheme} (e : X ≅ Y) (y : ↥Y) (z : ↑(Y.presheaf.stalk (e.hom (e.inv y)))) : (CategoryTheory.ConcreteCategory.hom (stalkMap e.inv y)) ((CategoryTheory.ConcreteCategory.hom (stalkMap e.hom (e.inv y))) z) = (CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkCongr ⋯).hom) z

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom {X Y : Scheme} (e : X ≅ Y) (x : ↥X) : CategoryTheory.CategoryStruct.comp (stalkMap e.inv (e.hom x)) (stalkMap e.hom x) = (X.presheaf.stalkCongr ⋯).hom

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc {X Y : Scheme} (e : X ≅ Y) (x : ↥X) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (stalkMap e.inv (e.hom x)) (CategoryTheory.CategoryStruct.comp (stalkMap e.hom x) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply {X Y : Scheme} (e : X ≅ Y) (x : ↥X) (y : ↑(X.presheaf.stalk (e.inv (e.hom x)))) : (CategoryTheory.ConcreteCategory.hom (stalkMap e.hom x)) ((CategoryTheory.ConcreteCategory.hom (stalkMap e.inv (e.hom x))) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkCongr ⋯).hom) y

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.germ_stalkMap {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U (f x) hx) (stalkMap f x) = CategoryTheory.CategoryStruct.comp (app f U) (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U (f x) hx) (CategoryTheory.CategoryStruct.comp (stalkMap f x) h) = CategoryTheory.CategoryStruct.comp (app f U) (CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U) (y : ↑(Y.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx)) ((CategoryTheory.ConcreteCategory.hom (app f U)) y)

noncomputable def AlgebraicGeometry.Scheme.Hom.arrowStalkMapIsoOfEq {X Y : Scheme} (f : X ⟶ Y) {x y : ↥X} (h : x = y) : CategoryTheory.Arrow.mk (stalkMap f x) ≅ CategoryTheory.Arrow.mk (stalkMap f y)

If x = y, the stalk maps are isomorphic.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_id (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_id (X : Scheme) (x : ↥X) : Hom.stalkMap (CategoryTheory.CategoryStruct.id X) x = CategoryTheory.CategoryStruct.id (X.presheaf.stalk x)

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_id.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_comp (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↥X) : Hom.stalkMap (CategoryTheory.CategoryStruct.comp f g) x = CategoryTheory.CategoryStruct.comp (Hom.stalkMap g (f x)) (Hom.stalkMap f x)

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_comp.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (Hom.stalkMap f x) = CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x') (X.presheaf.stalkSpecializes h)

Alias of AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_assoc {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') {Z : CommRingCat} (h✝ : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) h✝) = CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x') (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h✝)

Alias of AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (h : x ⤳ x') (y : ↑(Y.presheaf.stalk ((TopCat.Hom.hom f.base) x'))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes h)) ((CategoryTheory.ConcreteCategory.hom (Hom.stalkMap f x')) y)

Alias of AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap_apply.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_congr (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_congr {X Y : Scheme} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↥X) (hxx' : x = x') : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) (X.presheaf.stalkCongr ⋯).hom = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (Hom.stalkMap g x')

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_congr.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_congr_assoc {X Y : Scheme} (f g : X ⟶ Y) (hfg : f = g) (x x' : ↥X) (hxx' : x = x') {Z : CommRingCat} (h : X.presheaf.stalk x' ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (CategoryTheory.CategoryStruct.comp (Hom.stalkMap g x') h)

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_congr_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_congr_hom {X Y : Scheme} (f g : X ⟶ Y) (hfg : f = g) (x : ↥X) : Hom.stalkMap f x = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (Hom.stalkMap g x)

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_congr_hom_assoc {X Y : Scheme} (f g : X ⟶ Y) (hfg : f = g) (x : ↥X) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) h = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (CategoryTheory.CategoryStruct.comp (Hom.stalkMap g x) h)

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_congr_hom_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_congr_point {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (hxx' : x = x') : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) (X.presheaf.stalkCongr ⋯).hom = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (Hom.stalkMap f x')

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_congr_point_assoc {X Y : Scheme} (f : X ⟶ Y) (x x' : ↥X) (hxx' : x = x') {Z : CommRingCat} (h : X.presheaf.stalk x' ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom (CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x') h)

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_congr_point_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_hom_inv {X Y : Scheme} (e : X ≅ Y) (y : ↥Y) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.hom (e.inv y)) (Hom.stalkMap e.inv y) = (Y.presheaf.stalkCongr ⋯).hom

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_hom_inv_assoc {X Y : Scheme} (e : X ≅ Y) (y : ↥Y) {Z : CommRingCat} (h : Y.presheaf.stalk y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.hom (e.inv y)) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.inv y) h) = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkCongr ⋯).hom h

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply {X Y : Scheme} (e : X ≅ Y) (y : ↥Y) (z : ↑(Y.presheaf.stalk (e.hom (e.inv y)))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap e.inv y)) ((CategoryTheory.ConcreteCategory.hom (Hom.stalkMap e.hom (e.inv y))) z) = (CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkCongr ⋯).hom) z

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv_apply.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_inv_hom {X Y : Scheme} (e : X ≅ Y) (x : ↥X) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.inv (e.hom x)) (Hom.stalkMap e.hom x) = (X.presheaf.stalkCongr ⋯).hom

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_inv_hom_assoc {X Y : Scheme} (e : X ≅ Y) (x : ↥X) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.inv (e.hom x)) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap e.hom x) h) = CategoryTheory.CategoryStruct.comp (X.presheaf.stalkCongr ⋯).hom h

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply {X Y : Scheme} (e : X ≅ Y) (x : ↥X) (y : ↑(X.presheaf.stalk (e.inv (e.hom x)))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap e.hom x)) ((CategoryTheory.ConcreteCategory.hom (Hom.stalkMap e.inv (e.hom x))) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkCongr ⋯).hom) y

Alias of AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom_apply.

@[deprecated AlgebraicGeometry.Scheme.Hom.germ_stalkMap (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_germ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U (f x) hx) (Hom.stalkMap f x) = CategoryTheory.CategoryStruct.comp (Hom.app f U) (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx)

Alias of AlgebraicGeometry.Scheme.Hom.germ_stalkMap.

@[deprecated AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_germ_assoc {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U (f x) hx) (CategoryTheory.CategoryStruct.comp (Hom.stalkMap f x) h) = CategoryTheory.CategoryStruct.comp (Hom.app f U) (CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx) h)

Alias of AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc.

@[deprecated AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply (since := "2025-10-07")]

theorem AlgebraicGeometry.Scheme.stalkMap_germ_apply {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens) (x : ↥X) (hx : f x ∈ U) (y : ↑(Y.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (Hom.stalkMap f x)) ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.germ U (f x) hx)) y) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx)) ((CategoryTheory.ConcreteCategory.hom (Hom.app f U)) y)

Alias of AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply.

@[deprecated AlgebraicGeometry.Scheme.Hom.arrowStalkMapIsoOfEq (since := "2025-10-07")]

def AlgebraicGeometry.Scheme.arrowStalkMapIsoOfEq {X Y : Scheme} (f : X ⟶ Y) {x y : ↥X} (h : x = y) : CategoryTheory.Arrow.mk (Hom.stalkMap f x) ≅ CategoryTheory.Arrow.mk (Hom.stalkMap f y)

Alias of AlgebraicGeometry.Scheme.Hom.arrowStalkMapIsoOfEq.

---

If x = y, the stalk maps are isomorphic.

@[simp]

theorem AlgebraicGeometry.Spec_closedPoint {R S : CommRingCat} [IsLocalRing ↑R] [IsLocalRing ↑S] {f : R ⟶ S} [IsLocalHom (CommRingCat.Hom.hom f)] : (Spec.map f) (IsLocalRing.closedPoint ↑S) = IsLocalRing.closedPoint ↑R