Typeclasses for S-schemes and S-morphisms

We define these as thin wrappers around CategoryTheory/Comma/OverClass.

Main definition

• AlgebraicGeometry.Scheme.Over: X.Over S equips X with a S-scheme structure. X ↘ S : X ⟶ S is the structure morphism.
• AlgebraicGeometry.Scheme.Hom.IsOver: f.IsOver S asserts that f is a S-morphism.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Over (X S : Scheme) : Type u

X.Over S is the typeclass containing the data of a structure morphism X ↘ S : X ⟶ S.

Equations

• X.Over S = CategoryTheory.OverClass X S

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.CanonicallyOver (X S : Scheme) : Type u

X.CanonicallyOver S is the typeclass containing the data of a structure morphism X ↘ S : X ⟶ S, and that S is (uniquely) inferable from the structure of X.

Equations

• X.CanonicallyOver S = CategoryTheory.CanonicallyOverClass X S

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Hom.IsOver {X Y : Scheme} (f : X.Hom Y) (S : Scheme) [X.Over S] [Y.Over S] : Prop

Given X.Over S and Y.Over S and f : X ⟶ Y, f.IsOver S is the typeclass asserting f commutes with the structure morphisms.

Equations

• f.IsOver S = CategoryTheory.HomIsOver f S

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.isOver_iff {X Y : Scheme} (S : Scheme) [X.Over S] [Y.Over S] {f : X ⟶ Y} : IsOver f S ↔ CategoryTheory.CategoryStruct.comp f (Y ↘ S) = X ↘ S

Also note the existence of CategoryTheory.IsOverTower X Y S.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.asOver (X S : Scheme) [X.Over S] : CategoryTheory.Over S

Given X.Over S, this is the bundled object of Over S.

Equations

• X.asOver S = CategoryTheory.OverClass.asOver X S

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Hom.asOver {X Y : Scheme} (f : X.Hom Y) (S : Scheme) [X.Over S] [Y.Over S] [f.IsOver S] : CategoryTheory.OverClass.asOver X S ⟶ CategoryTheory.OverClass.asOver Y S

Given a morphism X ⟶ Y with f.IsOver S, this is the bundled morphism in Over S.

Equations

• f.asOver S = CategoryTheory.OverClass.asOverHom S f