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
equipsX
with aS
-scheme structure.X ↘ S : X ⟶ S
is the structure morphism.AlgebraicGeometry.Scheme.Hom.IsOver
:f.IsOver S
asserts thatf
is aS
-morphism.
@[reducible, inline]
X.Over S
is the typeclass containing the data of a structure morphism X ↘ S : X ⟶ S
.
Equations
Instances For
@[reducible, inline]
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
.
Instances For
Also note the existence of CategoryTheory.IsOverTower X Y S
.