congr_comp_reverse — Mathlib

English

A consequence of reversal compatibility: composing p with its reverse is equivalent to the identity in the quotient.

Русский

Следствие совместимости разворота: композиция p с p.reverse эквивалентна тождественному морфизмy в фактор-пространстве.

LaTeX

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

Lean4

theorem congr_comp_reverse {X Y : Paths <| Quiver.Symmetrify V} (p : X ⟶ Y) :
    Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (p ≫ p.reverse) =
      Quot.mk (@Quotient.CompClosure _ _ redStep _ _) (𝟙 X) :=
  by
  apply Quot.eqvGen_sound
  induction p with
  | nil => apply EqvGen.refl
  | cons q f ih =>
    simp only [Quiver.Path.reverse]
    fapply EqvGen.trans
    · exact q ≫ Quiver.Path.reverse q
    · apply EqvGen.symm
      apply EqvGen.rel
      have :
        Quotient.CompClosure redStep (q ≫ 𝟙 _ ≫ Quiver.Path.reverse q)
          (q ≫ (Quiver.Hom.toPath f ≫ Quiver.Hom.toPath (Quiver.reverse f)) ≫ Quiver.Path.reverse q) :=
        by
        apply Quotient.CompClosure.intro
        apply redStep.step
      simp only [Category.assoc,
        Category.id_comp] at this
          ⊢
            -- Porting note: `simp` cannot see how `Quiver.Path.comp_assoc` is relevant, so change to
                  -- category notation

      change
        Quotient.CompClosure redStep (q ≫ Quiver.Path.reverse q)
          (Quiver.Path.cons q f ≫ (Quiver.Hom.toPath (Quiver.reverse f)) ≫ (Quiver.Path.reverse q))
      simp only [← Category.assoc] at this ⊢
      exact this
    · exact ih

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