endIsFree — Mathlib

English

The endomorphism group at the root of a free connected groupoid is a free group; more precisely, End(root' T) is a free group generated by loops corresponding to the arrows not in the spanning tree.

Русский

Группа концевых переходов в корневой вершине свободного связного группоидa является свободной; End(root' T) свободна и порождается петлями, соответствующими рёбрам, выходящим за пределы дерева.

LaTeX

$$$$\operatorname{IsFreeGroup}(\operatorname{End}(\mathrm{root}'(T))).$$$$

Lean4

/-- Given a free groupoid and an arborescence of its generating quiver, the vertex
group at the root is freely generated by loops coming from generating arrows
in the complement of the tree. -/
theorem endIsFree : IsFreeGroup (End (root' T)) :=
  IsFreeGroup.ofUniqueLift ((wideSubquiverEquivSetTotal <| wideSubquiverSymmetrify T)ᶜ : Set _)
    (fun e => loopOfHom T (of e.val.hom))
    (by
      intro X _ f
      let f' : Labelling (Generators G) X := fun a b e =>
        if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨⟨a, b, e⟩, h⟩
      rcases unique_lift f' with ⟨F', hF', uF'⟩
      refine ⟨F'.mapEnd _, ?_, ?_⟩
      · suffices ∀ {x y} (q : x ⟶ y), F'.map (loopOfHom T q) = (F'.map q : X)
          by
          rintro
            ⟨⟨a, b, e⟩, h⟩
                -- Work around the defeq `X = End (F'.obj (IsFreeGroupoid.SpanningTree.root' T))`

          erw [Functor.mapEnd_apply]
          rw [this, hF']
          exact dif_neg h
        intro x y q
        suffices ∀ {a} (p : Path (root T) a), F'.map (homOfPath T p) = 1 by
          simp only [this, treeHom, comp_as_mul, inv_as_inv, loopOfHom, inv_one, mul_one, one_mul, Functor.map_inv,
            Functor.map_comp]
        intro a p
        induction p with
        | nil => rw [homOfPath, F'.map_id, id_as_one]
        | cons p e ih =>
          rw [homOfPath, F'.map_comp, comp_as_mul, ih, mul_one]
          rcases e with ⟨e | e, eT⟩
          · rw [hF']
            exact dif_pos (Or.inl eT)
          · rw [F'.map_inv, inv_as_inv, inv_eq_one, hF']
            exact dif_pos (Or.inr eT)
      · intro E hE
        ext x
        suffices (functorOfMonoidHom T E).map x = F'.map x by
          simpa only [loopOfHom, functorOfMonoidHom, IsIso.inv_id, treeHom_root, Category.id_comp,
            Category.comp_id] using this
        congr
        apply uF'
        intro a b e
        change E (loopOfHom T _) = dite _ _ _
        split_ifs with h
        · rw [loopOfHom_eq_id T e h, ← End.one_def, E.map_one]
        · exact hE ⟨⟨a, b, e⟩, h⟩)

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