English
Reversal preserves the Quotient.CompClosure relation: if p is related to q, then p.reverse is related to q.reverse.
Русский
Разворот сохраняет отношение в отношении Quotient.CompClosure: если p связано с q, то p.reverse связано с q.reverse.
LaTeX
$$Quotient.CompClosure redStep p q → Quotient.CompClosure redStep p.reverse q.reverse$$
Lean4
theorem congr_reverse {X Y : Paths <| Quiver.Symmetrify V} (p q : X ⟶ Y) :
Quotient.CompClosure redStep p q → Quotient.CompClosure redStep p.reverse q.reverse :=
by
rintro ⟨XW, pp, qq, WY, _, Z, f⟩
have :
Quotient.CompClosure redStep (WY.reverse ≫ 𝟙 _ ≫ XW.reverse)
(WY.reverse ≫ (f.toPath ≫ (Quiver.reverse f).toPath) ≫ XW.reverse) :=
by
constructor
constructor
simpa only [CategoryStruct.comp, CategoryStruct.id, Quiver.Path.reverse, Quiver.Path.nil_comp,
Quiver.Path.reverse_comp, Quiver.reverse_reverse, Quiver.Path.reverse_toPath, Quiver.Path.comp_assoc] using this
