Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Hom.asOverProp

{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X Y : AlgebraicGeometry.Scheme} →
    (f : X.Hom Y) →
      (S : AlgebraicGeometry.Scheme) →
        [inst : X.Over S] →
          [inst_1 : Y.Over S] →
            [f.IsOver S] → {hX : P (X ↘ S)} → {hY : P (Y ↘ S)} → X.asOverProp S hX ⟶ Y.asOverProp S hY

Bundle an S-morphism of S-scheme with P into a morphism in P.Over ⊤ S.

Defined in

Mathlib.AlgebraicGeometry.Cover.Over

Cited by

7 results in Mathlib

Foundations

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

Assumes

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