Documentation

Mathlib.AlgebraicGeometry.Scheme

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.

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.

Pretty printer for coercing schemes to types.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

The type of open sets of a scheme.

Equations

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

@[reducible, inline]

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

Equations

Schemes are a full subcategory of locally ringed spaces.

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

Pretty printer defined by notation3 command.

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

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.

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

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

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

The structure sheaf of a scheme.

Equations
@[reducible, inline]

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

Equations
@[reducible, inline]

Given a morphism of schemes f : X ⟶ Y, this is the induced map Γ(Y, ⊤) ⟶ Γ(X, ⊤).

Equations

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
@[simp]
@[simp]
theorem AlgebraicGeometry.Scheme.Hom.appLE_congr {X Y : 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 : CommRingCat} → (R S) → Prop) :
P (f.appLE U V e) P (f.appLE U' V' )

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

The forgetful functor from Scheme to LocallyRingedSpace.

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

The forget functor Scheme ⥤ LocallyRingedSpace is fully faithful.

Equations
  • One or more equations did not get rendered due to their size.
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.

Equations

Alias of AlgebraicGeometry.Scheme.homeoOfIso.


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

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

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

Equations
@[deprecated AlgebraicGeometry.Scheme.inv_appTop (since := "2024-11-23")]

Alias of AlgebraicGeometry.Scheme.inv_appTop.

def AlgebraicGeometry.Scheme.Hom.copyBase {X Y : Scheme} (f : X.Hom Y) (g : XY) (h : (CategoryTheory.ConcreteCategory.hom f.base) = g) :
X Y

Copies a morphism with a different underlying map

Equations
theorem AlgebraicGeometry.Scheme.Hom.copyBase_eq {X Y : Scheme} (f : X.Hom Y) (g : XY) (h : (CategoryTheory.ConcreteCategory.hom f.base) = g) :
f.copyBase g h = f

The spectrum of a commutative ring, as a scheme.

Equations

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

Equations

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]

The empty scheme.

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

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.

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

Equations
@[simp]

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) :

A variant of mem_basicOpen without the x ∈ U assumption.

@[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 fX.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

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
theorem AlgebraicGeometry.Scheme.zeroLocus_def (X : Scheme) {U : X.Opens} (s : Set (X.presheaf.obj (Opposite.op U))) :
X.zeroLocus s = fs, (X.basicOpen f).carrier
@[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 fs, xX.basicOpen f
theorem AlgebraicGeometry.Scheme.zeroLocus_mono (X : Scheme) {U : X.Opens} {s t : Set (X.presheaf.obj (Opposite.op U))} (h : s t) :
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) :