Documentation

Mathlib.RingTheory.RingHom.Locally

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 #

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

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
Instances For
    theorem RingHom.locally_iff_finite (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop) {R 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 = ), ts, 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 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 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 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 = ), ts, ∀ (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 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 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_StableUnderCompositionWithLocalizationAwayTarget {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hP0 : RingHom.RespectsIso fun {R S : Type u} [CommRing R] [CommRing S] => P) (hPa : RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S : Type u} [CommRing R] [CommRing S] => P) :

    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.

    theorem RingHom.locally_isStableUnderBaseChange {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.IsStableUnderBaseChange fun {R S : Type u} [CommRing R] [CommRing S] => P) :
    RingHom.IsStableUnderBaseChange 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_localizationAwayPreserves {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S)Prop} (hPl : RingHom.LocalizationAwayPreserves fun {R S : Type u} [CommRing R] [CommRing S] => P) :
    RingHom.LocalizationAwayPreserves 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 localization away, then so is Locally P.

    theorem RingHom.locally_localizationPreserves {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) :
    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.LocalizationAwayPreserves 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.