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 integral if the preimage of any affine open subset of Y is affine and the induced ring hom on sections is integral.

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
    @[deprecated AlgebraicGeometry.IsIntegralHom.isIntegral_app (since := "2025-10-15")]
    theorem AlgebraicGeometry.IsIntegralHom.integral_app {X Y : Scheme} (f : X ⟶ Y) [self : IsIntegralHom f] (U : Y.Opens) (hU : IsAffineOpen U) :
    (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral

    Alias of AlgebraicGeometry.IsIntegralHom.isIntegral_app.

    source
    theorem AlgebraicGeometry.Scheme.Hom.isIntegral_app {X Y : Scheme} (f : X ⟶ Y) [self : IsIntegralHom f] (U : Y.Opens) (hU : IsAffineOpen U) :
    (CommRingCat.Hom.hom (app f U)).IsIntegral

    Alias of AlgebraicGeometry.IsIntegralHom.isIntegral_app.

    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 100]
    instance AlgebraicGeometry.IsIntegralHom.instOfIsClosedImmersion {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] :
    IsIntegralHom f
    source
    instance AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme :
    CategoryTheory.MorphismProperty.IsMultiplicative @IsIntegralHom
    source
    instance AlgebraicGeometry.IsIntegralHom.instCompScheme {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIntegralHom f] [IsIntegralHom g] :
    IsIntegralHom (CategoryTheory.CategoryStruct.comp f g)
    source
    instance AlgebraicGeometry.IsIntegralHom.instFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsIntegralHom g] :
    IsIntegralHom (CategoryTheory.Limits.pullback.fst f g)
    source
    instance AlgebraicGeometry.IsIntegralHom.instSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsIntegralHom f] :
    IsIntegralHom (CategoryTheory.Limits.pullback.snd f g)
    source
    instance AlgebraicGeometry.IsIntegralHom.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [IsIntegralHom f] :
    IsIntegralHom (f ∣_ V)
    source
    instance AlgebraicGeometry.IsIntegralHom.instHasOfPostcompPropertySchemeIsSeparated :
    CategoryTheory.MorphismProperty.HasOfPostcompProperty @IsIntegralHom @IsSeparated
    source
    theorem AlgebraicGeometry.IsIntegralHom.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIntegralHom (CategoryTheory.CategoryStruct.comp f g)] [IsSeparated g] :
    IsIntegralHom f
    source
    theorem AlgebraicGeometry.IsIntegralHom.comp_iff {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [IsIntegralHom g] :
    IsIntegralHom (CategoryTheory.CategoryStruct.comp f g) ↔ IsIntegralHom f
    source
    theorem AlgebraicGeometry.IsIntegralHom.SpecMap_iff {R S : CommRingCat} {φ : R ⟶ S} :
    IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral
    source
    instance AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme_1 :
    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