Theorems · Theorem · commutative algebra

RingHom.RespectsIso.arrow_mk_iso_iff

∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    ∀ {A B A' B' : CommRingCat} {f : A ⟶ B} {g : A' ⟶ B'} (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g),
      P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)

Variant of MorphismProperty.arrow_mk_iso_iff specialized to morphism properties in CommRingCat given by ring hom properties.

Defined in

Mathlib.RingTheory.RingHomProperties

Cited by

6 results in Mathlib

Foundations

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