Grp

📁 Source: MathlibTest/CategoryTheory/ConcreteCategory/Grp.lean

Statistics

Metric	Count
Definitions Grp	1
Theorems	0
Total	1

CategoryTheory

Definitions

Name	Category	Theorems
Grp 📖	CompData	155 math math: Grp.mkIso_inv_hom, Grp.Hom.hom_div, Grp.comp', Grp.mkIso_hom_hom, Grp.instIsIsoHomHomMon, Grp.homMk'_hom, Equivalence.mapGrp_counitIso, Grp.Hom.hom_hom_zpow, Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, Functor.mapCommGrp_obj_grp_one, Grp.id', Functor.FullyFaithful.mapGrp_preimage, yonedaGrp_obj, yonedaCommGrpGrpObj_map, Preadditive.toCommGrp_map, CommGrp.mkIso_inv_hom, Functor.comp_mapGrp_mul, Grp.whiskerLeft_hom_hom, Functor.mapGrp_id_mul, Functor.mapGrpIdIso_hom_app_hom_hom, instFaithfulGrpFunctorOppositeGrpCatYonedaGrp, Grp.leftUnitor_hom_hom, CommGrp.id', CommGrp.comp', Grp.ε_def, Grp.rightUnitor_hom_hom_hom, Grp.lift_hom, CommGrp.comp_hom, Grp.hom_mul, Grp.instHasInitial, CommGrp.instFaithfulGrpForget₂Grp, Functor.mapGrpFunctor_obj, Grp.Hom.hom_zpow, Functor.mapGrp_obj_grp_one, Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, Functor.mapGrp_id_one, Grp.associator_inv_hom_hom, Grp.Hom.hom_hom_div, Grp.leftUnitor_hom_hom_hom, CommGrp.instIsIsoMonHomGrp, Grp.forget_map, Grp.mkIso_hom_hom_hom, CommGrp.forget₂CommMon_map_hom, CommGrp.forget₂Grp_obj_mul, Adjunction.mapGrp_unit, Grp.instIsMonHom, Grp.rightUnitor_inv_hom_hom, Functor.essImage_mapGrp, Grp.forget₂Mon_map_hom, Grp.whiskerRight_hom_hom, Grp.Hom.hom_hom_inv, Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, essImage_yonedaGrp, Grp.μ_def, Grp.snd_hom, Grp.tensorUnit_mul, CommGrp.forget₂Grp_obj_X, Grp.tensorUnit_X, Grp.whiskerLeft_hom, Functor.mapGrpNatIso_hom_app_hom_hom, Functor.mapGrpFunctor_map_app, Equivalence.mapGrp_inverse, Grp.leftUnitor_inv_hom_hom, Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, Grp.rightUnitor_inv_hom, CommGrp.hom_ext_iff, Grp.forget₂Mon_obj_mul, Grp.Hom.hom_pow, Grp.δ_def, Grp.associator_hom_hom_hom, Grp.braiding_inv_hom, Grp.mkIso'_hom_hom_hom, Grp.id_hom, Functor.mapGrpCompIso_hom_app_hom_hom, Grp.fst_hom, CommGrp.mkIso_inv_hom_hom_hom, CommGrp.mkIso'_inv_hom_hom_hom, Equivalence.mapGrp_unitIso, Grp.tensorUnit_one, yonedaCommGrpGrp_obj, CommGrp.forget₂Grp_obj_one, CommGrp.forget₂Grp_comp_forget, Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, Functor.mapGrp_map_hom_hom, CommGrp.forget₂Grp_map_hom, Grp.comp_hom_hom, Grp.braiding_inv_hom_hom, Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CommGrp.mkIso_hom_hom, instFullGrpFunctorOppositeGrpCatYonedaGrp, Grp.tensorObj_X, Grp.Hom.hom_mul, yonedaCommGrpGrpObj_obj_coe, Grp.tensorObj_mul, Grp.rightUnitor_hom_hom, Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, Grp.forget₂Mon_obj_X, Grp.hom_ext_iff, Grp.homMk''_hom_hom, Grp.instIsCommMonObj, Grp.forget₂Mon_comp_forget, Functor.Full.mapGrp, Functor.FullyFaithful.mapCommGrp_preimage, CommGrp.instIsIsoGrpHom, Grp.tensorObj_one, Functor.mapGrpIdIso_inv_app_hom_hom, CommGrp.mkIso_hom_hom_hom_hom, Grp.leftUnitor_inv_hom, CommGrp.id_hom, Functor.mapGrp_obj_grp_mul, Grp.mkIso_inv_hom_hom, Grp.snd_hom_hom, Functor.mapGrpNatTrans_app_hom_hom, Grp.hom_one, Grp.forget₂Mon_obj_one, Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, yonedaCommGrpGrp_map_app, Grp.associator_inv_hom, Grp.homMk_hom_hom, Functor.mapGrpNatIso_inv_app_hom_hom, Functor.mapGrpCompIso_inv_app_hom_hom, Grp.Hom.hom_inv, Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, Grp.instFaithfulMonForget₂Mon, Grp.braiding_hom_hom, Functor.mapCommGrp_map_hom_hom_hom, Functor.mapGrp_obj_grp_inv, Grp.η_def, Grp.associator_hom_hom, Preadditive.commGrpEquivalence_inverse_map, Functor.mapCommGrpNatTrans_app_hom_hom_hom, Functor.Faithful.mapGrp, Grp.forget_obj, yonedaGrp_map_app, CommGrp.mkIso'_hom_hom_hom_hom, Grp.whiskerRight_hom, Functor.mapCommGrp_obj_grp_mul, Grp.tensorHom_hom, Grp.Hom.hom_one, Equivalence.mapGrp_functor, Grp.fst_hom_hom, Grp.mkIso'_inv_hom_hom, Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, Grp.braiding_hom_hom_hom, Grp.instFaithfulForget, Grp.comp_hom, Grp.instFullMonForget₂Mon, Functor.mapGrp_obj_X, Grp.id_hom_hom, Functor.mapCommGrp_obj_grp_inv, Adjunction.mapGrp_counit, Functor.comp_mapGrp_one, CommGrp.forget_map, CommGrp.instFullGrpForget₂Grp

---

← Back to Index