@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.graphMor {X Y : Scheme} (f : X ⟶ Y) : X ⟶ X ⨯ Y

Graph morphism Γ_f : X → X × Y of f : X → Y, given by (𝟙 X, f) (Def 18, Lec 7 in the absolute case).

@[simp]

theorem AlgebraicGeometry.Scheme.graphMor_comp_fst {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (graphMor f) CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.id X

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

@[simp]

theorem AlgebraicGeometry.Scheme.graphMor_comp_snd {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (graphMor f) CategoryTheory.Limits.prod.snd = f

Second projection of the graph morphism is f.

theorem AlgebraicGeometry.Scheme.graphMor_of_id {X : Scheme} : graphMor (CategoryTheory.CategoryStruct.id X) = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)

The graph of the identity is the diagonal Δ_X = (𝟙, 𝟙).

theorem AlgebraicGeometry.Scheme.isPullback_graphMor {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.IsPullback f (graphMor f) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Y)) (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Y))

The graph morphism fits into a pullback square exhibiting Γ_f as the pullback of the diagonal Δ_Y along f × 𝟙_Y : X × Y → Y × Y.

instance AlgebraicGeometry.Scheme.isImmersion_graphMor {X Y : Scheme} (f : X ⟶ Y) : IsImmersion (graphMor f)

The graph morphism is always an immersion.

instance AlgebraicGeometry.Scheme.isClosedImmersion_graphMor {X Y : Scheme} (f : X ⟶ Y) [Y.IsSeparated] : IsClosedImmersion (graphMor f)

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