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.
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.
- isAffine_preimage (U : Y.Opens) : IsAffineOpen U → IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)
Instances
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)
Stacks Tag 01TB ((1) => (3))
Stacks Tag 01TB ((1) => (2))