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