Documentation

Mathlib.AlgebraicGeometry.Morphisms.Integral

Integral morphisms of schemes #

A morphism of schemes f : X ⟶ Y is integral if the preimage of an arbitrary affine open subset of Y is affine and the induced ring map is integral.

It is equivalent to ask only that Y is covered by affine opens whose preimage is affine and the induced ring map is integral.

A morphism of schemes X ⟶ Y is integral if the preimage of any affine open subset of Y is affine and the induced ring hom on sections is integral.

Instances
    @[deprecated AlgebraicGeometry.IsIntegralHom.isIntegral_app (since := "2025-10-15")]

    Alias of AlgebraicGeometry.IsIntegralHom.isIntegral_app.