Documentation

Mathlib.AlgebraicGeometry.Over

Typeclasses for S-schemes and S-morphisms #

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

Main definition #

source
@[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
Instances For
    source
    @[reducible, inline]
    abbrev AlgebraicGeometry.Scheme.CanonicallyOver {X : Scheme} (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
    Instances For
      source
      @[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
      Instances For
        source
        @[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.

        source
        @[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
        Instances For
          source
          @[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
          Instances For