Transporting local flatness across ring isomorphisms

A commutative square whose horizontal maps are isomorphisms transports flatness after localizing the target at corresponding primes. This lets symmetry arguments reduce flatness of a morphism to flatness at one point.

theorem RingHom.flat_localization_comap_iff {R : Type u_1} {S : Type u_2} {R' : Type u_3} {S' : Type u_4} [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] (f : R →+* S) (g : R' →+* S') (eR : R ≃+* R') (eS : S ≃+* S') (h : eS.toRingHom.comp f = g.comp eR.toRingHom) (p : Ideal S') [p.IsPrime] : ((algebraMap S (Localization.AtPrime (Ideal.comap eS p))).comp f).Flat ↔ ((algebraMap S' (Localization.AtPrime p)).comp g).Flat

A square of ring maps with isomorphic source and target preserves flatness after localizing the target at corresponding prime ideals.