Base change of completed rational localisations to a quotient ring

Let J be an ideal of a ring A with a pair of definition P, and write q : A → A ⧸ J for the quotient map. For a presentation p = (T, s) of A, the base change

A⟨T/s⟩ → (A ⧸ J)⟨q(T)/q(s)⟩

of q (Presentation.mapHom) is the completion of the localised quotient map, which is an open quotient map. So the rational localisation of A ⧸ J is a quotient of that of A.

Main results

• TauCeti.Huber.PairOfDefinition.Presentation.mapHom_quotientMk_surjective: the base change A⟨T/s⟩ → (A ⧸ J)⟨q(T)/q(s)⟩ is surjective.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Proposition 7.38.

theorem TauCeti.Huber.PairOfDefinition.Presentation.mapHom_quotientMk_surjective {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] {P : PairOfDefinition A} (J : Ideal A) [DecidableEq (A ⧸ J)] (p : P.Presentation) (q : (P.quotient J).Presentation) (hnum : q.num = Finset.image (⇑(Ideal.Quotient.mk J)) p.num) (hden : q.den = (Ideal.Quotient.mk J) p.den) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (mapHom (Ideal.Quotient.mk J) ⋯ p q hden ⋯).hom)

The rational localisation of A ⧸ J is a quotient of that of A: for a presentation p = (T, s) of A and the presentation q = (q(T), q(s)) of A ⧸ J, the base change A⟨p⟩ → (A ⧸ J)⟨q⟩ of the quotient map is surjective.