Documentation

Mathlib.AlgebraicGeometry.Over

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

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

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

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

Instances For

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

Instances For