Theorems · Theorem · category theory

GrpCat.shrinkFunctor_map

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C GrpCat)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] {X Y : C} (f : X ⟶ Y),
  (GrpCat.shrinkFunctor.{w, w', v, u} F).map f =
    GrpCat.ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (GrpCat.Hom.hom (F.map f))).comp Shrink.mulEquiv.toMonoidHom)

Defined in

Mathlib.Algebra.Category.Grp.Shrink

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategorySmall