Theorems · Theorem · category theory

MonCat.shrinkFunctorMap_app

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C MonCat} (τ : F ⟶ G)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] [inst_2 : ∀ (X : C), Small.{w, w'} ↑(G.obj X)] (X : C),
  (MonCat.shrinkFunctorMap τ).app X =
    MonCat.ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (MonCat.Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom)

Defined in

Mathlib.Algebra.Category.MonCat.Shrink

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySmallSmall