Colimits of algebras with a fixed residue ring

Fix an ideal I of a commutative ring R. If the canonical maps R / I → B / IB are isomorphisms for every algebra in a diagram, the same holds for its colimit. No filteredness or nonemptiness assumption on the diagram is needed. This gives the residue-ring identification in constructions by colimits of étale neighbourhoods.

Use I.bijective_algebraMap_quotient_colimit D hD for bijectivity and I.quotientColimitEquiv D hD for the corresponding algebra equivalence, where hD gives bijectivity of the canonical residue map at each object of D.

The proof constructs compatible residue maps to R / I and descends them through the colimit. Maps into an algebra annihilated by I are unique whenever R / I → B / IB is surjective.

References

• Stacks Project, Tag 0A02, the residue-ring identification in the construction of the henselization of a pair.

theorem Ideal.bijective_algebraMap_quotient_colimit {R : Type u} [CommRing R] (I : Ideal R) {J : Type v} [CategoryTheory.Category.{t, v} J] (D : CategoryTheory.Functor J (CommAlgCat R)) [CategoryTheory.Limits.HasColimit D] (hD : ∀ (j : J), Function.Bijective ⇑(algebraMap (R ⧸ I) (↑(D.obj j) ⧸ map (algebraMap R ↑(D.obj j)) I))) : Function.Bijective ⇑(algebraMap (R ⧸ I) (↑(CategoryTheory.Limits.colimit D) ⧸ map (algebraMap R ↑(CategoryTheory.Limits.colimit D)) I))

Colimits preserve the property that the canonical residue-algebra map is bijective.

noncomputable def Ideal.quotientColimitEquiv {R : Type u} [CommRing R] (I : Ideal R) {J : Type v} [CategoryTheory.Category.{t, v} J] (D : CategoryTheory.Functor J (CommAlgCat R)) [CategoryTheory.Limits.HasColimit D] (hD : ∀ (j : J), Function.Bijective ⇑(algebraMap (R ⧸ I) (↑(D.obj j) ⧸ map (algebraMap R ↑(D.obj j)) I))) : (R ⧸ I) ≃ₐ[R] ↑(CategoryTheory.Limits.colimit D) ⧸ map (algebraMap R ↑(CategoryTheory.Limits.colimit D)) I

The canonical residue-algebra equivalence for a colimit of algebras with residue ring R / I.

@[simp]

theorem Ideal.quotientColimitEquiv_toAlgHom {R : Type u} [CommRing R] (I : Ideal R) {J : Type v} [CategoryTheory.Category.{t, v} J] (D : CategoryTheory.Functor J (CommAlgCat R)) [CategoryTheory.Limits.HasColimit D] (hD : ∀ (j : J), Function.Bijective ⇑(algebraMap (R ⧸ I) (↑(D.obj j) ⧸ map (algebraMap R ↑(D.obj j)) I))) : ↑(I.quotientColimitEquiv D hD) = IsScalarTower.toAlgHom R (R ⧸ I) (↑(CategoryTheory.Limits.colimit D) ⧸ map (algebraMap R ↑(CategoryTheory.Limits.colimit D)) I)

The forward colimit residue equivalence is the canonical residue-algebra map.

@[simp]

theorem Ideal.quotientColimitEquiv_mk {R : Type u} [CommRing R] (I : Ideal R) {J : Type v} [CategoryTheory.Category.{t, v} J] (D : CategoryTheory.Functor J (CommAlgCat R)) [CategoryTheory.Limits.HasColimit D] (hD : ∀ (j : J), Function.Bijective ⇑(algebraMap (R ⧸ I) (↑(D.obj j) ⧸ map (algebraMap R ↑(D.obj j)) I))) (r : R) : (I.quotientColimitEquiv D hD) ((Quotient.mk I) r) = (Quotient.mk (map (algebraMap R ↑(CategoryTheory.Limits.colimit D)) I)) ((algebraMap R ↑(CategoryTheory.Limits.colimit D)) r)

The colimit residue equivalence is the structure map on representatives.

@[simp]

theorem Ideal.quotientColimitEquiv_symm_mk_ι {R : Type u} [CommRing R] (I : Ideal R) {J : Type v} [CategoryTheory.Category.{t, v} J] (D : CategoryTheory.Functor J (CommAlgCat R)) [CategoryTheory.Limits.HasColimit D] (hD : ∀ (j : J), Function.Bijective ⇑(algebraMap (R ⧸ I) (↑(D.obj j) ⧸ map (algebraMap R ↑(D.obj j)) I))) (j : J) (b : ↑(D.obj j)) : (I.quotientColimitEquiv D hD).symm ((Quotient.mk (map (algebraMap R ↑(CategoryTheory.Limits.colimit D)) I)) ((CommAlgCat.Hom.hom (CategoryTheory.Limits.colimit.ι D j)) b)) = (AlgEquiv.ofBijective (IsScalarTower.toAlgHom R (R ⧸ I) (↑(D.obj j) ⧸ map (algebraMap R ↑(D.obj j)) I)) ⋯).symm ((Quotient.mk (map (algebraMap R ↑(D.obj j)) I)) b)

The inverse colimit residue equivalence agrees with the inverse residue equivalence at each stage.