isoClosure_respectsIso — Mathlib

English

For any C, P.isoClosure has the RespectsIso property.

Русский

Для любой категории C, P.isoClosure обладает свойством RespectsIso.

LaTeX

$$$P.isoClosure.RespectsIso$$$

Lean4

instance isoClosure_respectsIso (P : MorphismProperty C) : RespectsIso P.isoClosure
    where
  precomp := fun e (he : IsIso e) f ⟨_, _, f', hf', ⟨iso⟩⟩ =>
    ⟨_, _, f', hf', ⟨Arrow.isoMk (asIso iso.hom.left ≪≫ asIso (inv e)) (asIso iso.hom.right) (by simp)⟩⟩
  postcomp := fun e (he : IsIso e) f ⟨_, _, f', hf', ⟨iso⟩⟩ =>
    ⟨_, _, f', hf', ⟨Arrow.isoMk (asIso iso.hom.left) (asIso iso.hom.right ≪≫ asIso e) (by simp)⟩⟩

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