congr_reverse_comp — Mathlib

English

Similarly, the reverse composition p ≫ p.reverse is equivalent to the identity in the quotient.

Русский

Аналогично, развёрнутая композиция p.reverse ≫ p эквивалентна тождественному морфизму в фактор-пространстве.

LaTeX

$$Quot.mk (CompClosure redStep) (p.reverse ≫ p) = Quot.mk (CompClosure redStep) (id_Y)$$

Lean4

theorem congr_reverse_comp {X Y : Paths <| Quiver.Symmetrify V} (p : X ⟶ Y) :
    Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (p.reverse ≫ p) =
      Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (𝟙 Y) :=
  by
  nth_rw 2 [← Quiver.Path.reverse_reverse p]
  apply congr_comp_reverse

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