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.

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

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.

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 AlgebraicGeometry.IsIntegralHom.instIsStableUnderCompositionScheme :

CategoryTheory.MorphismProperty.IsStableUnderComposition @IsIntegralHom

instance AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme :

CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsIntegralHom

@[instance 100]

instance AlgebraicGeometry.IsIntegralHom.instOfIsClosedImmersion {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] :

IsIntegralHom f

instance AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme :

CategoryTheory.MorphismProperty.IsMultiplicative @IsIntegralHom

instance AlgebraicGeometry.IsIntegralHom.instCompScheme {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIntegralHom f] [IsIntegralHom g] :

IsIntegralHom (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.IsIntegralHom.instFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsIntegralHom g] :

IsIntegralHom (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.IsIntegralHom.instSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsIntegralHom f] :

IsIntegralHom (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.IsIntegralHom.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [IsIntegralHom f] :

IsIntegralHom (f ∣_ V)

instance AlgebraicGeometry.IsIntegralHom.instHasOfPostcompPropertySchemeIsSeparated :

CategoryTheory.MorphismProperty.HasOfPostcompProperty @IsIntegralHom @IsSeparated

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

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

theorem AlgebraicGeometry.IsIntegralHom.SpecMap_iff {R S : CommRingCat} {φ : R ⟶ S} :

IsIntegralHom (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral

instance AlgebraicGeometry.IsIntegralHom.instIsMultiplicativeScheme_1 :

CategoryTheory.MorphismProperty.IsMultiplicative @IsIntegralHom

instance AlgebraicGeometry.IsIntegralHom.instDescScheme {U V X : Scheme} (f : U ⟶ X) (g : V ⟶ X) [IsIntegralHom f] [IsIntegralHom g] :

IsIntegralHom (CategoryTheory.Limits.coprod.desc f g)

@[instance 100]

instance AlgebraicGeometry.IsIntegralHom.instUniversallyClosed {X Y : Scheme} (f : X ⟶ Y) [IsIntegralHom f] :

UniversallyClosed f

theorem AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom {X Y : Scheme} {f : X ⟶ Y} :

IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f

theorem AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom :

@IsIntegralHom = @UniversallyClosed ⊓ @IsAffineHom