English
An action groupoid over a free group is free; the spanning tree yields a canonical loop relations identity.
Русский
Группо-диграфия действия над свободной группой свободна; дерево покрытий задаёт канонические петли, являющиеся тождественными.
LaTeX
$$IsFreeGroupoid(ActionCategory G A) is free$$
Lean4
/-- An action groupoid over a free group is free. More generally, one could show that the groupoid
of elements over a free groupoid is free, but this version is easier to prove and suffices for our
purposes.
Analogous to the fact that a covering space of a graph is a graph. (A free groupoid is like a graph,
and a groupoid of elements is like a covering space.) -/
instance actionGroupoidIsFree {G A : Type u} [Group G] [IsFreeGroup G] [MulAction G A] :
IsFreeGroupoid (ActionCategory G A)
where
quiverGenerators := ⟨fun a b => { e : IsFreeGroup.Generators G // IsFreeGroup.of e • a.back = b.back }⟩
of := fun (e : Subtype _) => ⟨IsFreeGroup.of e, e.property⟩
unique_lift := by
intro X _ f
let f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e =>
⟨fun b => @f ⟨(), _⟩ ⟨(), b⟩ ⟨e, smul_inv_smul _ b⟩, IsFreeGroup.of e⟩
rcases IsFreeGroup.unique_lift f' with ⟨F', hF', uF'⟩
refine ⟨uncurry F' ?_, ?_, ?_⟩
· suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id _ by exact DFunLike.ext_iff.mp this
apply IsFreeGroup.ext_hom (fun x ↦ ?_)
rw [MonoidHom.comp_apply, hF']
rfl
· rintro ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b⟩ ⟨e, h : IsFreeGroup.of e • a = b⟩
change (F' (IsFreeGroup.of _)).left _ = _
rw [hF']
cases inv_smul_eq_iff.mpr h.symm
rfl
· intro E hE
have : curry E = F' := by
apply uF'
intro e
ext
· convert hE _ _ _
rfl
· rfl
apply Functor.hext
· intro
apply Unit.ext
· refine ActionCategory.cases ?_
intros
simp only [← this, uncurry_map, curry_apply_left, coe_back, homOfPair.val]
rfl
