Commit 2024-10-04 10:12 12bdcfbb

feat(RingTheory): target local closure of property of ring homomorphisms (#17032) If P is a property of ring homomorphisms, we call Locally P the closure of P with respect to standard open coverings on the (algebraic) target (i.e. geometric source). Hence for f : R →+* S, the property Locally P holds if it holds locally on S, i.e. if there exists a subset { t } of S generating the unit ideal, such that P holds for all compositions R →+* Sₜ. By construction, Locally P is local on the target. Moreover, stability properties of P are inherited by Locally P (TODO).