Scheme-theoretic fiber #
Main result #
AlgebraicGeometry.Scheme.Hom.fiber
:f.fiber y
is the scheme theoretic fiber off
aty
.AlgebraicGeometry.Scheme.Hom.fiberHomeo
:f.fiber y
is homeomorphic tof ⁻¹' {y}
.AlgebraicGeometry.Scheme.Hom.finite_preimage
: Finite morphisms have finite fibers.AlgebraicGeometry.Scheme.Hom.discrete_fiber
: Finite morphisms have discrete fibers.
f.fiber y
is the scheme theoretic fiber of f
at y
.
Instances For
f.fiberι y : f.fiber y ⟶ X
is the embedding of the scheme theoretic fiber into X
.
Instances For
def
AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
{X Y : Scheme}
(f : X.Hom Y)
(y : ↑↑Y.toPresheafedSpace)
:
The canonical map from the scheme theoretic fiber to the residue field.
Equations
Instances For
@[reducible]
def
AlgebraicGeometry.Scheme.Hom.fiberOverSpecResidueField
{X Y : Scheme}
(f : X.Hom Y)
(y : ↑↑Y.toPresheafedSpace)
:
(f.fiber y).Over (Spec (Y.residueField y))
The fiber of f
at y
is naturally a κ(y)
-scheme.
Instances For
instance
AlgebraicGeometry.instIsPreimmersionFiberι
{X Y : Scheme}
(f : X ⟶ Y)
(y : ↑↑Y.toPresheafedSpace)
:
def
AlgebraicGeometry.Scheme.Hom.fiberHomeo
{X Y : Scheme}
(f : X.Hom Y)
(y : ↑↑Y.toPresheafedSpace)
:
The scheme theoretic fiber of f
at y
is homeomorphic to f ⁻¹' {y}
.
Equations
Instances For
@[simp]
theorem
AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply
{X Y : Scheme}
(f : X.Hom Y)
(y : ↑↑Y.toPresheafedSpace)
(x : ↑↑(f.fiber y).toPresheafedSpace)
:
def
AlgebraicGeometry.Scheme.Hom.asFiber
{X Y : Scheme}
(f : X.Hom Y)
(x : ↑↑X.toPresheafedSpace)
:
↑↑(f.fiber ((CategoryTheory.ConcreteCategory.hom f.base) x)).toPresheafedSpace
A point x
as a point in the fiber of f
at f x
.
Equations
Instances For
instance
AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact
{X Y : Scheme}
(f : X ⟶ Y)
[QuasiCompact f]
(y : ↑↑Y.toPresheafedSpace)
:
instance
AlgebraicGeometry.instIsAffineFiberOfIsAffineHom
{X Y : Scheme}
(f : X ⟶ Y)
[IsAffineHom f]
(y : ↑↑Y.toPresheafedSpace)
:
IsAffine (Scheme.Hom.fiber f y)
instance
AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType
{X Y : Scheme}
(f : X ⟶ Y)
(y : ↑↑Y.toPresheafedSpace)
[LocallyOfFiniteType f]
:
instance
AlgebraicGeometry.instFiniteCarrierCarrierCommRingCatFiberOfIsFinite
{X Y : Scheme}
(f : X ⟶ Y)
(y : ↑↑Y.toPresheafedSpace)
[IsFinite f]
:
Finite ↑↑(Scheme.Hom.fiber f y).toPresheafedSpace
instance
AlgebraicGeometry.Scheme.Hom.discrete_fiber
{X Y : Scheme}
(f : X ⟶ Y)
(y : ↑↑Y.toPresheafedSpace)
[IsFinite f]
:
DiscreteTopology ↑↑(fiber f y).toPresheafedSpace