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 ⟶ Y) (y : ↥Y) : Scheme

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

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

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

instance AlgebraicGeometry.instCanonicallyOverFiber {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) : (Scheme.Hom.fiber f y).CanonicallyOver X

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

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

@[reducible]

def AlgebraicGeometry.Scheme.Hom.fiberOverSpecResidueField {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) : (fiber f y).Over (Spec (Y.residueField y))

The fiber of f at y is naturally a κ(y)-scheme.

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

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

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

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

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

@[simp]

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

@[simp]

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

def AlgebraicGeometry.Scheme.Hom.asFiber {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : ↥(fiber f (f x))

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

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.fiberι_asFiber {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : (fiberι f (f x)) (asFiber f x) = x

instance AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatFiberOfQuasiCompact {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (y : ↥Y) : CompactSpace ↥(Scheme.Hom.fiber f y)

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

@[deprecated AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton (since := "2026-02-05")]

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

Alias of AlgebraicGeometry.Scheme.Hom.isCompact_preimage_singleton.

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

instance AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatFiberOfLocallyOfFiniteType {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) [LocallyOfFiniteType f] : JacobsonSpace ↥(Scheme.Hom.fiber f y)

def AlgebraicGeometry.Scheme.Hom.asFiberHom {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : Spec (X.residueField x) ⟶ fiber f (f x)

The κ(x)-point of f ⁻¹' {f x} corresponding to x.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : CategoryTheory.CategoryStruct.comp (asFiberHom f x) (fiberι f (f x)) = X.fromSpecResidueField x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι_assoc {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (asFiberHom f x) (CategoryTheory.CategoryStruct.comp (fiberι f (f x)) h) = CategoryTheory.CategoryStruct.comp (X.fromSpecResidueField x) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : CategoryTheory.CategoryStruct.comp (asFiberHom f x) (fiberToSpecResidueField f (f x)) = Spec.map (residueFieldMap f x)

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberToSpecResidueField_assoc {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) {Z : Scheme} (h : Spec (Y.residueField (f x)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (asFiberHom f x) (CategoryTheory.CategoryStruct.comp (fiberToSpecResidueField f (f x)) h) = CategoryTheory.CategoryStruct.comp (Spec.map (residueFieldMap f x)) h

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.asFiberHom_apply {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) (y : ↥(Spec (X.residueField x))) : (asFiberHom f x) y = asFiber f x

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.range_asFiberHom {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : Set.range ⇑(asFiberHom f x) = {asFiber f x}

instance AlgebraicGeometry.instIsPreimmersionAsFiberHom {X Y : Scheme} (f : X ⟶ Y) (x : ↥X) : IsPreimmersion (Scheme.Hom.asFiberHom f x)