Documentation

Mathlib.AlgebraicGeometry.Morphisms.Finite

Finite morphisms of schemes #

A morphism of schemes f : X ⟶ Y is finite if the preimage of an arbitrary affine open subset of Y is affine and the induced ring map is finite.

It is equivalent to ask only that Y is covered by affine opens whose preimage is affine and the induced ring map is finite.

TODO #

source
class AlgebraicGeometry.IsFinite {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.isFinite_iff {X Y : Scheme} (f : X ⟶ Y) :
    IsFinite f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).Finite
    source
    instance AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop :
    HasAffineProperty @IsFinite fun (X x : Scheme) (f : X ⟶ x) (x_1 : IsAffine x) => IsAffine X ∧ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
    source
    instance AlgebraicGeometry.IsFinite.instIsStableUnderCompositionScheme :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @IsFinite
    source
    instance AlgebraicGeometry.IsFinite.instIsStableUnderBaseChangeScheme :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsFinite
    source
    instance AlgebraicGeometry.IsFinite.instContainsIdentitiesScheme :
    CategoryTheory.MorphismProperty.ContainsIdentities @IsFinite
    source
    instance AlgebraicGeometry.IsFinite.instIsMultiplicativeScheme :
    CategoryTheory.MorphismProperty.IsMultiplicative @IsFinite
    source
    @[instance 900]
    instance AlgebraicGeometry.IsFinite.instOfIsIsoScheme {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] :
    IsFinite f
    source
    instance AlgebraicGeometry.IsFinite.instCompScheme {X Y : Scheme} (f : X ⟶ Y) {Z : Scheme} (g : Y ⟶ Z) [IsFinite f] [IsFinite g] :
    IsFinite (CategoryTheory.CategoryStruct.comp f g)
    source
    theorem AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) :
    IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f
    source
    theorem AlgebraicGeometry.IsFinite.eq_inf :
    @IsFinite = @IsIntegralHom ⊓ @LocallyOfFiniteType
    source
    @[instance 900]
    instance AlgebraicGeometry.IsFinite.instIsIntegralHom {X Y : Scheme} (f : X ⟶ Y) [IsFinite f] :
    IsIntegralHom f
    source
    @[instance 900]
    instance AlgebraicGeometry.IsFinite.instLocallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) [hf : IsFinite f] :
    LocallyOfFiniteType f
    source
    theorem AlgebraicGeometry.IsClosedImmersion.iff_isFinite_and_mono {X Y : Scheme} (f : X ⟶ Y) :
    IsClosedImmersion f ↔ IsFinite f ∧ CategoryTheory.Mono f
    source
    theorem AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono :
    @IsClosedImmersion = @IsFinite ⊓ CategoryTheory.MorphismProperty.monomorphisms Scheme
    source
    @[instance 900]
    instance AlgebraicGeometry.IsFinite.instOfIsClosedImmersion {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] :
    IsFinite f