Theorems · Theorem · combinatorics

Quiver.SchreierGraph.map_smul_of_comp_labelling_eq

∀ {V : Type u_1} {M : Type u_2} [inst : Group M] [inst_1 : MulAction M V] {S : Type u_3} (ι : S → M) {W : Type u_4}
  [inst_2 : MulAction M W] (φ : Quiver.SchreierGraph V ι ⥤q Quiver.SchreierGraph W ι),
  φ ⋙q Quiver.SchreierGraph.labelling W ι = Quiver.SchreierGraph.labelling V ι →
    ∀ (v : Quiver.SchreierGraph V ι) (s : S), φ.obj (ι s • v) = ι s • φ.obj v

If a prefunctor between Schreier graphs commutes with the labelling (i.e., labels are preserved), then it commutes with the group action. In other words, morphisms that preserve edge labels also preserve the group structure.

Defined in

Mathlib.Combinatorics.Quiver.Schreier

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

GroupMulActionMulAction