Documentation

TauCeti.AlgebraicGeometry.Fibers.ResidueBaseChange

Special fibres and local base change #

For a local homomorphism of local rings, taking the special fibre after base change agrees canonically with extending the original special fibre along the induced extension of residue fields. The isomorphism compares two iterated pullbacks of schemes and preserves their maps to the original total space and to the new residue-field spectrum. It is the comparison used when changing the chosen DVR in a model of a curve.

source
noncomputable def TauCeti.specialFiberBaseChangeIso {R S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) :
(specialFiber S (genericFiber R S f).hom).left ≅ (genericFiber (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) (specialFiber R f).hom).left

Base change to a local ring followed by passage to its special fibre is the same as extending the original special fibre to the larger residue field.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.specialFiberBaseChangeIso_hom_fst {R S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) :
    CategoryTheory.CategoryStruct.comp (specialFiberBaseChangeIso f).hom (CategoryTheory.CategoryStruct.comp (genericFiberι (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))))) (specialFiberι R f)) = CategoryTheory.CategoryStruct.comp (specialFiberι S (genericFiber R S f).hom) (genericFiberι R S f)

    The special-fibre base-change isomorphism preserves projection to the original scheme.

    source
    @[simp]
    theorem TauCeti.specialFiberBaseChangeIso_hom_fst_assoc {R S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (specialFiberBaseChangeIso f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (genericFiberι (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))))) (specialFiberι R f)) h) = CategoryTheory.CategoryStruct.comp (specialFiberι S (genericFiber R S f).hom) (CategoryTheory.CategoryStruct.comp (genericFiberι R S f) h)

    The special-fibre base-change isomorphism preserves projection to the original scheme.

    source
    @[simp]
    theorem TauCeti.specialFiberBaseChangeIso_hom_snd {R S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) :
    CategoryTheory.CategoryStruct.comp (specialFiberBaseChangeIso f).hom (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S))))) = (specialFiber S (genericFiber R S f).hom).hom

    The special-fibre base-change isomorphism preserves projection to the new residue-field spectrum.

    source
    theorem TauCeti.specialFiberBaseChangeIso_hom_snd_assoc {R S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(IsLocalRing.ResidueField S) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (specialFiberBaseChangeIso f).hom (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)))))) h = CategoryTheory.CategoryStruct.comp (specialFiber S (genericFiber R S f).hom).hom h

    The special-fibre base-change isomorphism preserves projection to the new residue-field spectrum.

    source
    @[simp]
    theorem TauCeti.specialFiberBaseChangeIso_inv_fst {R S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) :
    CategoryTheory.CategoryStruct.comp (specialFiberBaseChangeIso f).inv (CategoryTheory.CategoryStruct.comp (specialFiberι S (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))))) (genericFiberι R S f)) = CategoryTheory.CategoryStruct.comp (genericFiberι (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))))) (specialFiberι R f)

    The inverse special-fibre base-change isomorphism preserves projection to the original scheme.

    source
    @[simp]
    theorem TauCeti.specialFiberBaseChangeIso_inv_fst_assoc {R S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (specialFiberBaseChangeIso f).inv (CategoryTheory.CategoryStruct.comp (specialFiberι S (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))))) (CategoryTheory.CategoryStruct.comp (genericFiberι R S f) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (genericFiberι (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S) (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))))) (specialFiberι R f)) h

    The inverse special-fibre base-change isomorphism preserves projection to the original scheme.

    source
    @[simp]
    theorem TauCeti.specialFiberBaseChangeIso_inv_snd {R S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) :
    CategoryTheory.CategoryStruct.comp (specialFiberBaseChangeIso f).inv (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue S)))) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S))))

    The inverse special-fibre base-change isomorphism preserves projection to the new residue-field spectrum.

    source
    theorem TauCeti.specialFiberBaseChangeIso_inv_snd_assoc {R S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧R) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(IsLocalRing.ResidueField S) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (specialFiberBaseChangeIso f).inv (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue S))))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (IsLocalRing.residue R)))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S))))) h

    The inverse special-fibre base-change isomorphism preserves projection to the new residue-field spectrum.