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 : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.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) inferrable from the structure of X.

Equations

• AlgebraicGeometry.Scheme.CanonicallyOver S = CategoryTheory.CanonicallyOverClass X S

@[reducible, inline]

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

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