English
Variant of arrow-mk-iso-iff for ring-hom properties: equivalent statements for morphisms in CommRingCat under isomorphism.
Русский
Вариант равносильности для стрелок-изоморфизмов в отношении свойств гомоморфизмов колец.
LaTeX
$$$\forall e:\text{Arrow.mk f} \cong \text{Arrow.mk g},\ P(f) \Leftrightarrow P(g).$$$
Lean4
/-- Variant of `MorphismProperty.arrow_mk_iso_iff` specialized to morphism properties in
`CommRingCat` given by ring hom properties. -/
theorem arrow_mk_iso_iff (hQ : RingHom.RespectsIso P) {A B A' B' : CommRingCat} {f : A ⟶ B} {g : A' ⟶ B'}
(e : Arrow.mk f ≅ Arrow.mk g) : P f.hom ↔ P g.hom :=
by
have : (toMorphismProperty P).RespectsIso := by rwa [← toMorphismProperty_respectsIso_iff]
change toMorphismProperty P _ ↔ toMorphismProperty P _
rw [MorphismProperty.arrow_mk_iso_iff (toMorphismProperty P) e]
