A ring map to a local ring factors through localization at the contracted maximal ideal. The residue fiber of a scheme over the stage is unchanged by this localization. These actual maps compare sections lifted at the local stage with their pullbacks to the original closed fiber.
The contraction of the original closed point to the stage.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)abbrev prime : Ideal BThe actual factorization through localization at the contracted prime.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)def localizationMap : Localization.AtPrime (prime φ) →+* ASurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)lemma localizationMap_comp :
(localizationMap φ).comp (algebraMap B (Localization.AtPrime (prime φ))) = φThe spectrum map from the original local ring to the localized stage.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)abbrev localSpecMap : Spec (CommRingCat.of A) ⟶
Spec (CommRingCat.of (Localization.AtPrime (prime φ)))The localization morphism of the stage.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)abbrev localizationSpec : Spec (CommRingCat.of (Localization.AtPrime (prime φ))) ⟶
Spec (CommRingCat.of B)The residue point of the localized stage uses its actual quotient map.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)abbrev residueSpec : Spec (CommRingCat.of (prime φ).ResidueField) ⟶
Spec (CommRingCat.of (Localization.AtPrime (prime φ)))The original residue point of the stage.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)abbrev stageResidueSpec : Spec (CommRingCat.of (prime φ).ResidueField) ⟶
Spec (CommRingCat.of B)The closed residue point of the original local base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)abbrev topResidueSpec : Spec (CommRingCat.of (IsLocalRing.maximalIdeal A).ResidueField) ⟶
Spec (CommRingCat.of A)The actual residue-field extension from a stage to the original base.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)abbrev residueMap : Spec (CommRingCat.of (IsLocalRing.maximalIdeal A).ResidueField) ⟶
Spec (CommRingCat.of (prime φ).ResidueField)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)lemma localSpecMap_localizationSpec :
localSpecMap φ ≫ localizationSpec φ = Spec.map (CommRingCat.ofHom φ)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)lemma residueSpec_localizationSpec :
residueSpec φ ≫ localizationSpec φ = stageResidueSpec φSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)lemma residueMap_residueSpec :
residueMap φ ≫ residueSpec φ = topResidueSpec (A := A) ≫ localSpecMap φSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)lemma residueMap_stageResidueSpec :
residueMap φ ≫ stageResidueSpec φ =
topResidueSpec (A := A) ≫ Spec.map (CommRingCat.ofHom φ)The actual stage after localization.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)
variable {P X : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of B))abbrev localizedScheme : Scheme.{u}The actual proper structure map after localization.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)
variable {P X : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of B))abbrev localizedBaseMap : localizedScheme φ q ⟶
Spec (CommRingCat.of (Localization.AtPrime (prime φ)))The original stage fiber maps canonically to the localized stage.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)
variable {P X : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of B))def fiberToLocalized : pullback q (stageResidueSpec φ) ⟶ localizedScheme φ qLocalization preserves the actual residue fiber.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)
variable {P X : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of B))lemma fiber_isPullback : IsPullback (fiberToLocalized φ q)
(pullback.snd q (stageResidueSpec φ)) (localizedBaseMap φ q) (residueSpec φ)The original scheme maps to the actual localized stage.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)
variable {P X : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of B))
variable (f : X ⟶ Spec (CommRingCat.of A)) (t : X ⟶ P)
variable (w : t ≫ q = f ≫ Spec.map (CommRingCat.ofHom φ))def lift : X ⟶ localizedScheme φ qThe original closed fiber maps to the actual stage residue fiber.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)
variable {P X : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of B))
variable (f : X ⟶ Spec (CommRingCat.of A)) (t : X ⟶ P)
variable (w : t ≫ q = f ≫ Spec.map (CommRingCat.ofHom φ))def topFiberMap : pullback f (topResidueSpec (A := A)) ⟶
pullback q (stageResidueSpec φ)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.LocalStageResidue
universe u
variable {B A : Type u} [CommRing B] [CommRing A] [IsLocalRing A]
variable (φ : B →+* A)
variable {P X : Scheme.{u}} (q : P ⟶ Spec (CommRingCat.of B))
variable (f : X ⟶ Spec (CommRingCat.of A)) (t : X ⟶ P)
variable (w : t ≫ q = f ≫ Spec.map (CommRingCat.ofHom φ))lemma topFiberMap_toLocalized :
topFiberMap φ q f t w ≫ fiberToLocalized φ q =
pullback.fst f (topResidueSpec (A := A)) ≫ lift φ q f t w