loopOfHom_eq_id — Mathlib

English

Proofs of loop identity use unique_path_root and equivalences; ultimately loops reduce to identity.

Русский

Доказательства идентичности петель используют уникальные корни путей и эквивалентности; петли сходятся к тождеству.

LaTeX

$$loop_of_hom_id$$

Lean4

/-- Turning an edge in the spanning tree into a loop gives the identity loop. -/
theorem loopOfHom_eq_id {a b : Generators G} (e) (H : e ∈ wideSubquiverSymmetrify T a b) :
    loopOfHom T (of e) = 𝟙 (root' T) :=
  by
  rw [loopOfHom, ← Category.assoc, IsIso.comp_inv_eq, Category.id_comp]
  rcases H with H | H
  · rw [treeHom_eq T (Path.cons default ⟨Sum.inl e, H⟩), homOfPath]
    rfl
  · rw [treeHom_eq T (Path.cons default ⟨Sum.inr e, H⟩), homOfPath]
    simp only [IsIso.inv_hom_id, Category.comp_id, Category.assoc, treeHom]

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