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) : 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) : 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) : Scheme.CanonicallyOver X

Equations

• AlgebraicGeometry.instCanonicallyOver_1 f y = { hom := f.fiberι y }

def AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField {X Y : Scheme} (f : X.Hom Y) (y : ↥Y) : 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) : (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) (x : ↥(f.fiber y)) : (CategoryTheory.ConcreteCategory.hom (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) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (f.fiberι y).base) = ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' {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.Hom Y) (y : ↥Y) : ↥(f.fiber y) ≃ₜ ↑(⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' {y})

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

Equations

• f.fiberHomeo y = ⋯.toHomeomorph.trans (Homeomorph.setCongr ⋯)

@[simp]

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

@[simp]

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

def AlgebraicGeometry.Scheme.Hom.asFiber {X Y : Scheme} (f : X.Hom Y) (x : ↥X) : ↥(f.fiber ((CategoryTheory.ConcreteCategory.hom f.base) x))

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

Equations

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

@[simp]

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

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

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

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)

instance AlgebraicGeometry.instFiniteCarrierCarrierCommRingCatFiberOfIsFinite {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) [IsFinite f] : Finite ↥(Scheme.Hom.fiber f y)

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

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

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