cancel_iso_inv_right — Mathlib

English

Let f, f' : X → Y and g : Z ≅ Y. Then f ≫ g.inv = f' ≫ g.inv iff f = f'.

Русский

Пусть f, f' : X → Y и g : Z ≅ Y. Тогда f ≫ g.inv = f' ≫ g.inv тогда и только тогда, когда f = f'.

LaTeX

$$$f \\circ g^{-1} = f' \\circ g^{-1} \\iff f = f'$$$

Lean4

@[simp]
theorem cancel_iso_inv_right {X Y Z : C} (f f' : X ⟶ Y) (g : Z ≅ Y) : f ≫ g.inv = f' ≫ g.inv ↔ f = f' := by
  simp only [cancel_mono]
    /-
    Unfortunately cancelling an isomorphism from the right of a chain of compositions is awkward.
    We would need separate lemmas for each chain length (worse: for each pair of chain lengths).

    We provide two more lemmas, for case of three morphisms, because this actually comes up in practice,
    but then stop.
    -/

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