inverseImage — Mathlib

English

If P respects iso, then the inverse image construction under F respects iso as well.

Русский

Если P сохраняет изоморфизмы, то обратное изображение под F тоже сохраняет их.

LaTeX

$$$\\mathrm{RespectsIso}(P) \\Rightarrow \\mathrm{RespectsIso}(P^{-1}\\!\\text{image}\\ F)$$$

Lean4

instance inverseImage (P : MorphismProperty D) [RespectsIso P] (F : C ⥤ D) : RespectsIso (P.inverseImage F)
    where
  precomp {X Y Z} e (he : IsIso e) f hf := by simpa [MorphismProperty.inverseImage, cancel_left_of_respectsIso] using hf
  postcomp {X Y Z} e (he : IsIso e) f
    hf := by simpa [MorphismProperty.inverseImage, cancel_right_of_respectsIso] using hf

Похожие утверждения