English
Equivalence between respecting iso for P and for its associated morphism-property.
Русский
Эквивалентность между сохранением изоморфизмов для P и для связанного с ним морфизм-свойства.
LaTeX
$$$\text{RespectsIso}(P) \iff (\text{toMorphismProperty }P).\text{RespectsIso}$$$
Lean4
theorem toMorphismProperty_respectsIso_iff : RespectsIso P ↔ (toMorphismProperty P).RespectsIso :=
by
refine ⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩
· intro X Y Z e f hf
exact h.right f.hom e.commRingCatIsoToRingEquiv hf
· intro X Y Z e f hf
exact h.left f.hom e.commRingCatIsoToRingEquiv hf
· intro X Y Z _ _ _ f e hf
exact MorphismProperty.RespectsIso.postcomp (toMorphismProperty P) e.toCommRingCatIso.hom (CommRingCat.ofHom f) hf
· intro X Y Z _ _ _ f e
exact MorphismProperty.RespectsIso.precomp (toMorphismProperty P) e.toCommRingCatIso.hom (CommRingCat.ofHom f)
