Theorems · Definition · category theory

Action.ofMulActionLimitCone

{ι : Type v} →
  (G : Type (max v u)) →
    [inst : Monoid G] →
      (F : ι → Type (max v u)) →
        [inst_1 : (i : ι) → MulAction G (F i)] →
          CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor fun i => Action.ofMulAction G (F i))

Given a family F of types with G-actions, this is the limit cone demonstrating that the product of F as types is a product in the category of G-sets.

Defined in

Mathlib.CategoryTheory.Action.Concrete

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MonoidMulAction