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 : Scheme} (f : X ⟶ Y) extends AlgebraicGeometry.IsAffineHom f : Prop

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) : IsAffineOpen U → IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
• integral_app (U : Y.Opens) (hU : IsAffineOpen U) : (Scheme.Hom.app f U).hom.IsIntegral

theorem AlgebraicGeometry.isIntegralHom_iff {X Y : Scheme} (f : X ⟶ Y) : IsIntegralHom f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (Scheme.Hom.app f U).hom.IsIntegral

instance AlgebraicGeometry.IsIntegralHom.hasAffineProperty : HasAffineProperty @IsIntegralHom fun (X x : Scheme) (f : X ⟶ x) (x_1 : IsAffine x) => IsAffine X ∧ (Scheme.Hom.app f ⊤).hom.IsIntegral

instance AlgebraicGeometry.IsIntegralHom.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @IsIntegralHom

instance AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsIntegralHom

instance AlgebraicGeometry.IsIntegralHom.instContainsIdentitiesScheme : CategoryTheory.MorphismProperty.ContainsIdentities @IsIntegralHom

instance AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @IsIntegralHom