cancel_right_of_respectsIso — Mathlib

English

If P respects iso, then P(f ≫ g) is equivalent to P f when g is an isomorphism.

Русский

Если P сохраняет изоморфизм, то P(f ≫ g) эквивалентно P(f) когда g — изоморфизм.

LaTeX

$$$P(f \gg g) \iff P(f)$ при $g$ изоморфизм$$

Lean4

theorem cancel_right_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
    [IsIso g] : P (f ≫ g) ↔ P f :=
  ⟨fun h => by simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h, RespectsIso.postcomp P g f⟩

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