Theorems · Definition · category theory

Action.functorCategoryEquivalenceCompEvaluation

(V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        (Action.functorCategoryEquivalence V G).functor.comp
            ((CategoryTheory.evaluation (CategoryTheory.SingleObj G) V).obj PUnit.unit) ≅
          Action.forget V G

The forgetful functor is intertwined by functorCategoryEquivalence with evaluation at PUnit.star.

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryMonoid