Derivations preserving localizations

An ambient derivation that maps a domain into itself also maps every prime localization into itself. The statement deliberately does not require an algebra structure from the derivation's constant ring to the localized ring; that structure need not exist in the Frobenius-constant application.

theorem BGS.CorvajaZannier.ambientDerivation_preserves_localizationAtPrime_of_preserves {C : Type u_1} {R : Type u_2} {U : Type u_3} [CommRing C] [CommRing R] [IsDomain R] [Field U] [Algebra C U] [Algebra R U] [IsFractionRing R U] (q : Ideal R) [q.IsPrime] [Algebra (Localization.AtPrime q) U] [IsScalarTower R (Localization.AtPrime q) U] (E : Derivation C U U) (hE : ∀ (r : R), ∃ (r' : R), E ((algebraMap R U) r) = (algebraMap R U) r') (z : Localization.AtPrime q) : ∃ (z' : Localization.AtPrime q), E ((algebraMap (Localization.AtPrime q) U) z) = (algebraMap (Localization.AtPrime q) U) z'

An ambient derivation which preserves a domain also preserves each of its localizations at a prime. This is the quotient-rule bridge from a global different-annihilator certificate to the local DVR Wronskian bounds.