endIsFreeOfConnectedFree — 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.

Русский

Группа эндоморфизмов корня свободного связного группооида является свободной; End(root' T) свободна.

LaTeX

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

Lean4

/-- A vertex group in a free connected groupoid is free. With some work one could drop the
connectedness assumption, by looking at connected components. -/
instance endIsFreeOfConnectedFree {G : Type u} [Groupoid G] [IsConnected G] [IsFreeGroupoid G] (r : G) :
    IsFreeGroup.{u} (End r) :=
  SpanningTree.endIsFree <| geodesicSubtree (symgen r)

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