The special fibre as the fibre at the closed point

For a scheme over a local ring, base change to the ring's residue field agrees with the scheme-theoretic fibre at the closed point. The two residue fields are constructed differently: one is the quotient by the maximal ideal, while the other is the residue field of the scheme point. This file gives their canonical equivalence and the resulting comparison of fibres, including its projection identities.

The comparison lets statements about the special fibre be transported between its base-change presentation and the fibre over the closed point, while preserving both projections.

noncomputable def TauCeti.localResidueFieldEquiv (R : CommRingCat) [IsLocalRing ↑R] : IsLocalRing.ResidueField ↑R ≃+* ↑((AlgebraicGeometry.Spec R).residueField (IsLocalRing.closedPoint ↑R))

The two constructions of the residue field at a local ring's closed point agree.

Equations

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

@[simp]

theorem TauCeti.localResidueFieldEquiv_algebraMap (R : CommRingCat) [IsLocalRing ↑R] (r : ↑R) : (localResidueFieldEquiv R) ((IsLocalRing.residue ↑R) r) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Spec.residueFieldIso R (IsLocalRing.closedPoint ↑R)).inv) ((algebraMap (↑R) (IsLocalRing.maximalIdeal ↑R).ResidueField) r)

The closed-point residue-field equivalence respects the map from the local ring.

noncomputable def TauCeti.specLocalResidueFieldIso (R : CommRingCat) [IsLocalRing ↑R] : AlgebraicGeometry.Spec ↧(IsLocalRing.ResidueField ↑R) ≅ AlgebraicGeometry.Spec ↧↑((AlgebraicGeometry.Spec R).residueField (IsLocalRing.closedPoint ↑R))

The spectrum of a local ring's residue field is the spectrum of the residue field at its closed point.

Equations

• TauCeti.specLocalResidueFieldIso R = AlgebraicGeometry.Scheme.Spec.mapIso (TauCeti.localResidueFieldEquiv R).toCommRingCatIso.symm.op

@[simp]

theorem TauCeti.specLocalResidueFieldIso_hom_fromSpecResidueField (R : CommRingCat) [IsLocalRing ↑R] : CategoryTheory.CategoryStruct.comp (specLocalResidueFieldIso R).hom ((AlgebraicGeometry.Spec R).fromSpecResidueField (IsLocalRing.closedPoint ↑R)) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (IsLocalRing.ResidueField ↑R)))

The residue-field map from a local ring is the canonical map from its closed point, after identifying the two presentations of the residue field.

@[simp]

theorem TauCeti.specLocalResidueFieldIso_hom_fromSpecResidueField_assoc (R : CommRingCat) [IsLocalRing ↑R] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec R ⟶ Z) : CategoryTheory.CategoryStruct.comp (specLocalResidueFieldIso R).hom (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).fromSpecResidueField (IsLocalRing.closedPoint ↑R)) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (↑R) (IsLocalRing.ResidueField ↑R)))) h

The residue-field map from a local ring is the canonical map from its closed point, after identifying the two presentations of the residue field.

theorem TauCeti.isPullback_specialFiber_closedPoint (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) : CategoryTheory.IsPullback (specialFiberι (↑R) toBase) (CategoryTheory.CategoryStruct.comp (specialFiber (↑R) toBase).hom (specLocalResidueFieldIso R).hom) toBase ((AlgebraicGeometry.Spec R).fromSpecResidueField (IsLocalRing.closedPoint ↑R))

The square defining the special fibre is the scheme-theoretic fibre square over the closed point of the base.

noncomputable def TauCeti.specialFiberIsoFiberClosedPoint (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) : (specialFiber (↑R) toBase).left ≅ AlgebraicGeometry.Scheme.Hom.fiber toBase (IsLocalRing.closedPoint ↑R)

The special fibre over the residue field of a local ring is canonically isomorphic to Mathlib's fibre at the closed point.

Equations

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

@[simp]

theorem TauCeti.specialFiberIsoFiberClosedPoint_hom_fiberι (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) : CategoryTheory.CategoryStruct.comp (specialFiberIsoFiberClosedPoint R toBase).hom (AlgebraicGeometry.Scheme.Hom.fiberι toBase (IsLocalRing.closedPoint ↑R)) = specialFiberι (↑R) toBase

The closed-point fibre comparison preserves the maps to the total space.

@[simp]

theorem TauCeti.specialFiberIsoFiberClosedPoint_hom_fiberι_assoc (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (specialFiberIsoFiberClosedPoint R toBase).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberι toBase (IsLocalRing.closedPoint ↑R)) h) = CategoryTheory.CategoryStruct.comp (specialFiberι (↑R) toBase) h

The closed-point fibre comparison preserves the maps to the total space.

@[simp]

theorem TauCeti.specialFiberIsoFiberClosedPoint_hom_fiberToSpecResidueField (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) : CategoryTheory.CategoryStruct.comp (specialFiberIsoFiberClosedPoint R toBase).hom (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField toBase (IsLocalRing.closedPoint ↑R)) = CategoryTheory.CategoryStruct.comp (specialFiber (↑R) toBase).hom (specLocalResidueFieldIso R).hom

The closed-point fibre comparison preserves the maps to the residue-field spectrum.

@[simp]

theorem TauCeti.specialFiberIsoFiberClosedPoint_hom_fiberToSpecResidueField_assoc (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ((AlgebraicGeometry.Spec R).residueField (IsLocalRing.closedPoint ↑R)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (specialFiberIsoFiberClosedPoint R toBase).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField toBase (IsLocalRing.closedPoint ↑R)) h) = CategoryTheory.CategoryStruct.comp (specialFiber (↑R) toBase).hom (CategoryTheory.CategoryStruct.comp (specLocalResidueFieldIso R).hom h)

The closed-point fibre comparison preserves the maps to the residue-field spectrum.

@[simp]

theorem TauCeti.specialFiberIsoFiberClosedPoint_inv_specialFiberι (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) : CategoryTheory.CategoryStruct.comp (specialFiberIsoFiberClosedPoint R toBase).inv (specialFiberι (↑R) toBase) = AlgebraicGeometry.Scheme.Hom.fiberι toBase (IsLocalRing.closedPoint ↑R)

The inverse closed-point fibre comparison preserves the maps to the total space.

@[simp]

theorem TauCeti.specialFiberIsoFiberClosedPoint_inv_specialFiberι_assoc (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (specialFiberIsoFiberClosedPoint R toBase).inv (CategoryTheory.CategoryStruct.comp (specialFiberι (↑R) toBase) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberι toBase (IsLocalRing.closedPoint ↑R)) h

The inverse closed-point fibre comparison preserves the maps to the total space.

@[simp]

theorem TauCeti.specialFiberIsoFiberClosedPoint_inv_fiberToSpecResidueField (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) : CategoryTheory.CategoryStruct.comp (specialFiberIsoFiberClosedPoint R toBase).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue ↑R)))) (specLocalResidueFieldIso R).hom) = AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField toBase (IsLocalRing.closedPoint ↑R)

The inverse closed-point fibre comparison preserves the maps to the residue-field spectrum. The structure morphism (specialFiber R toBase).hom is written in its simp normal form, the pullback projection given by specialFiber_hom.

theorem TauCeti.specialFiberIsoFiberClosedPoint_inv_fiberToSpecResidueField_assoc (R : CommRingCat) [IsLocalRing ↑R] {X : AlgebraicGeometry.Scheme} (toBase : X ⟶ AlgebraicGeometry.Spec R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧↑((AlgebraicGeometry.Spec R).residueField (IsLocalRing.closedPoint ↑R)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (specialFiberIsoFiberClosedPoint R toBase).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd toBase (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue ↑R)))) (specLocalResidueFieldIso R).hom) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField toBase (IsLocalRing.closedPoint ↑R)) h

The inverse closed-point fibre comparison preserves the maps to the residue-field spectrum. The structure morphism (specialFiber R toBase).hom is written in its simp normal form, the pullback projection given by specialFiber_hom.