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.toPresheafedSpace), IsLocalRing ↑(self.presheaf.stalk x)
• local_affine : ∀ (x : ↑self.toTopCat), ∃ (U : TopologicalSpace.OpenNhds x) (R : CommRingCat), Nonempty (self.restrict ⋯ ≅ AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op R))

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

Equations

• AlgebraicGeometry.Scheme.instCoeSortType = { coe := fun (X : AlgebraicGeometry.Scheme) => ↑↑X.toPresheafedSpace }

@[reducible, inline]

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

The type of open sets of a scheme.

Equations

• X.Opens = TopologicalSpace.Opens ↑↑X.toPresheafedSpace

structure AlgebraicGeometry.Scheme.Hom (X Y : AlgebraicGeometry.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.toPresheafedSpace), IsLocalHom (self.stalkMap x)

@[reducible, inline]

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

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

Equations

• f.toLRSHom = f.toHom_1

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

See Note [custom simps projection]

Equations

• AlgebraicGeometry.Scheme.Hom.Simps.toLRSHom f = f.toLRSHom

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

Schemes are a full subcategory of locally ringed spaces.

Equations

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

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.

Equations

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

def AlgebraicGeometry.«term_⁻¹ᵁ_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def AlgebraicGeometry.«termΓ(_,_)».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

@[reducible, inline]

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

The structure sheaf of a scheme.

Equations

• X.sheaf = X.sheaf

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Hom.app {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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).

Equations

• f.app U = f.c.app (Opposite.op U)

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

theorem AlgebraicGeometry.Scheme.Hom.naturality_assoc {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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 (f.app U) h) = CategoryTheory.CategoryStruct.comp (f.app U') (CategoryTheory.CategoryStruct.comp (X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op) h)

def AlgebraicGeometry.Scheme.Hom.appLE {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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).

Equations

• f.appLE U V e = CategoryTheory.CategoryStruct.comp (f.app U) (X.presheaf.map (CategoryTheory.homOfLE e).op)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appLE_map {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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 (f.appLE U V e) (X.presheaf.map i) = f.appLE U V' ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.appLE_map_assoc {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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 (f.appLE U V e) (CategoryTheory.CategoryStruct.comp (X.presheaf.map i) h) = CategoryTheory.CategoryStruct.comp (f.appLE U V' ⋯) h

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

theorem AlgebraicGeometry.Scheme.Hom.appLE_map'_assoc {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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 (f.appLE U V' ⋯) (CategoryTheory.CategoryStruct.comp (X.presheaf.map (CategoryTheory.eqToHom i).op) h) = CategoryTheory.CategoryStruct.comp (f.appLE U V e) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.map_appLE {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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) (f.appLE U V e) = f.appLE U' V ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.map_appLE_assoc {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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 (f.appLE U V e) h) = CategoryTheory.CategoryStruct.comp (f.appLE U' V ⋯) h

theorem AlgebraicGeometry.Scheme.Hom.map_appLE' {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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) (f.appLE U' V ⋯) = f.appLE U V e

theorem AlgebraicGeometry.Scheme.Hom.map_appLE'_assoc {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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 (f.appLE U' V ⋯) h) = CategoryTheory.CategoryStruct.comp (f.appLE U V e) h

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

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

theorem AlgebraicGeometry.Scheme.Hom.appLE_congr {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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 : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) : P (f.appLE U V e) ↔ P (f.appLE U' V' ⋯)

def AlgebraicGeometry.Scheme.Hom.stalkMap {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (x : ↑↑X.toPresheafedSpace) : Y.presheaf.stalk (f.base 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.

Equations

• f.stalkMap x = AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f.toLRSHom x

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

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

An alternative ext lemma for scheme morphisms.

theorem AlgebraicGeometry.Scheme.Hom.preimage_iSup {X Y : AlgebraicGeometry.Scheme} (f : X.Hom 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.preimage_iSup_eq_top {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) {ι : Sort u_1} {U : ι → Y.Opens} (hU : iSup U = ⊤) : ⨆ (i : ι), (TopologicalSpace.Opens.map f.base).obj (U i) = ⊤

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

@[simp]

theorem AlgebraicGeometry.Scheme.preimage_comp {X Y Z : AlgebraicGeometry.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)

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

The forgetful functor from Scheme to LocallyRingedSpace.

Equations

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

@[simp]

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

@[simp]

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

def AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace : AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.FullyFaithful

The forget functor Scheme ⥤ LocallyRingedSpace is fully faithful.

Equations

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

@[simp]

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

instance AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace : AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.Full

Equations

• AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace = ⋯

instance AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace : AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.Faithful

Equations

• AlgebraicGeometry.Scheme.instFaithfulLocallyRingedSpaceForgetToLocallyRingedSpace = ⋯

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

The forgetful functor from Scheme to TopCat.

Equations

• AlgebraicGeometry.Scheme.forgetToTop = AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.comp AlgebraicGeometry.LocallyRingedSpace.forgetToTop

@[simp]

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

@[simp]

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

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

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

Equations

• AlgebraicGeometry.Scheme.homeoOfIso e = TopCat.homeoOfIso (AlgebraicGeometry.Scheme.forgetToTop.mapIso e)

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

Alias of AlgebraicGeometry.Scheme.homeoOfIso.

---

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

Equations

• @CategoryTheory.Iso.schemeIsoToHomeo = @AlgebraicGeometry.Scheme.homeoOfIso

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

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

Equations

• f.homeomorph = (CategoryTheory.asIso f).schemeIsoToHomeo

instance AlgebraicGeometry.Scheme.hasCoeToTopCat : CoeOut AlgebraicGeometry.Scheme TopCat

Equations

• AlgebraicGeometry.Scheme.hasCoeToTopCat = { coe := fun (X : AlgebraicGeometry.Scheme) => ↑X.toPresheafedSpace }

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

forgetful functor to TopCat is the same as coercion

Equations

• X.forgetToTop_obj_eq_coe = (AlgebraicGeometry.Scheme.forgetToTop.obj X = ↑X.toPresheafedSpace)

@[simp]

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

@[simp]

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

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

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

@[simp]

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

theorem AlgebraicGeometry.Scheme.comp_coeBase_assoc {X Y Z : AlgebraicGeometry.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.comp_base {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).base = CategoryTheory.CategoryStruct.comp f.base g.base

theorem AlgebraicGeometry.Scheme.comp_base_assoc {X Y Z : AlgebraicGeometry.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.comp_base_apply {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑↑X.toPresheafedSpace) : (CategoryTheory.CategoryStruct.comp f g).base x = g.base (f.base x)

@[simp]

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

theorem AlgebraicGeometry.Scheme.comp_app_assoc {X Y Z : AlgebraicGeometry.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 (AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.CategoryStruct.comp f g) U) h = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f ((TopologicalSpace.Opens.map g.base).obj U)) h)

@[deprecated AlgebraicGeometry.Scheme.comp_app]

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

Alias of AlgebraicGeometry.Scheme.comp_app.

@[deprecated AlgebraicGeometry.Scheme.comp_app_assoc]

theorem AlgebraicGeometry.Scheme.comp_val_c_app_assoc {X Y Z : AlgebraicGeometry.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 (AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.CategoryStruct.comp f g) U) h = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f ((TopologicalSpace.Opens.map g.base).obj U)) h)

Alias of AlgebraicGeometry.Scheme.comp_app_assoc.

theorem AlgebraicGeometry.Scheme.appLE_comp_appLE {X Y Z : AlgebraicGeometry.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 (AlgebraicGeometry.Scheme.Hom.appLE g U V e₁) (AlgebraicGeometry.Scheme.Hom.appLE f V W e₂) = AlgebraicGeometry.Scheme.Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U W ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.comp_appLE {X Y Z : AlgebraicGeometry.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) : AlgebraicGeometry.Scheme.Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U V e = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U) (AlgebraicGeometry.Scheme.Hom.appLE f ((TopologicalSpace.Opens.map g.base).obj U) V e)

theorem AlgebraicGeometry.Scheme.comp_appLE_assoc {X Y Z : AlgebraicGeometry.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 (AlgebraicGeometry.Scheme.Hom.appLE (CategoryTheory.CategoryStruct.comp f g) U V e) h = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f ((TopologicalSpace.Opens.map g.base).obj U) V e) h)

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

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

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

theorem AlgebraicGeometry.Scheme.presheaf_map_eqToHom_op (X : AlgebraicGeometry.Scheme) (U V : X.Opens) (i : U = V) : X.presheaf.map (CategoryTheory.eqToHom i).op = CategoryTheory.eqToHom ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.Scheme.instIsIsoCommRingCatAppOppositeOpensαTopologicalSpaceCarrierC {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)ᵒᵖ) : CategoryTheory.IsIso (f.c.app U)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

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

def AlgebraicGeometry.Spec (R : CommRingCat) : AlgebraicGeometry.Scheme

The spectrum of a commutative ring, as a scheme.

Equations

• AlgebraicGeometry.Spec R = { toLocallyRingedSpace := AlgebraicGeometry.Spec.locallyRingedSpaceObj R, local_affine := ⋯ }

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

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

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

Equations

• AlgebraicGeometry.Spec.map f = { toHom_1 := AlgebraicGeometry.Spec.locallyRingedSpaceMap f }

@[simp]

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

@[simp]

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

@[simp]

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

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

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

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

theorem AlgebraicGeometry.Spec.map_base {R S : CommRingCat} (f : R ⟶ S) : (AlgebraicGeometry.Spec.map f).base = PrimeSpectrum.comap f

theorem AlgebraicGeometry.Spec.map_base_apply {R S : CommRingCat} (f : R ⟶ S) (x : ↑↑(AlgebraicGeometry.Spec S).toPresheafedSpace) : (AlgebraicGeometry.Spec.map f).base x = (PrimeSpectrum.comap f) x

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

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

instance AlgebraicGeometry.instNonemptyαTopologicalSpaceCarrierCommRingCatSpecOfNontrivialCommRing {A : CommRingCat} [Nontrivial ↑A] : Nonempty ↑↑(AlgebraicGeometry.Spec A).toPresheafedSpace

Equations

• ⋯ = ⋯

def AlgebraicGeometry.Scheme.empty : AlgebraicGeometry.Scheme

The empty scheme.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.empty_carrier : ↑AlgebraicGeometry.Scheme.empty.toPresheafedSpace = TopCat.of PEmpty.{u_1 + 1}

@[simp]

theorem AlgebraicGeometry.Scheme.empty_presheaf : AlgebraicGeometry.Scheme.empty.presheaf = (CategoryTheory.Functor.const (TopologicalSpace.Opens ↑(TopCat.of PEmpty.{u_1 + 1} ))ᵒᵖ).obj (CommRingCat.of PUnit.{u_1 + 1} )

instance AlgebraicGeometry.Scheme.instEmptyCollection : EmptyCollection AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.Scheme.instEmptyCollection = { emptyCollection := AlgebraicGeometry.Scheme.empty }

instance AlgebraicGeometry.Scheme.instInhabited : Inhabited AlgebraicGeometry.Scheme

Equations

• AlgebraicGeometry.Scheme.instInhabited = { default := ∅ }

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

The global sections, notated Gamma.

Equations

• AlgebraicGeometry.Scheme.Γ = AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.op.comp AlgebraicGeometry.LocallyRingedSpace.Γ

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

@[simp]

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

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

@[simp]

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

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

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

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

Equations

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

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

The global sections of Spec R is isomorphic to R.

Equations

• AlgebraicGeometry.Scheme.ΓSpecIso R = AlgebraicGeometry.Scheme.SpecΓIdentity.app R

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.ΓSpecIso_naturality {R S : CommRingCat} (f : R ⟶ S) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map f) ⊤) (AlgebraicGeometry.Scheme.ΓSpecIso S).hom = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Γ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 (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map f) ⊤) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso S).hom h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Γ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 (AlgebraicGeometry.Scheme.ΓSpecIso S).inv = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv (AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Spec.map f) ⊤)

@[simp]

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

theorem AlgebraicGeometry.Scheme.ΓSpecIso_inv (R : CommRingCat) : (AlgebraicGeometry.Scheme.ΓSpecIso R).inv = AlgebraicGeometry.StructureSheaf.toOpen ↑R ⊤

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

instance AlgebraicGeometry.Scheme.instUniqueαTopologicalSpaceCarrierCommRingCatSpecOf {K : Type u_1} [Field K] : Unique ↑↑(AlgebraicGeometry.Spec (CommRingCat.of K)).toPresheafedSpace

Equations

• AlgebraicGeometry.Scheme.instUniqueαTopologicalSpaceCarrierCommRingCatSpecOf = inferInstanceAs (Unique (PrimeSpectrum K))

@[simp]

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

def AlgebraicGeometry.Scheme.basicOpen (X : AlgebraicGeometry.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.

Equations

• X.basicOpen f = X.toRingedSpace.basicOpen f

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

@[simp]

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

A variant of mem_basicOpen for bundled x : U.

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

A variant of mem_basicOpen without the x ∈ U assumption.

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem AlgebraicGeometry.Scheme.basicOpen_restrict (X : AlgebraicGeometry.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 : AlgebraicGeometry.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 ((AlgebraicGeometry.Scheme.Hom.app f U) r)

theorem AlgebraicGeometry.Scheme.basicOpen_appLE {X Y : AlgebraicGeometry.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 ((AlgebraicGeometry.Scheme.Hom.appLE f V U e) s) = U ⊓ (TopologicalSpace.Opens.map f.base).obj (Y.basicOpen s)

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.basicOpen_mul (X : AlgebraicGeometry.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 : AlgebraicGeometry.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_of_isUnit (X : AlgebraicGeometry.Scheme) {U : X.Opens} {f : ↑(X.presheaf.obj (Opposite.op U))} (hf : IsUnit f) : X.basicOpen f = U

instance AlgebraicGeometry.Scheme.algebra_section_section_basicOpen {X : AlgebraicGeometry.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)))

Equations

• AlgebraicGeometry.Scheme.algebra_section_section_basicOpen f = RingHom.toAlgebra (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)

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

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.

Equations

• X.zeroLocus s = X.toRingedSpace.zeroLocus s

theorem AlgebraicGeometry.Scheme.zeroLocus_def (X : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))) : IsClosed (X.zeroLocus s)

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance AlgebraicGeometry.Scheme.instIsLocalHomαCommRingStalkCommRingCatPresheafCoeHomTopCatCarrierTopologicalSpaceBaseStalkMap {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↑↑X.toPresheafedSpace) : IsLocalHom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)

Equations

• ⋯ = ⋯

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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