Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Hom.asOver

{X Y : AlgebraicGeometry.Scheme} →
  (f : X.Hom Y) →
    (S : AlgebraicGeometry.Scheme) →
      [inst : X.Over S] →
        [inst_1 : 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.

Defined in

Mathlib.AlgebraicGeometry.Over

Cited by

9 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.Scheme.OverAlgebraicGeometry.Scheme.OverAlgebraicGeometry.Scheme.Hom.IsOver