Scheme structures on locally closed images

A quasi-compact morphism with locally closed topological image factors through an immersion with exactly that image. The intermediate scheme is the scheme-theoretic image inside the coborder, the complement of closure (Set.range f) \ Set.range f. The first map is surjective and scheme-theoretically dominant; if the source is reduced, the intermediate scheme is reduced as well. This gives a scheme structure on a locally closed orbit.

The scheme structure is supplied by the morphism, including when the source is nonreduced. Local closedness alone does not imply flatness.

References

• Mathlib's Scheme.Hom.toImage and IsOpenImmersion.lift constructions.
• J. S. Milne, Algebraic Groups (2017), §§7.c–7.f (orbit schemes).
• The Stacks Project, Tag 01R5 (scheme-theoretic images).

def AlgebraicGeometry.Scheme.Hom.coborderRangeOfIsLocallyClosed {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : Y.Opens

The largest open subset of the target in which the topological image is closed.

Equations

• AlgebraicGeometry.Scheme.Hom.coborderRangeOfIsLocallyClosed f h = { carrier := coborder (Set.range ⇑f), is_open' := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.coe_coborderRangeOfIsLocallyClosed {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : ↑(coborderRangeOfIsLocallyClosed f h) = coborder (Set.range ⇑f)

The open used for the locally closed image has the coborder as its underlying set.

noncomputable def AlgebraicGeometry.Scheme.Hom.liftCoborderRange {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : X ⟶ ↑(coborderRangeOfIsLocallyClosed f h)

Regard a morphism with locally closed image as a morphism into the coborder of its image.

Equations

• AlgebraicGeometry.Scheme.Hom.liftCoborderRange f h = AlgebraicGeometry.IsOpenImmersion.lift (AlgebraicGeometry.Scheme.Hom.coborderRangeOfIsLocallyClosed f h).ι f ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.liftCoborderRange_ι {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : CategoryTheory.CategoryStruct.comp (liftCoborderRange f h) (coborderRangeOfIsLocallyClosed f h).ι = f

Composing the lift with the open inclusion recovers the original morphism.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.liftCoborderRange_ι_assoc {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) {Z : Scheme} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (liftCoborderRange f h) (CategoryTheory.CategoryStruct.comp (coborderRangeOfIsLocallyClosed f h).ι h✝) = CategoryTheory.CategoryStruct.comp f h✝

Composing the lift with the open inclusion recovers the original morphism.

theorem AlgebraicGeometry.Scheme.Hom.range_liftCoborderRange {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : Set.range ⇑(liftCoborderRange f h) = ⇑(coborderRangeOfIsLocallyClosed f h).ι ⁻¹' Set.range ⇑f

The lifted image is the preimage of the original image under the open inclusion.

theorem AlgebraicGeometry.Scheme.Hom.isClosed_range_liftCoborderRange {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : IsClosed (Set.range ⇑(liftCoborderRange f h))

The image becomes closed inside its coborder.

instance AlgebraicGeometry.Scheme.Hom.instQuasiCompactLiftCoborderRange {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (h : IsLocallyClosed (Set.range ⇑f)) : QuasiCompact (liftCoborderRange f h)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Hom.locallyClosedImage {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : Scheme

The scheme-theoretic image formed in an open where the original image is closed.

Equations

• AlgebraicGeometry.Scheme.Hom.locallyClosedImage f h = AlgebraicGeometry.Scheme.Hom.image (AlgebraicGeometry.Scheme.Hom.liftCoborderRange f h)

noncomputable def AlgebraicGeometry.Scheme.Hom.locallyClosedImageι {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : locallyClosedImage f h ⟶ Y

The immersion of the locally closed image into the original target.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.Hom.toLocallyClosedImage {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : X ⟶ locallyClosedImage f h

The canonical map from the source onto its locally closed scheme image.

Equations

• AlgebraicGeometry.Scheme.Hom.toLocallyClosedImage f h = AlgebraicGeometry.Scheme.Hom.toImage (AlgebraicGeometry.Scheme.Hom.liftCoborderRange f h)

theorem AlgebraicGeometry.Scheme.Hom.locallyClosedImageι_def {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : locallyClosedImageι f h = CategoryTheory.CategoryStruct.comp (imageι (liftCoborderRange f h)) (coborderRangeOfIsLocallyClosed f h).ι

The inclusion factors as a closed immersion into the coborder followed by that open subscheme's inclusion.

theorem AlgebraicGeometry.Scheme.Hom.toLocallyClosedImage_def {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : toLocallyClosedImage f h = toImage (liftCoborderRange f h)

The image factorization map is the usual scheme-theoretic image factorization of the lifted morphism.

instance AlgebraicGeometry.Scheme.Hom.instIsImmersionLocallyClosedImageι {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : IsImmersion (locallyClosedImageι f h)

The locally closed scheme image inclusion is an immersion.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toLocallyClosedImage_locallyClosedImageι {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) : CategoryTheory.CategoryStruct.comp (toLocallyClosedImage f h) (locallyClosedImageι f h) = f

The locally closed scheme image factorization recovers the original morphism.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toLocallyClosedImage_locallyClosedImageι_assoc {X Y : Scheme} (f : X ⟶ Y) (h : IsLocallyClosed (Set.range ⇑f)) {Z : Scheme} (h✝ : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (toLocallyClosedImage f h) (CategoryTheory.CategoryStruct.comp (locallyClosedImageι f h) h✝) = CategoryTheory.CategoryStruct.comp f h✝

The locally closed scheme image factorization recovers the original morphism.

instance AlgebraicGeometry.Scheme.Hom.instSurjectiveToLocallyClosedImage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (h : IsLocallyClosed (Set.range ⇑f)) : Surjective (toLocallyClosedImage f h)

The map onto the locally closed scheme image is surjective on all points.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.range_locallyClosedImageι {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (h : IsLocallyClosed (Set.range ⇑f)) : Set.range ⇑(locallyClosedImageι f h) = Set.range ⇑f

The immersion has precisely the original topological image, including nonclosed points.

instance AlgebraicGeometry.Scheme.Hom.instIsSchemeTheoreticallyDominantToLocallyClosedImage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (h : IsLocallyClosed (Set.range ⇑f)) : IsSchemeTheoreticallyDominant (toLocallyClosedImage f h)

No proper closed subscheme of the constructed image contains the factorization map.

instance AlgebraicGeometry.Scheme.Hom.instQuasiCompactToLocallyClosedImage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (h : IsLocallyClosed (Set.range ⇑f)) : QuasiCompact (toLocallyClosedImage f h)

The factorization map remains quasi-compact.

instance AlgebraicGeometry.Scheme.Hom.instLocallyOfFiniteTypeToLocallyClosedImage {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] (h : IsLocallyClosed (Set.range ⇑f)) : LocallyOfFiniteType (toLocallyClosedImage f h)

A locally finite-type morphism stays locally of finite type after factorization through its locally closed scheme image.