Theorems · Theorem · category theory

Action.forget_map

∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G] {X Y : Action V G}
  (f : X ⟶ Y), (Action.forget V G).map f = f.hom

Defined in

Mathlib.CategoryTheory.Action.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryMonoid