Theorems · Theorem · commutative algebra

RingHom.HoldsForLocalization.isLocalizationMap

∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S]
  {P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P) →
      (RingHom.HoldsForLocalization fun {R S} [CommRing R] [CommRing S] => P) →
        ∀ {M : Submonoid R} {T : Submonoid S} {R' : Type u} [inst_2 : CommRing R'] [inst_3 : Algebra R R']
          [inst_4 : IsLocalization M R'] (S' : Type u) [inst_5 : CommRing S'] [inst_6 : Algebra S S']
          [inst_7 : IsLocalization T S'] {f : R →+* S} (hy : M ≤ Submonoid.comap f T),
          P f → P (IsLocalization.map S' f hy)

Defined in

Mathlib.RingTheory.LocalProperties.Basic

Cited by

1 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingCommRingAlgebraIsLocalizationCommRingAlgebraIsLocalization