SchemeTheory.primeLocalization_commuting_square
A commuting square of actual coefficient maps remains commuting after localization at the preserved primes. This uses only the existing localRingHom construction and does not install any group action on either ring.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace SchemeTheory
universe u vLean source · statement
theorem primeLocalization_commuting_square
{A : Type u} {B : Type v} [CommRing A] [CommRing B]
(P : Ideal A) [P.IsPrime] (Q : Ideal B) [Q.IsPrime]
(f : A →+* B) (s : A →+* A) (t : B →+* B)
(hf : P = Q.comap f) (hs : P = P.comap s) (ht : Q = Q.comap t)
(hcomm : f.comp s = t.comp f) :
(Localization.localRingHom P Q f hf).comp (Localization.localRingHom P P s hs) =
(Localization.localRingHom Q Q t ht).comp (Localization.localRingHom P Q f hf)