IsFreeGroupoid.SpanningTree.endIsFree
theorem IsFreeGroupoid.SpanningTree.endIsFree :
∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
(T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
[inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)],
IsFreeGroup (CategoryTheory.End (IsFreeGroupoid.SpanningTree.root' T))
The theorem `IsFreeGroupoid.SpanningTree.endIsFree` states that for any free groupoid `G` and an arborescence of the symmetrized generating quiver of `G`, the vertex group at the root of this arborescence is freely generated by loops which originate from generating arrows that are not part of the tree. In other words, the endomorphisms of the root vertex of the tree in the free groupoid form a free group, with the generators being loops from non-tree generating arrows.
More concisely: The endomorphisms of the root vertex in a free groupoid form a free group, generated by loops from non-tree generating arrows.
|
IsFreeGroupoid.path_nonempty_of_hom
theorem IsFreeGroupoid.path_nonempty_of_hom :
∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G] {a b : G},
Nonempty (a ⟶ b) → Nonempty (Quiver.Path (IsFreeGroupoid.symgen a) (IsFreeGroupoid.symgen b))
This theorem states that for any type `G` that has the structure of a groupoid and is a free groupoid, if there exists a morphism from `a` to `b` (denoted `a ⟶ b`), then there must exist a so-called "zigzag" path (also known as a Quiver path) in the generating quiver from `a` to `b`. In other words, if there's a way to morph `a` into `b` in the groupoid, then there's also a way to get from `a` to `b` via a sequence of steps in the underlying quiver (a kind of directed graph), where each step could be either forward in the direction of an arrow or backward against it.
More concisely: For any free groupoid `G` with type `G` and a morphism `a ⟶ b`, there exists a zigzag path from `a` to `b` in the generating quiver of `G`.
|
IsFreeGroupoid.ext_functor
theorem IsFreeGroupoid.ext_functor :
∀ {G : Type u_1} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G] {X : Type v} [inst_2 : Group X]
(f g : CategoryTheory.Functor G (CategoryTheory.SingleObj X)),
(∀ (a b : IsFreeGroupoid.Generators G) (e : a ⟶ b), f.map (IsFreeGroupoid.of e) = g.map (IsFreeGroupoid.of e)) →
f = g
The theorem `IsFreeGroupoid.ext_functor` states that for any type `G` that has a structure of a free groupoid and any group `X`, if we have two functors `f` and `g` from `G` to the single-object category associated with `X`, then these two functors are equal if they agree on the generating quiver of `G`. In other words, for every pair of generators `a` and `b` in `G`, and for every morphism `e` from `a` to `b`, if the image of `e` under `f` is the same as the image of `e` under `g`, then `f` and `g` are the same functor.
More concisely: If two functors from a free groupoid to a single-object category agree on their images of generating morphisms, then they are equal.
|
IsFreeGroupoid.SpanningTree.loopOfHom_eq_id
theorem IsFreeGroupoid.SpanningTree.loopOfHom_eq_id :
∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
(T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
[inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)]
{a b : IsFreeGroupoid.Generators G},
∀ e ∈ Quiver.wideSubquiverSymmetrify T a b,
IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e) =
CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root' T)
This theorem states that for any groupoid `G` that is free, given a wide subquiver `T` of the symmetrized generators of `G` that forms an arborescence (a directed, rooted tree), any edge `e` in the symmetrized wide subquiver `T` that connects two generators `a` and `b` of `G` will, when used to create a loop in the spanning tree of `T`, yield the identity loop. In other words, if you start at the root of the tree, follow the path defined by the edge `e`, and return to the root, you end up with the identity morphism on the root of the tree.
More concisely: In a free groupoid with a wide, arborescent subquiver of symmetrized generators, any edge connecting generators yields the identity morphism when forming a loop in the spanning tree.
|
IsFreeGroupoid.SpanningTree.treeHom_eq
theorem IsFreeGroupoid.SpanningTree.treeHom_eq :
∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
(T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
[inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] {a : G}
(p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) a),
IsFreeGroupoid.SpanningTree.treeHom T a = IsFreeGroupoid.SpanningTree.homOfPath T p
This theorem states that for any given free groupoid `G`, and any spanning tree `T` of the symmetrized quiver of the generators of `G`, for any vertex `a` in `G`, if there is a path `p` from the root of the arborescence to `a` (in the context of the type associated with the `WideSubquiver T`), then the tree homomorphism at `a` is equal to the homomorphism of the path `p`. Essentially, it asserts a unique correspondence between a path to a given vertex and the tree homomorphism at that vertex, stemming from the uniqueness of paths in the tree.
More concisely: For any free groupoid `G` with spanning tree `T`, the tree homomorphism at a vertex `a` equals the homomorphism of any path from the root to `a` in the symmetrized quiver of `G` with respect to `T`.
|