| Name | Category | Theorems |
|---|
asHom 📖 | CompOp | 1 mathmath: ext_iff
|
group 📖 | CompOp | 2 mathmath: IsFreeGroupoid.SpanningTree.endIsFree, IsFreeGroupoid.endIsFreeOfConnectedFree
|
inhabited 📖 | CompOp | — |
monoid 📖 | CompOp | 83 mathmath: Rep.coe_linearization_obj_ρ, Action.leftRegularTensorIso_inv_hom, CategoryTheory.TwistShiftData.z_zero_zero, Monoid.Foldl.ofFreeMonoid_apply, Action.ofMulAction_apply, CategoryTheory.Functor.commShift₂_comm, Traversable.foldlm.ofFreeMonoid_comp_of, Action.rightDual_ρ, CategoryTheory.CatCenter.smul_iso_inv_eq', Rep.linearization_single, CategoryTheory.Iso.conj_pow, CategoryTheory.CatCenter.smul_iso_inv_eq'_assoc, smul_left, IsFreeGroupoid.SpanningTree.functorOfMonoidHom_map, Rep.ρ_hom, Action.FunctorCategoryEquivalence.functor_map_app, ContinuousCohomology.I_obj_ρ_apply, CategoryTheory.Aut.toEnd_apply, CategoryTheory.TwistShiftData.assoc, ContinuousCohomology.Iobj_ρ_apply, CategoryTheory.isUnit_iff_isIso, CategoryTheory.TwistShiftData.shift_z_app, Action.tensorUnit_ρ, FDRep.hom_hom_action_ρ, CategoryTheory.Functor.mapAction_obj_ρ_apply, Action.FintypeCat.toEndHom_apply, CategoryTheory.SingleObj.functor_map, CategoryTheory.CatCenter.smul_iso_hom_eq'_assoc, Action.FunctorCategoryEquivalence.inverse_obj_ρ_apply, Traversable.foldl.unop_ofFreeMonoid, Action.leftRegularTensorIso_hom_hom, CategoryTheory.Functor.CommShift₂.comm, CategoryTheory.TwistShiftData.z_zero_left, Action.FintypeCat.quotientToEndHom_mk, CategoryTheory.PreGaloisCategory.FibreFunctor.end_isUnit, Monoid.foldlM.ofFreeMonoid_apply, CategoryTheory.CatCenter.smul_iso_inv_eq_assoc, Action.res_map_hom, Rep.linearization_obj_ρ, Action.ρ_self_inv_apply, Rep.linearizationTrivialIso_inv_hom, Action.ρ_one, Action.ρAut_apply_hom, smul_right, Action.trivial_ρ, CategoryTheory.CatCenter.smul_iso_hom_eq_assoc, Action.Hom.comm_assoc, Traversable.foldr.ofFreeMonoid_comp_of, CategoryTheory.Functor.mapEnd_apply, Traversable.foldrm.ofFreeMonoid_comp_of, CategoryTheory.CatCenter.smul_iso_inv_eq, CategoryTheory.CatCenter.app_neg_one_zpow, Action.res_obj_ρ, Rep.ofHom_ρ, Action.FunctorCategoryEquivalence.inverse_map_hom, CategoryTheory.TwistShiftData.shiftFunctorAdd'_inv_app, CategoryTheory.CatCenter.smul_iso_hom_eq', CategoryTheory.TwistShiftData.shiftFunctorAdd'_hom_app, Traversable.foldl.ofFreeMonoid_comp_of, Action.tensor_ρ, Monoid.Foldr.ofFreeMonoid_apply, Action.isContinuous_def, CategoryTheory.Functor.mapAction_map_hom, Action.leftDual_ρ, CategoryTheory.TwistShiftData.commShift, Action.Iso.conj_ρ, Rep.linearizationTrivialIso_hom_hom, CategoryTheory.CatCenter.smul_iso_hom_eq, CategoryTheory.CommShift₂Setup.z_zero₂, CategoryTheory.CommShift₂Setup.int_ε, CategoryTheory.Functor.commShift₂_comm_assoc, Action.FunctorCategoryEquivalence.functor_obj_map, Monoid.foldrM.ofFreeMonoid_apply, Action.ρAut_apply_inv, Action.Hom.comm, Action.ρ_inv_self_apply, FDRep.hom_action_ρ, CategoryTheory.CommShift₂Setup.z_zero₁, CategoryTheory.CommShift₂Setup.hε, Action.FintypeCat.toEndHom_trivial_of_mem, CategoryTheory.CommShift₂Setup.int_z, Action.FintypeCat.ofMulAction_apply, CategoryTheory.TwistShiftData.z_zero_right
|
mul 📖 | CompOp | 40 mathmath: CategoryTheory.InducedCategory.endEquiv_symm_apply_hom, CategoryTheory.InducedCategory.endEquiv_apply, FDRep.endRingEquiv_symm_comp_ρ, CategoryTheory.Iso.refl_conj, CategoryTheory.Iso.conj_pow, mul_def, ModuleCat.endRingEquiv_symm_apply_hom, CategoryTheory.CatCenter.mul_app, CategoryTheory.CatCenter.mul_app', CategoryTheory.Functor.map_conj, CategoryTheory.SingleObj.toEnd_def, CategoryTheory.CatCenter.mul_app_assoc, CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply, Units.toAut_hom, CategoryTheory.HomOrthogonal.matrixDecomposition_comp, FGModuleCat.Iso.conj_eq_conj, CategoryTheory.CatCenter.mul_app'_assoc, SemimoduleCat.Iso.conj_eq_conj, CategoryTheory.Iso.symm_self_conj, Rep.Action_ρ_eq_ρ, CategoryTheory.Iso.self_symm_conj, Units.toAut_inv, CategoryTheory.Iso.conjAut_hom, ModuleCat.Iso.conj_eq_conj, CategoryTheory.Iso.conj_id, CategoryTheory.ActionCategory.stabilizerIsoEnd_apply, CategoryTheory.Iso.trans_conj, FDRep.of_ρ, CategoryTheory.Functor.FullyFaithful.mulEquivEnd_apply, CategoryTheory.CatCenter.localization_mul, CategoryTheory.Iso.conj_comp, CategoryTheory.CatCenter.instIsMulCommutative, Action.Iso.conj_ρ, ModuleCat.endRingEquiv_apply, Rep.ihom_obj_ρ, FGModuleCat.Iso.conj_hom_eq_conj, CategoryTheory.Iso.conj_apply, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi, CategoryTheory.ActionCategory.stabilizerIsoEnd_symm_apply, FDRep.endRingEquiv_comp_ρ
|
mulActionLeft 📖 | CompOp | 1 mathmath: smul_left
|
mulActionRight 📖 | CompOp | 1 mathmath: smul_right
|
of 📖 | CompOp | — |
one 📖 | CompOp | 3 mathmath: CategoryTheory.HomOrthogonal.matrixDecomposition_id, one_def, CategoryTheory.CatCenter.localization_one
|