Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality

∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {F : CategoryTheory.Functor C FintypeCat} {G : Type u_1}
  {inst_1 : Group G} {inst_2 : (X : C) → MulAction G (F.obj X).obj}
  [self : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] (g : G) {X Y : C} (f : X ⟶ Y) (x : (F.obj X).obj),
  (CategoryTheory.ConcreteCategory.hom (F.map f)) (g • x) = g • (CategoryTheory.ConcreteCategory.hom (F.map f)) x

Defined in

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.PreGaloisCategory.IsNaturalSMul