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.
TODO #
- Show integral = universally closed + affine
class
AlgebraicGeometry.IsIntegralHom
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
extends AlgebraicGeometry.IsAffineHom f :
A morphism of schemes X ⟶ Y is finite if
the preimage of any affine open subset of Y is affine and the induced ring
hom is finite.
- isAffine_preimage : ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
- integral_app : ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → RingHom.IsIntegral (AlgebraicGeometry.Scheme.Hom.app f U)
Instances
theorem
AlgebraicGeometry.isIntegralHom_iff
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
:
AlgebraicGeometry.IsIntegralHom f ↔ AlgebraicGeometry.IsAffineHom f ∧ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → RingHom.IsIntegral (AlgebraicGeometry.Scheme.Hom.app f U)
instance
AlgebraicGeometry.IsIntegralHom.hasAffineProperty :
AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsIntegralHom
fun (X x : AlgebraicGeometry.Scheme) (f : X ⟶ x) (x_1 : AlgebraicGeometry.IsAffine x) =>
AlgebraicGeometry.IsAffine X ∧ RingHom.IsIntegral (AlgebraicGeometry.Scheme.Hom.app f ⊤)