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.

Also see AlgebraicGeometry.IsFinite.finite_preimage_singleton in Mathlib/AlgebraicGeometry/Fiber.lean for the fact that finite morphisms have finite fibers.

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
    theorem AlgebraicGeometry.IsFinite.SpecMap_iff {R S : CommRingCat} (f : R ⟶ S) :
    IsFinite (Spec.map f) ↔ (CommRingCat.Hom.hom f).Finite
    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
    source
    theorem AlgebraicGeometry.isFinite_iff_locallyOfFiniteType_of_jacobsonSpace {X Y : Scheme} {f : X ⟶ Y} [Subsingleton ↥X] [IsReduced X] [JacobsonSpace ↥Y] :
    IsFinite f ↔ LocallyOfFiniteType f

    If X is a jacobson scheme and k is a field, Spec(k) ⟶ X is finite iff it is (locally) of finite type. (The statement is more general to allow the empty scheme as well)

    source
    theorem AlgebraicGeometry.Scheme.Hom.closePoints_subset_preimage_closedPoints {X Y : Scheme} (f : X ⟶ Y) [JacobsonSpace ↥Y] [LocallyOfFiniteType f] :
    closedPoints ↥X ⊆ ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' closedPoints ↥Y

    Stacks Tag 01TB ((1) => (3))

    source
    theorem AlgebraicGeometry.isClosed_singleton_iff_locallyOfFiniteType {X : Scheme} [JacobsonSpace ↥X] {x : ↥X} :
    IsClosed {x} ↔ LocallyOfFiniteType (X.fromSpecResidueField x)

    Stacks Tag 01TB ((1) => (2))