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 if P does.
• RingHom.locally_stableUnderBaseChange: Locally P is stable under base change if P is.
• RingHom.locally_stableUnderComposition: Locally P is stable under composition if P is and P is preserved under localizations.
• RingHom.locally_stableUnderCompositionWithLocalizationAway: Locally P is stable under composition with localization away maps if P is.
• RingHom.locally_localizationPreserves: If P is preserved by localizations, then so is Locally P.

def RingHom.Locally (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {R : Type u} {S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : Prop

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)

theorem RingHom.locally_iff_finite (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) {R : Type u} {S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => P) f ↔ ∃ (s : Finset S) (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

theorem RingHom.locally_of_exists {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {R : Type u} {S : Type u} [CommRing R] [CommRing S] (hP : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (f : R →+* S) {ι : Type u_1} (s : ι → S) (hsone : Ideal.span (Set.range s) = ⊤) (Sₜ : ι → Type u) [(i : ι) → CommRing (Sₜ i)] [(i : ι) → Algebra S (Sₜ i)] [∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)] (hf : ∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)) : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => P) f

If P respects isomorphisms, to check P holds locally for f : R →+* S, it suffices to check P holds on a standard open cover.

theorem RingHom.locally_iff_exists {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {R : Type u} {S : Type u} [CommRing R] [CommRing S] (hP : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (f : R →+* S) : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => P) f ↔ ∃ (ι : Type u) (s : ι → S) (_ : Ideal.span (Set.range s) = ⊤) (Sₜ : ι → Type u) (x : (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra S (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)), ∀ (i : ι), P ((algebraMap S (Sₜ i)).comp f)

Equivalence variant of locally_of_exists. This is sometimes easier to use, if the IsLocalization.Away instance can't be automatically inferred.

theorem RingHom.locally_iff_isLocalization {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {R : Type u} {S : Type u} [CommRing R] [CommRing S] (hP : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (f : R →+* S) : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => P) f ↔ ∃ (s : Finset S) (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [inst_2 : IsLocalization.Away t Sₜ], P ((algebraMap S Sₜ).comp f)

In the definition of Locally we may replace Localization.Away with an arbitrary algebra satisfying IsLocalization.Away.

theorem RingHom.locally_of {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {R : Type u} {S : Type u} [CommRing R] [CommRing S] (hP : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (f : R →+* S) (hf : P f) : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => P) f

If f satisfies P, then in particular it satisfies Locally P.

theorem RingHom.locally_iff_of_localizationSpanTarget {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPs : RingHom.OfLocalizationSpanTarget fun {R S : Type u} [CommRing R] [CommRing S] => P) {R : Type u} {S : Type u} [CommRing R] [CommRing S] (f : R →+* S) : RingHom.Locally (fun {R S : Type u} [CommRing R] [CommRing S] => P) f ↔ P f

If P is local on the target, then Locally P coincides with P.

theorem RingHom.locally_ofLocalizationSpanTarget {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hP : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.OfLocalizationSpanTarget fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => P

Locally P is local on the target.

theorem RingHom.locally_respectsIso {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => P

If P respects isomorphism, so does Locally P.

theorem RingHom.locally_holdsForLocalizationAway {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPa : RingHom.HoldsForLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.HoldsForLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => P

If P holds for localization away maps, then so does Locally P.

theorem RingHom.locally_stableUnderComposition {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPl : RingHom.LocalizationPreserves fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPc : RingHom.StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.StableUnderComposition fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => P

If P preserves localizations, then Locally P is stable under composition if P is.

theorem RingHom.locally_stableUnderCompositionWithLocalizationAway {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPa : RingHom.StableUnderCompositionWithLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.StableUnderCompositionWithLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => P

If P is stable under composition with localization away maps, then so is Locally P.

theorem RingHom.locally_stableUnderBaseChange {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPb : RingHom.StableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.StableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => P

If P is stable under base change, then so is Locally P.

theorem RingHom.locally_localizationPreserves {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPi : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPl : RingHom.LocalizationPreserves fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.LocalizationPreserves fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => P

If P is preserved by localizations, then so is Locally P.

theorem RingHom.locally_propertyIsLocal {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} (hPl : RingHom.LocalizationPreserves fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPa : RingHom.StableUnderCompositionWithLocalizationAway fun {R S : Type u} [CommRing R] [CommRing S] => P) : RingHom.PropertyIsLocal fun {R S : Type u} [CommRing R] [CommRing S] => RingHom.Locally fun {R S : Type u} [CommRing R] [CommRing S] => 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.