noncomputable def AlgebraicGeometry.graphMorphism {S X Y : Scheme} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) (w : sX = CategoryTheory.CategoryStruct.comp f sY) : X ⟶ CategoryTheory.Limits.pullback sX sY

Graph morphism Γ_f : X → X ×_S Y of a morphism f : X → Y over S, defined by (𝟙 X, f) via the pullback universal property (Def 18, Lec 7).

@[simp]

theorem AlgebraicGeometry.graphMorphism_fst {S X Y : Scheme} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) (w : sX = CategoryTheory.CategoryStruct.comp f sY) : CategoryTheory.CategoryStruct.comp (graphMorphism f sX sY w) (CategoryTheory.Limits.pullback.fst sX sY) = CategoryTheory.CategoryStruct.id X

First projection of the graph morphism is the identity on X.

@[simp]

theorem AlgebraicGeometry.graphMorphism_snd {S X Y : Scheme} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) (w : sX = CategoryTheory.CategoryStruct.comp f sY) : CategoryTheory.CategoryStruct.comp (graphMorphism f sX sY w) (CategoryTheory.Limits.pullback.snd sX sY) = f

Second projection of the graph morphism is f.

instance AlgebraicGeometry.graphMorphism_isSplitMono {S X Y : Scheme} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) (w : sX = CategoryTheory.CategoryStruct.comp f sY) : CategoryTheory.IsSplitMono (graphMorphism f sX sY w)

The graph morphism is a split monomorphism, with pullback.fst as retraction.

instance AlgebraicGeometry.graphMorphism_mono {S X Y : Scheme} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) (w : sX = CategoryTheory.CategoryStruct.comp f sY) : CategoryTheory.Mono (graphMorphism f sX sY w)

As a split mono, the graph morphism is in particular a monomorphism.

theorem AlgebraicGeometry.graphMorphism_id {S X : Scheme} (sX : X ⟶ S) : graphMorphism (CategoryTheory.CategoryStruct.id X) sX sX ⋯ = CategoryTheory.Limits.pullback.diagonal sX

The graph of the identity morphism is the diagonal Δ_{X/S}.

instance AlgebraicGeometry.graphMorphism_isClosedImmersion {S X Y : Scheme} (f : X ⟶ Y) (sX : X ⟶ S) (sY : Y ⟶ S) (w : sX = CategoryTheory.CategoryStruct.comp f sY) [IsSeparated sY] : IsClosedImmersion (graphMorphism f sX sY w)

If the target Y → S is separated, the graph morphism is a closed immersion.