Scheme-theoretic fiber

Main result

• AlgebraicGeometry.Scheme.Hom.fiber: f.fiber y is the scheme theoretic fiber of f at y.
• AlgebraicGeometry.Scheme.Hom.fiberHomeo: f.fiber y is homeomorphic to f ⁻¹' {y}.
• AlgebraicGeometry.Scheme.Hom.finite_preimage: Finite morphisms have finite fibers.
• AlgebraicGeometry.Scheme.Hom.discrete_fiber: Finite morphisms have discrete fibers.

def AlgebraicGeometry.Scheme.Hom.fiber {X Y : Scheme} (f : X.Hom Y) (y : ↑↑Y.toPresheafedSpace) : Scheme

f.fiber y is the scheme theoretic fiber of f at y.

Equations

• f.fiber y = CategoryTheory.Limits.pullback f (Y.fromSpecResidueField y)

def AlgebraicGeometry.Scheme.Hom.fiberι {X Y : Scheme} (f : X.Hom Y) (y : ↑↑Y.toPresheafedSpace) : f.fiber y ⟶ X

f.fiberι y : f.fiber y ⟶ X is the embedding of the scheme theoretic fiber into X.

Equations

• f.fiberι y = CategoryTheory.Limits.pullback.fst f (Y.fromSpecResidueField y)

instance AlgebraicGeometry.instCanonicallyOver_1 {X Y : Scheme} (f : X.Hom Y) (y : ↑↑Y.toPresheafedSpace) : Scheme.CanonicallyOver X

Equations

• AlgebraicGeometry.instCanonicallyOver_1 f y = CategoryTheory.CanonicallyOverClass.mk

def AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField {X Y : Scheme} (f : X.Hom Y) (y : ↑↑Y.toPresheafedSpace) : f.fiber y ⟶ Spec (Y.residueField y)

The canonical map from the scheme theoretic fiber to the residue field.

Equations

• f.fiberToSpecResidueField y = CategoryTheory.Limits.pullback.snd f (Y.fromSpecResidueField y)

@[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.

Equations

• f.fiberOverSpecResidueField y = { hom := f.fiberToSpecResidueField y }

theorem AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply {X Y : Scheme} (f : X.Hom Y) (y : ↑↑Y.toPresheafedSpace) (x : ↑↑(f.fiber y).toPresheafedSpace) : (f.fiberToSpecResidueField y).base x = IsLocalRing.closedPoint ↑(Y.residueField y)

theorem AlgebraicGeometry.Scheme.Hom.range_fiberι {X Y : Scheme} (f : X.Hom Y) (y : ↑↑Y.toPresheafedSpace) : Set.range ⇑(f.fiberι y).base = ⇑f.base ⁻¹' {y}

instance AlgebraicGeometry.instIsPreimmersionFiberι {X Y : Scheme} (f : X ⟶ Y) (y : ↑↑Y.toPresheafedSpace) : IsPreimmersion (Scheme.Hom.fiberι f y)

def AlgebraicGeometry.Scheme.Hom.fiberHomeo {X Y : Scheme} (f : X.Hom Y) (y : ↑↑Y.toPresheafedSpace) : ↑↑(f.fiber y).toPresheafedSpace ≃ₜ ↑(⇑f.base ⁻¹' {y})

The scheme theoretic fiber of f at y is homeomorphic to f ⁻¹' {y}.

Equations

• f.fiberHomeo y = (Homeomorph.ofIsEmbedding ⇑(f.fiberι y).base ⋯).trans (Homeomorph.setCongr ⋯)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.fiberHomeo_apply {X Y : Scheme} (f : X.Hom Y) (y : ↑↑Y.toPresheafedSpace) (x : ↑↑(f.fiber y).toPresheafedSpace) : ↑((f.fiberHomeo y) x) = (f.fiberι y).base x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm {X Y : Scheme} (f : X.Hom Y) (y : ↑↑Y.toPresheafedSpace) (x : ↑(⇑f.base ⁻¹' {y})) : (f.fiberι y).base ((f.fiberHomeo y).symm x) = ↑x

def AlgebraicGeometry.Scheme.Hom.asFiber {X Y : Scheme} (f : X.Hom Y) (x : ↑↑X.toPresheafedSpace) : ↑↑(f.fiber (f.base x)).toPresheafedSpace

A point x as a point in the fiber of f at f x.

Equations

• f.asFiber x = (f.fiberHomeo (f.base x)).symm ⟨x, ⋯⟩

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.fiberι_asFiber {X Y : Scheme} (f : X.Hom Y) (x : ↑↑X.toPresheafedSpace) : (f.fiberι (f.base x)).base (f.asFiber x) = x

instance AlgebraicGeometry.instCompactSpaceαTopologicalSpaceCarrierCommRingCatFiberOfQuasiCompact {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (y : ↑↑Y.toPresheafedSpace) : CompactSpace ↑↑(Scheme.Hom.fiber f y).toPresheafedSpace

theorem AlgebraicGeometry.QuasiCompact.isCompact_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (y : ↑↑Y.toPresheafedSpace) : IsCompact (⇑f.base ⁻¹' {y})

instance AlgebraicGeometry.instIsAffineFiberOfIsAffineHom {X Y : Scheme} (f : X ⟶ Y) [IsAffineHom f] (y : ↑↑Y.toPresheafedSpace) : IsAffine (Scheme.Hom.fiber f y)

instance AlgebraicGeometry.instJacobsonSpaceαTopologicalSpaceCarrierCommRingCatFiberOfLocallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) (y : ↑↑Y.toPresheafedSpace) [LocallyOfFiniteType f] : JacobsonSpace ↑↑(Scheme.Hom.fiber f y).toPresheafedSpace

instance AlgebraicGeometry.instFiniteαTopologicalSpaceCarrierCommRingCatFiberOfIsFinite {X Y : Scheme} (f : X ⟶ Y) (y : ↑↑Y.toPresheafedSpace) [IsFinite f] : Finite ↑↑(Scheme.Hom.fiber f y).toPresheafedSpace

theorem AlgebraicGeometry.IsFinite.finite_preimage_singleton {X Y : Scheme} (f : X ⟶ Y) [IsFinite f] (y : ↑↑Y.toPresheafedSpace) : (⇑f.base ⁻¹' {y}).Finite

theorem AlgebraicGeometry.Scheme.Hom.finite_preimage {X Y : Scheme} (f : X.Hom Y) [IsFinite f] {s : Set ↑↑Y.toPresheafedSpace} (hs : s.Finite) : (⇑f.base ⁻¹' s).Finite

instance AlgebraicGeometry.Scheme.Hom.discrete_fiber {X Y : Scheme} (f : X ⟶ Y) (y : ↑↑Y.toPresheafedSpace) [IsFinite f] : DiscreteTopology ↑↑(fiber f y).toPresheafedSpace