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.
class
AlgebraicGeometry.IsIntegralHom
{X Y : Scheme}
(f : X ⟶ Y)
extends AlgebraicGeometry.IsAffineHom f :
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.
- isAffine_preimage (U : Y.Opens) : IsAffineOpen U → IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
- isIntegral_app (U : Y.Opens) (hU : IsAffineOpen U) : (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral
Instances
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
@[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)
:
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
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
@[instance 100]
instance
AlgebraicGeometry.IsIntegralHom.instOfIsClosedImmersion
{X Y : Scheme}
(f : X ⟶ Y)
[IsClosedImmersion f]
:
instance
AlgebraicGeometry.IsIntegralHom.instCompScheme
{X Y Z : Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[IsIntegralHom f]
[IsIntegralHom g]
:
instance
AlgebraicGeometry.IsIntegralHom.instFstScheme
{X Y S : Scheme}
(f : X ⟶ S)
(g : Y ⟶ S)
[IsIntegralHom g]
:
instance
AlgebraicGeometry.IsIntegralHom.instSndScheme
{X Y S : Scheme}
(f : X ⟶ S)
(g : Y ⟶ S)
[IsIntegralHom f]
:
instance
AlgebraicGeometry.IsIntegralHom.instMorphismRestrict
{X Y : Scheme}
(f : X ⟶ Y)
(V : Y.Opens)
[IsIntegralHom f]
:
IsIntegralHom (f ∣_ V)
theorem
AlgebraicGeometry.IsIntegralHom.of_comp
{X Y Z : Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[IsIntegralHom (CategoryTheory.CategoryStruct.comp f g)]
[IsSeparated g]
:
theorem
AlgebraicGeometry.IsIntegralHom.comp_iff
{X Y Z : Scheme}
{f : X ⟶ Y}
{g : Y ⟶ Z}
[IsIntegralHom g]
:
@[instance 100]
instance
AlgebraicGeometry.IsIntegralHom.instUniversallyClosed
{X Y : Scheme}
(f : X ⟶ Y)
[IsIntegralHom f]
:
theorem
AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom
{X Y : Scheme}
{f : X ⟶ Y}
: