Basic

📁 Source: Mathlib/CategoryTheory/Action/Basic.lean

Statistics

Metric	Count
Definitions counitIso, functor, inverse, unitIso, comp, hom, id, instInhabited, HomSubtype, V, actionPUnitEquivalence, actionPunitEquivalence, forget, functorCategoryEquivalence, functorCategoryEquivalenceCompEvaluation, hasForgetToV, inhabited', instCategory, instConcreteCategoryHomSubtypeV, instFunLikeHomSubtypeV, instInhabitedAddCommGrpCat, mkIso, res, resComp, resCongr, resEquiv, resId, trivial, ρ, ρAut, mapAction, mapAction, mapAction, mapActionComp, mapActionCongr	35
Theorems counitIso_hom_app_app, counitIso_inv_app_app, functor_map_app, functor_obj_map, functor_obj_obj, inverse_map_hom, inverse_obj_V, inverse_obj_ρ_apply, unitIso_hom_app_hom, unitIso_inv_app_hom, comm, comm_assoc, comp_hom, ext, ext_iff, id_hom, conj_ρ, comp_hom, comp_hom_assoc, forget_map, forget_obj, full_res, functorCategoryEquivalence_counitIso, functorCategoryEquivalence_functor, functorCategoryEquivalence_inverse, functorCategoryEquivalence_unitIso, hom_ext, hom_ext_iff, hom_injective, hom_inv_hom, hom_inv_hom_assoc, id_hom, instFaithfulForget, instFaithfulRes, instIsEquivalenceFunctorSingleObjFunctor, instIsEquivalenceFunctorSingleObjInverse, instIsIsoHomHom, instIsIsoHomInv, inv_hom_hom, inv_hom_hom_assoc, isIso_hom_mk, isIso_of_hom_isIso, mkIso_hom_hom, mkIso_inv_hom, preservesColimits_forget, preservesLimits_forget, resComp_hom_app_hom, resComp_inv_app_hom, resCongr_hom, resCongr_inv, resEquiv_functor, resEquiv_inverse, resId_hom_app_hom, resId_inv_app_hom, res_map_hom, res_obj_V, res_obj_ρ, trivial_V, trivial_ρ, ρAut_apply_hom, ρAut_apply_inv, ρ_one, mapAction_functor, mapAction_inverse, instFaithfulActionMapAction, instFullActionMapActionOfFaithful, mapActionComp_hom, mapActionComp_inv, mapActionCongr_hom, mapActionCongr_inv, mapAction_map_hom, mapAction_obj_V, mapAction_obj_ρ_apply	73
Total	108

Action

Definitions

Name	Category	Theorems
HomSubtype 📖	CompOp	13 math math: DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, forget₂_preservesZeroMorphisms, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FDRep.forget₂_ρ, isContinuous_def, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, forget₂_linear, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, forget₂_additive, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
V 📖	CompOp	169 math math: resCongr_inv, DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, leftRegularTensorIso_inv_hom, neg_hom, ContinuousCohomology.I_obj_V_isAddCommGroup, inv_hom_hom_assoc, sum_hom, ContinuousCohomology.I_obj_V_carrier, ofMulAction_apply, FDRep.endRingEquiv_symm_comp_ρ, CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected, Representation.LinearizeMonoidal.ε_η, CategoryTheory.Functor.mapAction_δ_hom, tensorObj_V, TannakaDuality.FiniteGroup.forget_obj, Representation.linearize_single, Hom.comp_hom, leftUnitor_inv_hom, comp_hom, rightDual_ρ, whiskerRight_hom, Rep.ε_def, CategoryTheory.Functor.mapContActionCongr_inv, FunctorCategoryEquivalence.functor_obj_obj, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, Representation.LinearizeMonoidal.μ_apply_single_single, Rep.μ_def, forget₂_preservesZeroMorphisms, smul_hom, Rep.ActionToRep_obj_ρ, CategoryTheory.Functor.mapContActionCongr_hom, FunctorCategoryEquivalence.unitIso_inv_app_hom, FunctorCategoryEquivalence.functor_map_app, ContinuousCohomology.I_obj_ρ_apply, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, Rep.ActionToRep_obj_V, Representation.LinearizeMonoidal.μ_comp_assoc, hom_inv_hom, ContinuousCohomology.Iobj_ρ_apply, mkIso_hom_hom, TannakaDuality.FiniteGroup.sumSMulInv_apply, Rep.δ_def, resId_inv_app_hom, ContinuousCohomology.I_obj_V_isModule, FDRep.average_char_eq_finrank_invariants, Representation.LinearizeMonoidal.ε_one, Representation.LinearizeMonoidal.μ_comp_rTensor, instIsIsoHomInv, Representation.LinearizeMonoidal.μ_δ, CategoryTheory.PreGaloisCategory.instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, FDRep.hom_hom_action_ρ, CategoryTheory.Functor.mapAction_obj_ρ_apply, FintypeCat.toEndHom_apply, ContAction.resCongr_hom, Representation.linearizeTrivialIso_apply, hom_injective, nsmul_hom, diagonalSuccIsoTensorTrivial_inv_hom_apply, Representation.LinearizeMonoidal.η_toLinearMap, id_hom, Rep.RepToAction_obj_V_isAddCommGroup, sub_hom, TannakaDuality.FiniteGroup.equivApp_inv, CategoryTheory.Functor.mapAction_obj_V, res_obj_V, TannakaDuality.FiniteGroup.equivApp_hom, FDRep.char_linHom, forget_obj, rightDual_v, Representation.LinearizeMonoidal.assoc_comp_δ, Hom.id_hom, leftRegularTensorIso_hom_hom, Representation.linearizeOfMulActionIso_apply, ContinuousCohomology.I_map_hom, Rep.ActionToRep_map, CategoryTheory.Functor.mapAction_μ_hom, FintypeCat.quotientToEndHom_mk, Representation.LinearizeMonoidal.rTensor_comp_δ, Rep.RepToAction_obj_V_carrier, Rep.RepToAction_obj_V_isModule, zero_hom, Representation.LinearizeMonoidal.μ_comp_lTensor, Representation.LinearizeMonoidal.rightUnitor_δ, Representation.LinearizeMonoidal.η_single, res_map_hom, instIsIsoHomHom, ρ_self_inv_apply, FDRep.char_one, ρ_one, add_hom, ρAut_apply_hom, TannakaDuality.FiniteGroup.sumSMulInv_single_id, CategoryTheory.FintypeCat.Action.isConnected_iff_transitive, CategoryTheory.Functor.mapActionCongr_inv, Hom.comm_assoc, tensor_ρ_apply, FunctorCategoryEquivalence.inverse_obj_V, resComp_inv_app_hom, Representation.LinearizeMonoidal.leftUnitor_δ, FunctorCategoryEquivalence.unitIso_hom_app_hom, hom_inv_hom_assoc, tensorHom_hom, inv_hom_hom, associator_hom_hom, res_obj_ρ, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, Rep.linearization_map, CategoryTheory.Functor.mapActionCongr_hom, Representation.LinearizeMonoidal.η_ε, Representation.LinearizeMonoidal.lTensor_comp_δ, mkIso_inv_hom, Representation.LinearizeMonoidal.δ_apply_single, FintypeCat.quotientToQuotientOfLE_hom_mk, Representation.linearizeOfMulActionIso_symm_apply, ContAction.resCongr_inv, whiskerLeft_hom, Rep.linearization_obj_V, Representation.linearizeMap_single, zsmul_hom, Rep.η_def, Representation.LinearizeMonoidal.μ_toLinearMap, Representation.LinearizeMonoidal.μ_leftUnitor, Representation.LinearizeMonoidal.μ_rightUnitor, tensorUnit_V, ContinuousCohomology.I_obj_V_topologicalSpace, FDRep.forget₂_ρ, Representation.LinearizeMonoidal.δ_μ, tensor_ρ, FDRep.Iso.conj_ρ, β_inv_hom, FDRep.char_dual, resId_hom_app_hom, rightUnitor_hom_hom, leftDual_v, Representation.linearizeMap_toLinearMap, isContinuous_def, CategoryTheory.Functor.mapAction_map_hom, associator_inv_hom, leftDual_ρ, Iso.conj_ρ, rightUnitor_inv_hom, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, Representation.LinearizeMonoidal.μ_apply_apply, resComp_hom_app_hom, TannakaDuality.FiniteGroup.ofRightFDRep_hom, forget₂_linear, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FunctorCategoryEquivalence.functor_obj_map, ρAut_apply_inv, Hom.comm, ρ_inv_self_apply, comp_hom_assoc, ContinuousCohomology.const_app_hom, ofMulAction_V, FDRep.hom_action_ρ, FDRep.dualTensorIsoLinHom_hom_hom, resCongr_hom, Representation.linearize_apply, trivial_V, FDRep.endRingEquiv_comp_ρ, β_hom_hom, Representation.linearizeTrivial_def, leftUnitor_hom_hom, forget₂_additive, Representation.LinearizeMonoidal.ε_toLinearMap, Representation.linearizeTrivialIso_symm_apply, FintypeCat.ofMulAction_apply, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
actionPUnitEquivalence 📖	CompOp	—
actionPunitEquivalence 📖	CompOp	—
forget 📖	CompOp	26 math math: forget_η, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget, instReflectsLimitsOfShapeForget, forget_preservesZeroMorphisms, instPreservesColimitForgetOfHasColimitComp, preservesColimits_forget, instPreservesFiniteLimitsForgetOfHasFiniteLimits, instFaithfulForget, forget_δ, preservesLimits_forget, instPreservesLimitForgetOfHasLimitComp, forget_obj, forget_additive, instPreservesFiniteColimitsForgetOfHasFiniteColimits, instReflectsColimitsForget, instReflectsColimitsOfShapeForget, instPreservesLimitsOfShapeForgetOfHasLimitsOfShape, forget_ε, instReflectsLimitsForget, forget_linear, forget_μ, instReflectsLimitForget, Iso.conj_ρ, instPreservesColimitsOfShapeForgetOfHasColimitsOfShape, instReflectsColimitForget, forget_map
functorCategoryEquivalence 📖	CompOp	16 math math: functorCategoryEquivalence_inverse, functorCategoryEquivalence_unitIso, leftUnitor_inv_hom, whiskerRight_hom, functorCategoryEquivalence_functor, functorCategoryEquivalence_counitIso, tensorHom_hom, associator_hom_hom, whiskerLeft_hom, rightUnitor_hom_hom, associator_inv_hom, functorCategoryEquivalence_linear, functorCategoryEquivalence_preservesZeroMorphisms, rightUnitor_inv_hom, functorCategoryEquivalence_additive, leftUnitor_hom_hom
functorCategoryEquivalenceCompEvaluation 📖	CompOp	—
hasForgetToV 📖	CompOp	5 math math: CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, forget₂_preservesZeroMorphisms, forget₂_linear, forget₂_additive, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
inhabited' 📖	CompOp	—
instCategory 📖	CompOp	290 math math: resCongr_inv, forget_η, DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, instIsEquivalenceFunctorSingleObjInverse, Rep.μ_hom, leftRegularTensorIso_inv_hom, neg_hom, ContinuousCohomology.I_obj_V_isAddCommGroup, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, inv_hom_hom_assoc, FDRep.char_tensor, sum_hom, ContinuousCohomology.I_obj_V_carrier, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget, Representation.LinearizeMonoidal.ε_η, diagonalSuccIsoTensorDiagonal_inv_hom, CategoryTheory.Functor.mapAction_δ_hom, Functor.mapActionPreservesLimitsOfShapeOfPreserves, tensorObj_V, TannakaDuality.FiniteGroup.forget_obj, functorCategoryEquivalence_inverse, instHasLimits, FunctorCategoryEquivalence.counitIso_inv_app_app, functorCategoryEquivalence_unitIso, leftUnitor_inv_hom, comp_hom, instHasFiniteProducts, rightDual_ρ, instHasFiniteCoproducts, whiskerRight_hom, Rep.ε_def, CategoryTheory.Functor.mapContActionCongr_inv, CategoryTheory.Functor.mapActionComp_hom, FunctorCategoryEquivalence.functor_obj_obj, instReflectsLimitsOfShapeForget, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, Representation.LinearizeMonoidal.μ_apply_single_single, Rep.μ_def, Functor.mapActionPreservesLimit_of_preserves, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor, forget₂_preservesZeroMorphisms, smul_hom, CategoryTheory.Functor.mapContActionComp_inv, forget_preservesZeroMorphisms, Rep.ActionToRep_obj_ρ, CategoryTheory.Functor.mapContActionCongr_hom, FunctorCategoryEquivalence.unitIso_inv_app_hom, CategoryTheory.Functor.mapActionComp_inv, FunctorCategoryEquivalence.functor_map_app, CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, ContinuousCohomology.I_obj_ρ_apply, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FDRep.instFiniteDimensionalHom, Rep.ActionToRep_obj_V, instPreservesColimitForgetOfHasColimitComp, FunctorCategoryEquivalence.functor_δ, ContAction.resEquiv_inverse, Representation.LinearizeMonoidal.μ_comp_assoc, hom_inv_hom, CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction, CategoryTheory.FintypeCat.instMonoActionFintypeCatImageComplementIncl, ContinuousCohomology.instLinearActionTopModuleCatInvariants, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, Functor.mapActionPreservesColimit_of_preserves, isIso_of_hom_isIso, mkIso_hom_hom, preservesColimits_forget, Rep.δ_def, CategoryTheory.PreGaloisCategory.functorToContAction_map, CategoryTheory.Equivalence.mapAction_functor, resId_inv_app_hom, ContinuousCohomology.I_obj_V_isModule, CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction, Representation.LinearizeMonoidal.ε_one, Representation.LinearizeMonoidal.μ_comp_rTensor, instIsIsoHomInv, CategoryTheory.Equivalence.mapContAction_functor, tensorUnit_ρ, functorCategoryEquivalence_functor, Representation.LinearizeMonoidal.μ_δ, Rep.RepToAction_map_hom, Functor.instPreservesFiniteLimitsMapActionOfHasFiniteLimits, CategoryTheory.PreGaloisCategory.exists_lift_of_continuous, CategoryTheory.Functor.mapAction_η_hom, CategoryTheory.Functor.mapContAction_map, instPreservesFiniteLimitsForgetOfHasFiniteLimits, CategoryTheory.PreGaloisCategory.instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, CategoryTheory.Functor.mapAction_obj_ρ_apply, FintypeCat.toEndHom_apply, ContAction.resCongr_hom, ContinuousCohomology.instAdditiveActionTopModuleCatInvariants, nsmul_hom, instFaithfulForget, classifyingSpaceUniversalCover_map, diagonalSuccIsoTensorTrivial_inv_hom_apply, preservesLimitsOfShape_of_preserves, CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected, CategoryTheory.Functor.mapAction_linear, CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCat, instIsEquivalenceFunctorSingleObjFunctor, res_additive, forget_δ, ContinuousCohomology.MultiInd.d_comp_d_assoc, FunctorCategoryEquivalence.inverse_obj_ρ_apply, Representation.LinearizeMonoidal.η_toLinearMap, hasLimitsOfShape, ContAction.res_obj_obj, id_hom, Rep.RepToAction_obj_V_isAddCommGroup, sub_hom, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite, hasColimitsOfShape, preservesLimits_forget, CategoryTheory.Functor.mapAction_ε_hom, TannakaDuality.FiniteGroup.forget_map, CategoryTheory.Functor.mapAction_obj_V, instPreservesLimitForgetOfHasLimitComp, res_obj_V, forget_obj, rightDual_v, ContAction.resComp_hom, Representation.LinearizeMonoidal.assoc_comp_δ, CategoryTheory.Functor.mapAction_preadditive, leftRegularTensorIso_hom_hom, preservesColimitsOfSize_of_preserves, ContinuousCohomology.I_map_hom, Rep.ActionToRep_map, CategoryTheory.Functor.mapAction_μ_hom, FintypeCat.quotientToEndHom_mk, CategoryTheory.Functor.instFullActionMapActionOfFaithful, forget_additive, Representation.LinearizeMonoidal.rTensor_comp_δ, Rep.RepToAction_obj_V_carrier, Rep.RepToAction_obj_V_isModule, zero_hom, Representation.LinearizeMonoidal.μ_comp_lTensor, Representation.LinearizeMonoidal.rightUnitor_δ, Rep.δ_hom, Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits, instPreservesFiniteColimitsForgetOfHasFiniteColimits, ContAction.resEquiv_functor, FDRep.instHasKernels, Representation.LinearizeMonoidal.η_single, res_map_hom, Rep.linearization_obj_ρ, instIsIsoHomHom, instReflectsColimitsForget, CategoryTheory.PreGaloisCategory.functorToAction_map, instReflectsColimitsOfShapeForget, FDRep.instInjectiveOfNeZeroCastCard, Rep.ε_hom, instPreservesLimitsOfShapeForgetOfHasLimitsOfShape, add_hom, instHasFiniteColimits, CategoryTheory.FintypeCat.Action.isConnected_iff_transitive, CategoryTheory.Functor.mapActionCongr_inv, FDRep.simple_iff_end_is_rank_one, CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction, tensor_ρ_apply, Rep.instIsEquivalenceActionModuleCatRepToAction, functorCategoryEquivalence_counitIso, forget_ε, FunctorCategoryEquivalence.inverse_obj_V, resComp_inv_app_hom, Rep.η_hom, Representation.LinearizeMonoidal.leftUnitor_δ, Rep.RepToAction_obj_ρ, FunctorCategoryEquivalence.unitIso_hom_app_hom, hom_inv_hom_assoc, tensorHom_hom, inv_hom_hom, associator_hom_hom, res_obj_ρ, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction, Functor.preservesLimitsOfSize_of_preserves, Rep.linearization_map, full_res, instReflectsLimitsForget, CategoryTheory.PreGaloisCategory.has_decomp_quotients, CategoryTheory.Functor.mapActionCongr_hom, Representation.LinearizeMonoidal.η_ε, Representation.LinearizeMonoidal.lTensor_comp_δ, mkIso_inv_hom, Representation.LinearizeMonoidal.δ_apply_single, FunctorCategoryEquivalence.inverse_map_hom, ContAction.resCongr_inv, whiskerLeft_hom, Rep.linearization_obj_V, zsmul_hom, CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction, preservesLimitsOfSize_of_preserves, Rep.η_def, Representation.LinearizeMonoidal.μ_toLinearMap, Representation.LinearizeMonoidal.μ_leftUnitor, FunctorCategoryEquivalence.counitIso_hom_app_app, ContinuousCohomology.instLinearActionTopModuleCatI, Representation.LinearizeMonoidal.μ_rightUnitor, tensorUnit_V, ContinuousCohomology.I_obj_V_topologicalSpace, instMonoidalPreadditive, FDRep.forget₂_ρ, Representation.LinearizeMonoidal.δ_μ, FDRep.char_orthonormal, FunctorCategoryEquivalence.functor_μ, CategoryTheory.Equivalence.mapContAction_inverse, tensor_ρ, ContinuousCohomology.MultiInd.d_comp_d, CategoryTheory.Functor.mapContActionComp_hom, resEquiv_inverse, Functor.preservesColimitsOfSize_of_preserves, β_inv_hom, forget_linear, CategoryTheory.PreGaloisCategory.exists_lift_of_mono, diagonalSuccIsoTensorDiagonal_hom_hom, resId_hom_app_hom, instHasColimits, rightUnitor_hom_hom, forget_μ, diagonalSuccIsoTensorTrivial_hom_hom_apply, leftDual_v, CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj, CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, isContinuous_def, CategoryTheory.Functor.mapAction_map_hom, Functor.mapActionPreservesColimitsOfShapeOfPreserves, associator_inv_hom, resEquiv_functor, Rep.RepToAction_obj, leftDual_ρ, instFaithfulRes, Rep.instIsEquivalenceActionModuleCatActionToRep, functorCategoryEquivalence_linear, CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup, instReflectsLimitForget, CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat, functorCategoryEquivalence_preservesZeroMorphisms, FDRep.instProjectiveOfNeZeroCastCard, Iso.conj_ρ, preservesColimit_of_preserves, rightUnitor_inv_hom, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, res_linear, instPreservesColimitsOfShapeForgetOfHasColimitsOfShape, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, Representation.LinearizeMonoidal.μ_apply_apply, ContinuousCohomology.MultiInd.d_succ, FDRep.scalar_product_char_eq_finrank_equivariant, instMonoidalLinear, resComp_hom_app_hom, functorCategoryEquivalence_additive, preservesColimitsOfShape_of_preserves, CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, forget₂_linear, isIso_hom_mk, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FunctorCategoryEquivalence.functor_obj_map, CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction, CategoryTheory.Functor.mapContAction_obj_obj, comp_hom_assoc, ContinuousCohomology.const_app_hom, ContAction.resComp_inv, instHasFiniteLimits, TannakaDuality.FiniteGroup.equivHom_surjective, TannakaDuality.FiniteGroup.equivHom_injective, ContAction.res_map, FDRep.dualTensorIsoLinHom_hom_hom, CategoryTheory.Equivalence.mapAction_inverse, resCongr_hom, β_hom_hom, CategoryTheory.FintypeCat.Action.isConnected_of_transitive, instReflectsColimitForget, CategoryTheory.PreGaloisCategory.functorToAction_full, TannakaDuality.FiniteGroup.equivHom_apply, leftUnitor_hom_hom, FunctorCategoryEquivalence.functor_η, FDRep.simple_iff_char_is_norm_one, ContinuousCohomology.instAdditiveActionTopModuleCatI, forget₂_additive, forget_map, classifyingSpaceUniversalCover_obj, FintypeCat.toEndHom_trivial_of_mem, CategoryTheory.Functor.instFaithfulActionMapAction, Representation.LinearizeMonoidal.ε_toLinearMap, FunctorCategoryEquivalence.functor_ε, CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction, FDRep.finrank_hom_simple_simple, preservesLimit_of_preserves, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
instConcreteCategoryHomSubtypeV 📖	CompOp	12 math math: CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, forget₂_preservesZeroMorphisms, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FDRep.forget₂_ρ, isContinuous_def, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, forget₂_linear, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, forget₂_additive, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
instFunLikeHomSubtypeV 📖	CompOp	13 math math: DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, forget₂_preservesZeroMorphisms, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, FDRep.forget₂_ρ, isContinuous_def, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρOfIsNoetherianRing, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, forget₂_linear, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVIntertwiningMapVρ, forget₂_additive, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
instInhabitedAddCommGrpCat 📖	CompOp	—
mkIso 📖	CompOp	10 math math: resCongr_inv, CategoryTheory.Functor.mapContActionCongr_inv, CategoryTheory.Functor.mapContActionCongr_hom, mkIso_hom_hom, ContAction.resCongr_hom, CategoryTheory.Functor.mapActionCongr_inv, CategoryTheory.Functor.mapActionCongr_hom, mkIso_inv_hom, ContAction.resCongr_inv, resCongr_hom
res 📖	CompOp	19 math math: resCongr_inv, resId_inv_app_hom, ContAction.resCongr_hom, res_additive, ContAction.res_obj_obj, res_obj_V, res_map_hom, resComp_inv_app_hom, res_obj_ρ, full_res, ContAction.resCongr_inv, resEquiv_inverse, resId_hom_app_hom, resEquiv_functor, instFaithfulRes, res_linear, resComp_hom_app_hom, ContAction.res_map, resCongr_hom
resComp 📖	CompOp	2 math math: resComp_inv_app_hom, resComp_hom_app_hom
resCongr 📖	CompOp	2 math math: resCongr_inv, resCongr_hom
resEquiv 📖	CompOp	2 math math: resEquiv_inverse, resEquiv_functor
resId 📖	CompOp	2 math math: resId_inv_app_hom, resId_hom_app_hom
trivial 📖	CompOp	9 math math: leftRegularTensorIso_inv_hom, Representation.linearizeTrivialIso_apply, diagonalSuccIsoTensorTrivial_inv_hom_apply, leftRegularTensorIso_hom_hom, trivial_ρ, diagonalSuccIsoTensorTrivial_hom_hom_apply, trivial_V, Representation.linearizeTrivial_def, Representation.linearizeTrivialIso_symm_apply
ρ 📖	CompOp	39 math math: leftRegularTensorIso_inv_hom, ofMulAction_apply, FDRep.endRingEquiv_symm_comp_ρ, Representation.linearize_single, rightDual_ρ, Rep.ActionToRep_obj_ρ, FunctorCategoryEquivalence.functor_map_app, ContinuousCohomology.I_obj_ρ_apply, ContinuousCohomology.Iobj_ρ_apply, tensorUnit_ρ, FDRep.hom_hom_action_ρ, CategoryTheory.Functor.mapAction_obj_ρ_apply, FunctorCategoryEquivalence.inverse_obj_ρ_apply, leftRegularTensorIso_hom_hom, ofMulAction_ρ, Rep.ActionToRep_map, res_map_hom, ρ_self_inv_apply, ρ_one, ρAut_apply_hom, trivial_ρ, Hom.comm_assoc, tensor_ρ_apply, Rep.RepToAction_obj_ρ, res_obj_ρ, tensor_ρ, FDRep.of_ρ, isContinuous_def, CategoryTheory.Functor.mapAction_map_hom, leftDual_ρ, Iso.conj_ρ, FunctorCategoryEquivalence.functor_obj_map, ρAut_apply_inv, Hom.comm, ρ_inv_self_apply, FDRep.hom_action_ρ, Representation.linearize_apply, FDRep.endRingEquiv_comp_ρ, FintypeCat.ofMulAction_apply
ρAut 📖	CompOp	2 math math: ρAut_apply_hom, ρAut_apply_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp Action CategoryTheory.Category.toCategoryStruct instCategory V	—	—
comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V Hom.hom Action instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom
forget_map 📖	mathematical	—	CategoryTheory.Functor.map Action instCategory forget Hom.hom	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj Action instCategory forget V	—	—
full_res 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	CategoryTheory.Functor.Full Action instCategory res	—	Hom.comm hom_ext
functorCategoryEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso Action CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category instCategory CategoryTheory.Functor.category functorCategoryEquivalence FunctorCategoryEquivalence.counitIso	—	—
functorCategoryEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Action CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category instCategory CategoryTheory.Functor.category functorCategoryEquivalence FunctorCategoryEquivalence.functor	—	—
functorCategoryEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Action CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category instCategory CategoryTheory.Functor.category functorCategoryEquivalence FunctorCategoryEquivalence.inverse	—	—
functorCategoryEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso Action CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category instCategory CategoryTheory.Functor.category functorCategoryEquivalence FunctorCategoryEquivalence.unitIso	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_injective 📖	mathematical	—	Hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct V Hom.hom	—	Hom.ext
hom_inv_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V Hom.hom CategoryTheory.Iso.hom Action instCategory CategoryTheory.Iso.inv CategoryTheory.CategoryStruct.id	—	comp_hom CategoryTheory.Iso.hom_inv_id id_hom
hom_inv_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V Hom.hom CategoryTheory.Iso.hom Action instCategory CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' hom_inv_hom
id_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id Action CategoryTheory.Category.toCategoryStruct instCategory V	—	—
instFaithfulForget 📖	mathematical	—	CategoryTheory.Functor.Faithful Action instCategory forget	—	Hom.ext
instFaithfulRes 📖	mathematical	—	CategoryTheory.Functor.Faithful Action instCategory res	—	hom_ext res_map_hom
instIsEquivalenceFunctorSingleObjFunctor 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence Action instCategory CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category FunctorCategoryEquivalence.functor	—	CategoryTheory.Equivalence.isEquivalence_functor
instIsEquivalenceFunctorSingleObjInverse 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action instCategory FunctorCategoryEquivalence.inverse	—	CategoryTheory.Equivalence.isEquivalence_inverse
instIsIsoHomHom 📖	mathematical	—	CategoryTheory.IsIso V Hom.hom CategoryTheory.Iso.hom Action instCategory	—	hom_inv_hom inv_hom_hom
instIsIsoHomInv 📖	mathematical	—	CategoryTheory.IsIso V Hom.hom CategoryTheory.Iso.inv Action instCategory	—	inv_hom_hom hom_inv_hom
inv_hom_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V Hom.hom CategoryTheory.Iso.inv Action instCategory CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	comp_hom CategoryTheory.Iso.inv_hom_id id_hom
inv_hom_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V Hom.hom CategoryTheory.Iso.inv Action instCategory CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inv_hom_hom
isIso_hom_mk 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct V DFunLike.coe MonoidHom CategoryTheory.End MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike ρ	CategoryTheory.IsIso Action instCategory	—	CategoryTheory.Iso.isIso_hom
isIso_of_hom_isIso 📖	mathematical	—	CategoryTheory.IsIso Action instCategory	—	CategoryTheory.Iso.isIso_hom Hom.comm
mkIso_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.hom Action instCategory mkIso V	—	—
mkIso_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.inv Action instCategory mkIso V	—	—
preservesColimits_forget 📖	mathematical	—	CategoryTheory.Limits.PreservesColimits Action instCategory forget	—	CategoryTheory.Limits.preservesColimits_of_natIso CategoryTheory.Limits.comp_preservesColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Limits.evaluation_preservesColimits
preservesLimits_forget 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits Action instCategory forget	—	CategoryTheory.Limits.preservesLimits_of_natIso CategoryTheory.Limits.comp_preservesLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.Limits.evaluationPreservesLimits
resComp_hom_app_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Action instCategory CategoryTheory.Functor.comp res MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category resComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct V	—	—
resComp_inv_app_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Action instCategory res MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Functor.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category resComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct V	—	—
resCongr_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor Action instCategory CategoryTheory.Functor.category res resCongr CategoryTheory.Functor.obj mkIso CategoryTheory.Iso.refl V	—	—
resCongr_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor Action instCategory CategoryTheory.Functor.category res resCongr CategoryTheory.Functor.obj mkIso CategoryTheory.Iso.refl V	—	—
resEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor Action instCategory resEquiv res MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike	—	—
resEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse Action instCategory resEquiv res MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm	—	—
resId_hom_app_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Action instCategory res MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category resId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct V	—	—
resId_inv_app_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Action instCategory CategoryTheory.Functor.id res MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category resId CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct V	—	—
res_map_hom 📖	mathematical	—	Hom.hom V MonoidHom.comp CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid ρ CategoryTheory.Functor.map Action instCategory res	—	—
res_obj_V 📖	mathematical	—	V CategoryTheory.Functor.obj Action instCategory res	—	—
res_obj_ρ 📖	mathematical	—	ρ CategoryTheory.Functor.obj Action instCategory res MonoidHom.comp CategoryTheory.End CategoryTheory.Category.toCategoryStruct V MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid	—	—
trivial_V 📖	mathematical	—	V trivial	—	—
trivial_ρ 📖	mathematical	—	ρ trivial MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid instOneMonoidHom	—	—
ρAut_apply_hom 📖	mathematical	—	CategoryTheory.Iso.hom V DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MonoidHom CategoryTheory.Aut MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Aut.instGroup MonoidHom.instFunLike ρAut CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.monoid ρ	—	—
ρAut_apply_inv 📖	mathematical	—	CategoryTheory.Iso.inv V DivInvMonoid.toMonoid Group.toDivInvMonoid DFunLike.coe MonoidHom CategoryTheory.Aut MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.Aut.instGroup MonoidHom.instFunLike ρAut CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.End.monoid ρ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
ρ_one 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct V MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike ρ MulOne.toOne CategoryTheory.CategoryStruct.id	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass

Action.FunctorCategoryEquivalence

Definitions

Name	Category	Theorems
counitIso 📖	CompOp	3 math math: counitIso_inv_app_app, Action.functorCategoryEquivalence_counitIso, counitIso_hom_app_app
functor 📖	CompOp	13 math math: counitIso_inv_app_app, functor_obj_obj, unitIso_inv_app_hom, functor_map_app, functor_δ, Action.functorCategoryEquivalence_functor, Action.instIsEquivalenceFunctorSingleObjFunctor, unitIso_hom_app_hom, counitIso_hom_app_app, functor_μ, functor_obj_map, functor_η, functor_ε
inverse 📖	CompOp	9 math math: Action.instIsEquivalenceFunctorSingleObjInverse, Action.functorCategoryEquivalence_inverse, counitIso_inv_app_app, unitIso_inv_app_hom, inverse_obj_ρ_apply, inverse_obj_V, unitIso_hom_app_hom, inverse_map_hom, counitIso_hom_app_app
unitIso 📖	CompOp	3 math math: Action.functorCategoryEquivalence_unitIso, unitIso_inv_app_hom, unitIso_hom_app_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counitIso_hom_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp Action Action.instCategory inverse functor CategoryTheory.Functor.id CategoryTheory.Iso.hom counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
counitIso_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp Action Action.instCategory inverse functor CategoryTheory.Iso.inv counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
functor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action.V DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ CategoryTheory.Functor.map Action Action.instCategory CategoryTheory.Functor CategoryTheory.Functor.category functor Action.Hom.hom	—	—
functor_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.obj Action Action.instCategory CategoryTheory.Functor CategoryTheory.Functor.category functor DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct Action.V MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ	—	—
functor_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category Action Action.instCategory CategoryTheory.Functor CategoryTheory.Functor.category functor Action.V	—	—
inverse_map_hom 📖	mathematical	—	Action.Hom.hom CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MulOne.toOne CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category Action Action.instCategory inverse CategoryTheory.NatTrans.app	—	—
inverse_obj_V 📖	mathematical	—	Action.V CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category Action Action.instCategory inverse	—	—
inverse_obj_ρ_apply 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.SingleObj CategoryTheory.SingleObj.category MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ CategoryTheory.Functor CategoryTheory.Functor.category Action Action.instCategory inverse CategoryTheory.Functor.map	—	—
unitIso_hom_app_hom 📖	mathematical	—	Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category functor inverse CategoryTheory.NatTrans.app CategoryTheory.Iso.hom unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Action.V	—	—
unitIso_inv_app_hom 📖	mathematical	—	Action.Hom.hom CategoryTheory.Functor.obj Action Action.instCategory CategoryTheory.Functor.comp CategoryTheory.Functor CategoryTheory.SingleObj CategoryTheory.SingleObj.category CategoryTheory.Functor.category functor inverse CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Action.V	—	—

Action.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	1 math math: comp_hom
hom 📖	CompOp	71 math math: Action.leftRegularTensorIso_inv_hom, Action.neg_hom, Action.inv_hom_hom_assoc, Action.sum_hom, Action.diagonalSuccIsoTensorDiagonal_inv_hom, CategoryTheory.Functor.mapAction_δ_hom, comp_hom, Action.leftUnitor_inv_hom, Action.comp_hom, Action.whiskerRight_hom, Action.smul_hom, Action.FunctorCategoryEquivalence.unitIso_inv_app_hom, Action.FunctorCategoryEquivalence.functor_map_app, Action.hom_inv_hom, Action.mkIso_hom_hom, Action.resId_inv_app_hom, Action.instIsIsoHomInv, Rep.RepToAction_map_hom, CategoryTheory.Functor.mapAction_η_hom, Action.FintypeCat.toEndHom_apply, Action.hom_ext_iff, Action.hom_injective, Action.nsmul_hom, Action.diagonalSuccIsoTensorTrivial_inv_hom_apply, Action.id_hom, Action.sub_hom, CategoryTheory.Functor.mapAction_ε_hom, TannakaDuality.FiniteGroup.forget_map, id_hom, Action.leftRegularTensorIso_hom_hom, ContinuousCohomology.I_map_hom, Rep.ActionToRep_map, CategoryTheory.Functor.mapAction_μ_hom, Action.FintypeCat.quotientToEndHom_mk, Action.zero_hom, Action.res_map_hom, Action.instIsIsoHomHom, CategoryTheory.PreGaloisCategory.functorToAction_map, Action.add_hom, comm_assoc, Action.resComp_inv_app_hom, Action.FunctorCategoryEquivalence.unitIso_hom_app_hom, Action.hom_inv_hom_assoc, ext_iff, Action.tensorHom_hom, Action.inv_hom_hom, Action.associator_hom_hom, Action.mkIso_inv_hom, Action.FintypeCat.quotientToQuotientOfLE_hom_mk, Action.FunctorCategoryEquivalence.inverse_map_hom, Action.whiskerLeft_hom, Representation.linearizeMap_single, Action.zsmul_hom, Action.β_inv_hom, Action.diagonalSuccIsoTensorDiagonal_hom_hom, Action.resId_hom_app_hom, Action.rightUnitor_hom_hom, Action.diagonalSuccIsoTensorTrivial_hom_hom_apply, Representation.linearizeMap_toLinearMap, CategoryTheory.Functor.mapAction_map_hom, Action.associator_inv_hom, Action.rightUnitor_inv_hom, Action.resComp_hom_app_hom, TannakaDuality.FiniteGroup.ofRightFDRep_hom, comm, Action.comp_hom_assoc, ContinuousCohomology.const_app_hom, FDRep.dualTensorIsoLinHom_hom_hom, Action.β_hom_hom, Action.leftUnitor_hom_hom, Action.forget_map
id 📖	CompOp	1 math math: id_hom
instInhabited 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Action.V DFunLike.coe MonoidHom CategoryTheory.End MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ hom	—	—
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Action.V DFunLike.coe MonoidHom CategoryTheory.End MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
comp_hom 📖	mathematical	—	hom comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Action.V	—	—
ext 📖	—	hom	—	—	—
ext_iff 📖	mathematical	—	hom	—	ext
id_hom 📖	mathematical	—	hom id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Action.V	—	—

Action.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_ρ 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct Action.V MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ MulEquiv CategoryTheory.Functor.obj Action Action.instCategory Action.forget CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike CategoryTheory.Iso.conj CategoryTheory.Functor.mapIso	—	CategoryTheory.Iso.conj_apply CategoryTheory.Iso.eq_inv_comp Action.Hom.comm

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
mapAction 📖	CompOp	2 math math: mapAction_functor, mapAction_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapAction_functor 📖	mathematical	—	functor Action Action.instCategory mapAction CategoryTheory.Functor.mapAction	—	—
mapAction_inverse 📖	mathematical	—	inverse Action Action.instCategory mapAction CategoryTheory.Functor.mapAction	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapAction 📖	CompOp	29 math math: mapAction_δ_hom, Action.Functor.mapActionPreservesLimitsOfShapeOfPreserves, mapContActionCongr_inv, mapActionComp_hom, Action.Functor.mapActionPreservesLimit_of_preserves, mapContActionCongr_hom, mapActionComp_inv, Action.Functor.mapActionPreservesColimit_of_preserves, CategoryTheory.Equivalence.mapAction_functor, Action.Functor.instPreservesFiniteLimitsMapActionOfHasFiniteLimits, mapAction_η_hom, mapContAction_map, mapAction_obj_ρ_apply, mapAction_linear, mapAction_ε_hom, mapAction_obj_V, mapAction_preadditive, mapAction_μ_hom, instFullActionMapActionOfFaithful, Action.Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits, mapActionCongr_inv, Action.Functor.preservesLimitsOfSize_of_preserves, mapActionCongr_hom, Action.Functor.preservesColimitsOfSize_of_preserves, mapAction_map_hom, Action.Functor.mapActionPreservesColimitsOfShapeOfPreserves, mapContAction_obj_obj, CategoryTheory.Equivalence.mapAction_inverse, instFaithfulActionMapAction
mapActionComp 📖	CompOp	2 math math: mapActionComp_hom, mapActionComp_inv
mapActionCongr 📖	CompOp	2 math math: mapActionCongr_inv, mapActionCongr_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulActionMapAction 📖	mathematical	—	Faithful Action Action.instCategory mapAction	—	Action.hom_ext map_injective
instFullActionMapActionOfFaithful 📖	mathematical	—	Full Action Action.instCategory mapAction	—	FullyFaithful.full
mapActionComp_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor Action Action.instCategory category mapAction comp mapActionComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Iso.refl	—	—
mapActionComp_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor Action Action.instCategory category mapAction comp mapActionComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct obj CategoryTheory.Iso.refl	—	—
mapActionCongr_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor Action Action.instCategory category mapAction mapActionCongr obj Action.mkIso CategoryTheory.Iso.app Action.V	—	—
mapActionCongr_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor Action Action.instCategory category mapAction mapActionCongr obj Action.mkIso CategoryTheory.Iso.app Action.V	—	—
mapAction_map_hom 📖	mathematical	—	Action.Hom.hom obj Action.V CategoryTheory.End CategoryTheory.Category.toCategoryStruct MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MulOne.toOne map DFunLike.coe MonoidHom MonoidHom.instFunLike Action.ρ Action Action.instCategory mapAction	—	—
mapAction_obj_V 📖	mathematical	—	Action.V obj Action Action.instCategory mapAction	—	—
mapAction_obj_ρ_apply 📖	mathematical	—	DFunLike.coe MonoidHom CategoryTheory.End CategoryTheory.Category.toCategoryStruct obj Action.V MulOneClass.toMulOne Monoid.toMulOneClass CategoryTheory.End.monoid MonoidHom.instFunLike Action.ρ Action Action.instCategory mapAction map	—	—

CategoryTheory.Functor.FullyFaithful

Definitions

Name	Category	Theorems
mapAction 📖	CompOp	—

---

← Back to Index