Closed immersions over a base

Mathlib's IsClosedImmersion.lift factors a scheme morphism through a closed immersion when the defining ideal vanishes on the source. The factor remains over the same base. This file packages that lift in Over S, for use with structure maps of group schemes. Sections over a base with at most one point are also closed immersions.

A closed immersion also preserves the height of every point for the specialization order (AlgebraicGeometry.Scheme.Hom.height_apply_eq_height): the closure of a point of the source is carried homeomorphically onto the closure of its image. So the dimension of the closure of a point can be computed in a closed subscheme or in the ambient scheme alike.

instance TauCeti.isClosedImmersion_section {S : AlgebraicGeometry.Scheme} {X : CategoryTheory.Over S} [Subsingleton ↥S] (x : CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S) ⟶ X) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left x)

A section over a base with at most one point is a closed immersion.

noncomputable def TauCeti.closedImmersionOverLift {S : AlgebraicGeometry.Scheme} {X Y Z : CategoryTheory.Over S} (i : X ⟶ Y) (f : Z ⟶ Y) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (h : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left f)) : Z ⟶ X

Factor a morphism over S through a closed immersion over S, when the defining ideal of the immersion vanishes on the morphism.

@[simp]

theorem TauCeti.closedImmersionOverLift_left {S : AlgebraicGeometry.Scheme} {X Y Z : CategoryTheory.Over S} (i : X ⟶ Y) (f : Z ⟶ Y) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (h : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left f)) : CategoryTheory.Over.Hom.left (closedImmersionOverLift i f h) = AlgebraicGeometry.IsClosedImmersion.lift (CategoryTheory.Over.Hom.left i) (CategoryTheory.Over.Hom.left f) h

The underlying scheme morphism of the lift is Mathlib's closed-immersion lift.

@[simp]

theorem TauCeti.closedImmersionOverLift_comp {S : AlgebraicGeometry.Scheme} {X Y Z : CategoryTheory.Over S} (i : X ⟶ Y) (f : Z ⟶ Y) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (h : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left f)) : CategoryTheory.CategoryStruct.comp (closedImmersionOverLift i f h) i = f

The lift factors the original morphism over the base.

@[simp]

theorem TauCeti.closedImmersionOverLift_comp_assoc {S : AlgebraicGeometry.Scheme} {X Y Z : CategoryTheory.Over S} (i : X ⟶ Y) (f : Z ⟶ Y) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left i)] (h : AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left i) ≤ AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.Over.Hom.left f)) {Z✝ : CategoryTheory.Over S} (h✝ : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (closedImmersionOverLift i f h) (CategoryTheory.CategoryStruct.comp i h✝) = CategoryTheory.CategoryStruct.comp f h✝

The lift factors the original morphism over the base.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.height_apply_eq_height {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (x : ↥X) : Order.height (f x) = Order.height x

A closed immersion preserves the height of points for the specialization order, that is, the dimension of the closure of a point: the specializations of f x all lie in the closed image of f, and f is an embedding.