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.

source
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.

Instances
    source
    theorem AlgebraicGeometry.isIntegralHom_iff {X Y : Scheme} (f : X ⟶ Y) :
    IsIntegralHom f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral
    source
    instance AlgebraicGeometry.IsIntegralHom.hasAffineProperty :
    HasAffineProperty @IsIntegralHom fun (X x : Scheme) (f : X ⟶ x) (x_1 : IsAffine x) => IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)).IsIntegral
    source
    instance AlgebraicGeometry.IsIntegralHom.instIsStableUnderCompositionScheme :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @IsIntegralHom
    source
    instance AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsIntegralHom
    source
    instance AlgebraicGeometry.IsIntegralHom.instContainsIdentitiesScheme :
    CategoryTheory.MorphismProperty.ContainsIdentities @IsIntegralHom
    source
    theorem AlgebraicGeometry.IsIntegralHom.SpecMap_iff {R S : CommRingCat} {φ : R ⟶ S} :
    IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral
    source
    instance AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme :
    CategoryTheory.MorphismProperty.IsMultiplicative @IsIntegralHom
    source
    @[instance 100]
    instance AlgebraicGeometry.IsIntegralHom.instUniversallyClosed {X Y : Scheme} (f : X ⟶ Y) [IsIntegralHom f] :
    UniversallyClosed f
    source
    theorem AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom {X Y : Scheme} {f : X ⟶ Y} :
    IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f
    source
    theorem AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom :
    @IsIntegralHom = @UniversallyClosed ⊓ @IsAffineHom