| Name | Category | Theorems |
|---|
category 📖 | CompOp | 103 mathmath: CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_apply_coe, Action.instIsEquivalenceFunctorSingleObjInverse, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, mapHom_id, Action.functorCategoryEquivalence_inverse, Action.FunctorCategoryEquivalence.counitIso_inv_app_app, Action.functorCategoryEquivalence_unitIso, CategoryTheory.Mat.instFaithfulMat_SingleObjMulOppositeEquivalenceSingleObjInverse, Action.leftUnitor_inv_hom, CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, MulEquiv.toSingleObjEquiv_inverse_map, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesQuotientsByFiniteGroups, Action.whiskerRight_hom, CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_symm_apply, Action.FunctorCategoryEquivalence.functor_obj_obj, CategoryTheory.PreGaloisCategory.isGalois_iff_aux, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, MonoidHom.id_toFunctor, Rep.homEquiv_apply_hom, CategoryTheory.FintypeCat.instHasColimitsOfShapeSingleObjFintypeCatOfFinite, IsFreeGroupoid.SpanningTree.functorOfMonoidHom_map, CategoryTheory.actionAsFunctor_map, Action.FunctorCategoryEquivalence.unitIso_inv_app_hom, Action.FunctorCategoryEquivalence.functor_map_app, Rep.MonoidalClosed.linearHomEquivComm_hom, CategoryTheory.Limits.SingleObj.Types.colimitEquivQuotient_apply, Action.FunctorCategoryEquivalence.functor_δ, inv_as_inv, MulEquiv.toSingleObjEquiv_unitIso_hom, CategoryTheory.Mat.instEssSurjMat_SingleObjMulOppositeEquivalenceSingleObjInverse, CategoryTheory.ActionCategory.uncurry_map, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_carrier, Action.functorCategoryEquivalence_functor, functor_map, CategoryTheory.ActionCategory.coe_back, Action.diagonalSuccIsoTensorTrivial_inv_hom_apply, MulEquiv.toSingleObjEquiv_functor_obj, Action.instIsEquivalenceFunctorSingleObjFunctor, MulEquiv.toSingleObjEquiv_counitIso_hom, IsFreeGroupoid.ext_functor_iff, functor_obj, CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_symm_apply, Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply, CategoryTheory.ActionCategory.π_obj, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite, CategoryTheory.PreGaloisCategory.instHasColimitsOfShapeSingleObjOfFinite, MulEquiv.toSingleObjEquiv_inverse_obj, MulEquiv.toSingleObjEquiv_unitIso_inv, CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_apply, Units.toAut_hom, IsFreeGroupoid.SpanningTree.functorOfMonoidHom_obj, MulEquiv.toSingleObjEquiv_counitIso_inv, CategoryTheory.ActionCategory.back_coe, differenceFunctor_map, CategoryTheory.Limits.SingleObj.colimitTypeRel_iff_orbitRel, CategoryTheory.ActionCategory.curry_apply_left, mapHom_comp, Action.functorCategoryEquivalence_counitIso, MonoidHom.comp_toFunctor, Action.FunctorCategoryEquivalence.inverse_obj_V, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeFintypeCatSingleObjInclOfFinite, Action.FunctorCategoryEquivalence.unitIso_hom_app_hom, CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_apply_coe, Action.tensorHom_hom, Action.associator_hom_hom, CategoryTheory.Mat.instIsEquivalenceMat_SingleObjMulOppositeEquivalenceSingleObjInverse, CategoryTheory.actionAsFunctor_obj, CategoryTheory.Limits.SingleObj.colimitTypeRelEquivOrbitRelQuotient_symm_apply, CategoryTheory.ActionCategory.comp_val, CategoryTheory.ActionCategory.uncurry_obj, Action.FunctorCategoryEquivalence.inverse_map_hom, CategoryTheory.PreGaloisCategory.hasQuotientsByFiniteGroups, Action.whiskerLeft_hom, Rep.MonoidalClosed.linearHomEquiv_hom, Units.toAut_inv, IsFreeGroupoid.unique_lift, CategoryTheory.ActionCategory.id_val, differenceFunctor_obj, Action.FunctorCategoryEquivalence.counitIso_hom_app_app, Rep.homEquiv_symm_apply_hom, CategoryTheory.PreGaloisCategory.IsGalois.quotientByAutTerminal, Action.FunctorCategoryEquivalence.functor_μ, CategoryTheory.ActionCategory.stabilizerIsoEnd_apply, CategoryTheory.Mat.instFullMat_SingleObjMulOppositeEquivalenceSingleObjInverse, CategoryTheory.ActionCategory.homOfPair.val, Rep.ihom_coev_app_hom, Action.rightUnitor_hom_hom, CategoryTheory.ActionCategory.π_map, CategoryTheory.Mat.equivalenceSingleObjInverse_map, Action.associator_inv_hom, Action.functorCategoryEquivalence_linear, Action.functorCategoryEquivalence_preservesZeroMorphisms, CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_symm_apply_coe, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_str, Action.rightUnitor_inv_hom, MulEquiv.toSingleObjEquiv_functor_map, Action.functorCategoryEquivalence_additive, Action.FunctorCategoryEquivalence.functor_obj_map, CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply, Action.leftUnitor_hom_hom, Action.FunctorCategoryEquivalence.functor_η, Action.FunctorCategoryEquivalence.functor_ε
|
categoryStruct 📖 | CompOp | 5 mathmath: id_as_one, comp_as_mul, toEnd_def, Units.toAut_hom, Units.toAut_inv
|
differenceFunctor 📖 | CompOp | 2 mathmath: differenceFunctor_map, differenceFunctor_obj
|
finCategoryOfFintype 📖 | CompOp | — |
functor 📖 | CompOp | 4 mathmath: CategoryTheory.PreGaloisCategory.isGalois_iff_aux, functor_map, functor_obj, CategoryTheory.PreGaloisCategory.IsGalois.quotientByAutTerminal
|
groupoid 📖 | CompOp | 1 mathmath: inv_as_inv
|
mapHom 📖 | CompOp | 2 mathmath: mapHom_id, mapHom_comp
|
natTrans 📖 | CompOp | 1 mathmath: natTrans_app
|
toEnd 📖 | CompOp | 3 mathmath: toEnd_def, Units.toAut_hom, Units.toAut_inv
|