Theorems · Theorem · category theory

CommGrpCat.coyonedaType_map_app

∀ {X Y : Type uᵒᵖ} (f : X ⟶ Y) (G : CommGrpCat),
  (CommGrpCat.coyonedaType.map f).app G =
    CommGrpCat.ofHom
      (MonoidHom.pi fun i => Pi.evalMonoidHom (fun a => ↑G) ((CategoryTheory.ConcreteCategory.hom f.unop) i))

Defined in

Mathlib.Algebra.Category.Grp.Yoneda

Cited by

0 results in Mathlib

Foundations

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