Scheme-theoretic images

This file contains general results about Mathlib's scheme-theoretic image construction. For a quasi-compact morphism the map onto its scheme-theoretic image is scheme-theoretically dominant. In particular, a reduced source gives a reduced image. When the topological image is closed, the factorization is surjective on points.

Main declarations

• TauCeti.specTargetImageIdeal_specMap: the ideal defining the image of a spectrum map is the kernel of the corresponding ring homomorphism.

References

• The Stacks Project, Tag 01R5, especially Lemmas 29.6.3 and 29.6.7.

@[simp]

theorem TauCeti.specTargetImageIdeal_specMap {R S : CommRingCat} (f : R ⟶ S) : AlgebraicGeometry.specTargetImageIdeal (AlgebraicGeometry.Spec.map f) = RingHom.ker (CommRingCat.Hom.hom f)

The ideal defining the scheme-theoretic image of a spectrum map is the kernel of the corresponding ring homomorphism.

instance AlgebraicGeometry.Scheme.Hom.isSchemeTheoreticallyDominant_toImage {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] : IsSchemeTheoreticallyDominant (toImage f)

The factorization through the scheme-theoretic image is scheme-theoretically dominant.

instance AlgebraicGeometry.Scheme.Hom.isReduced_image {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [IsReduced X] : IsReduced (image f)

The scheme-theoretic image of a quasi-compact morphism from a reduced scheme is reduced.

theorem AlgebraicGeometry.Scheme.Hom.toImage_surjective_of_isClosed_range {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (h : IsClosed (Set.range ⇑f)) : Function.Surjective ⇑(toImage f)

If a quasi-compact morphism has closed topological image, its map to the scheme-theoretic image is surjective.