Theorems · Definition · combinatorics

Quiver.SchreierGraph.labellingCostarEquiv

{V : Type u_1} →
  {M : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M V] →
        {S : Type u_3} →
          (ι : S → M) → (x : Quiver.SchreierGraph V ι) → Quiver.Costar x ≃ Quiver.Costar (Quiver.SingleObj.star S)

The costar map of the labelling prefunctor as an equivalence.

Defined in

Mathlib.Combinatorics.Quiver.Schreier

Cited by

4 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

GroupMulAction