Target local closure of ring homomorphism properties #
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ₜ
.
Assuming without further mention that P
is stable under composition with isomorphisms,
Locally P
is local on the target by construction, i.e. it satisfies
OfLocalizationSpanTarget
. If P
itself is local on the target, Locally P
coincides with P
.
The Locally
construction preserves various properties of P
, e.g. if P
is stable under
composition, base change, etc., so is Locally P
.
Main results #
RingHom.locally_ofLocalizationSpanTarget
:Locally P
is local on the target.RingHom.locally_holdsForLocalizationAway
:Locally P
holds for localization away maps ifP
does.RingHom.locally_isStableUnderBaseChange
:Locally P
is stable under base change ifP
is.RingHom.locally_stableUnderComposition
:Locally P
is stable under composition ifP
is andP
is preserved under localizations.RingHom.locally_stableUnderCompositionWithLocalizationAway
:Locally P
is stable under composition with localization away maps ifP
is.RingHom.locally_localizationPreserves
: IfP
is preserved by localizations, then so isLocally P
.
For a property of ring homomorphisms P
, Locally P
holds for f : R →+* S
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ₜ
.
We may require s
to be finite here, for the equivalence, see locally_iff_finite
.
Equations
- RingHom.Locally P f = ∃ (s : Set S) (_ : Ideal.span s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
Instances For
If P
respects isomorphisms, to check P
holds locally for f : R →+* S
, it suffices
to check P
holds on a standard open cover.
Equivalence variant of locally_of_exists
. This is sometimes easier to use, if the
IsLocalization.Away
instance can't be automatically inferred.
In the definition of Locally
we may replace Localization.Away
with an arbitrary
algebra satisfying IsLocalization.Away
.
If f
satisfies P
, then in particular it satisfies Locally P
.
If P
is local on the target, then Locally P
coincides with P
.
Locally P
is local on the target.
If P
respects isomorphism, so does Locally P
.
If P
holds for localization away maps, then so does Locally P
.
If P
preserves localizations, then Locally P
is stable under composition if P
is.
If P
is stable under composition with localization away maps on the right,
then so is Locally P
.
If P
is stable under composition with localization away maps on the left,
then so is Locally P
.
If P
is stable under base change, then so is Locally P
.
If P
is preserved by localization away, then so is Locally P
.
If P
is preserved by localizations, then so is Locally P
.
If P
is preserved by localizations and stable under composition with localization
away maps, then Locally P
is a local property of ring homomorphisms.