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.

noncomputable 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.

Equations

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

noncomputable 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.

Equations

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

@[instance_reducible]

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

Equations

• AlgebraicGeometry.instCanonicallyOverFiber f y = { hom := AlgebraicGeometry.Scheme.Hom.fiberι f y }

noncomputable 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.

Equations

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

theorem AlgebraicGeometry.Scheme.Hom.fiber_fac {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) : CategoryTheory.CategoryStruct.comp (fiberι f y) f = CategoryTheory.CategoryStruct.comp (fiberToSpecResidueField f y) (Y.fromSpecResidueField y)

theorem AlgebraicGeometry.Scheme.Hom.fiber_fac_assoc {X Y : Scheme} (f : X ⟶ Y) (y : ↥Y) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (fiberι f y) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (fiberToSpecResidueField f y) (CategoryTheory.CategoryStruct.comp (Y.fromSpecResidueField y) h)

@[reducible]

noncomputable 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.

Equations

• AlgebraicGeometry.Scheme.Hom.fiberOverSpecResidueField f y = { hom := AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f y }

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.isPullback_fiberToSpecResidueField_of_isPullback {P X Y Z : Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) (y : ↥Y) : CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯) (Scheme.Hom.fiberToSpecResidueField snd y) (Scheme.Hom.fiberToSpecResidueField f (g y)) (Spec.map (Scheme.Hom.residueFieldMap g y))

noncomputable def AlgebraicGeometry.Spec.fiberToSpecResidueFieldIso (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) : CategoryTheory.Arrow.mk (Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p) ≅ CategoryTheory.Arrow.mk (map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))

The morphism from the fiber of Spec S ⟶ Spec R at some prime p to Spec κ(p) is isomorphic to the map induced by κ(p) ⟶ κ(p) ⊗[R] S.

Equations

• One or more equations did not get rendered due to their size.

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)

noncomputable 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}.

Equations

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

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

noncomputable 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.

Equations

• AlgebraicGeometry.Scheme.Hom.asFiber f x = (AlgebraicGeometry.Scheme.Hom.fiberHomeo f (f x)).symm ⟨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})

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)

noncomputable 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.

Equations

• AlgebraicGeometry.Scheme.Hom.asFiberHom f x = CategoryTheory.Limits.pullback.lift (X.fromSpecResidueField x) (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.residueFieldMap f 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)