Theorems · Inductive type · category theory

CategoryTheory.PreGaloisCategory.IsNaturalSMul

{C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      (G : Type u_1) → [inst_1 : Group G] → [(X : C) → MulAction G (F.obj X).obj] → Prop

We say G acts naturally on the fibers of F if for every f : X ⟶ Y, the G-actions on F.obj X and F.obj Y are compatible with F.map f.

Defined in

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Cited by

10 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

CategoryTheory.CategoryGroupMulAction