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.

TODO #

source
class AlgebraicGeometry.IsIntegralHom {X Y : AlgebraicGeometry.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.

Instances
    source
    theorem AlgebraicGeometry.isIntegralHom_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.IsIntegralHom f ↔ AlgebraicGeometry.IsAffineHom f ∧ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → (AlgebraicGeometry.Scheme.Hom.app f U).hom.IsIntegral
    source
    instance AlgebraicGeometry.IsIntegralHom.hasAffineProperty :
    AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsIntegralHom fun (X x : AlgebraicGeometry.Scheme) (f : X ⟶ x) (x_1 : AlgebraicGeometry.IsAffine x) => AlgebraicGeometry.IsAffine X ∧ (AlgebraicGeometry.Scheme.Hom.app f ⊤).hom.IsIntegral
    source
    instance AlgebraicGeometry.IsIntegralHom.instIsStableUnderCompositionScheme :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.IsIntegralHom
    source
    instance AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsIntegralHom
    source
    instance AlgebraicGeometry.IsIntegralHom.instContainsIdentitiesScheme :
    CategoryTheory.MorphismProperty.ContainsIdentities @AlgebraicGeometry.IsIntegralHom
    source
    instance AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme :
    CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsIntegralHom