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	20 math math: DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV, Rep.norm_comm_apply, forget₂_preservesZeroMorphisms, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.standardComplex.εToSingle₀_comp_eq, Rep.applyAsHom_comm_apply, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, FDRep.forget₂_ρ, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, isContinuous_def, Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV, forget₂_linear, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, forget₂_additive, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
V 📖	CompOp	651 math math: resCongr_inv, Rep.resCoindHomEquiv_symm_apply_hom, Representation.repOfTprodIso_inv_apply, Rep.resCoindHomEquiv_apply_hom, groupCohomology.instEpiModuleCatH2π, DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, groupHomology.π_comp_H2Iso_hom_assoc, Rep.invariantsAdjunction_homEquiv_symm_apply_hom, Rep.coe_linearization_obj_ρ, groupHomology.mapCycles₂_comp_assoc, groupCohomology.toCocycles_comp_isoCocycles₁_hom, Rep.MonoidalClosed.linearHomEquiv_symm_hom, leftRegularTensorIso_inv_hom, groupCohomology.isoCocycles₁_hom_comp_i_apply, neg_hom, groupCohomology.mem_cocycles₂_def, ContinuousCohomology.I_obj_V_isAddCommGroup, groupHomology.coinfNatTrans_app, groupCohomology.d₂₃_hom_apply, inv_hom_hom_assoc, groupHomology.d₁₀_single_one, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV, groupHomology.boundaries₂_le_cycles₂, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, sum_hom, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, Rep.diagonalSuccIsoFree_inv_hom_single, groupCohomology.d₀₁_comp_d₁₂, Representation.repOfTprodIso_apply, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, ContinuousCohomology.I_obj_V_carrier, groupCohomology.cocyclesIso₀_hom_comp_f, Rep.resCoindAdjunction_counit_app_hom_hom, groupHomology.d₃₂_single, ofMulAction_apply, groupCohomology.eq_d₀₁_comp_inv, groupCohomology.H1π_comp_map_assoc, groupHomology.mapCycles₁_comp_apply, groupHomology.cyclesIso₀_inv_comp_iCycles_apply, Rep.leftRegularHom_hom, groupCohomology.π_comp_H0Iso_hom, FDRep.endRingEquiv_symm_comp_ρ, groupHomology.H0IsoOfIsTrivial_inv_eq_π, groupCohomology.π_comp_H1Iso_hom_assoc, CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected, groupCohomology.eq_d₁₂_comp_inv, Rep.indToCoindAux_self, groupCohomology.mapCocycles₂_comp_i, groupHomology.eq_d₃₂_comp_inv, diagonalSuccIsoTensorDiagonal_inv_hom, Rep.coe_res_obj_ρ, Rep.invariantsFunctor_obj_carrier, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, CategoryTheory.Functor.mapAction_δ_hom, Rep.diagonalHomEquiv_symm_apply, tensorObj_V, groupCohomology.H0IsoOfIsTrivial_hom, TannakaDuality.FiniteGroup.forget_obj, Hom.comp_hom, groupCohomology.coe_mapCocycles₁, groupHomology.mem_cycles₂_iff, groupHomology.cyclesMap_comp_isoCycles₂_hom, groupCohomology.d₁₂_hom_apply, groupHomology.comp_d₂₁_eq, groupCohomology.coboundariesToCocycles₁_apply, groupHomology.mapCycles₁_comp_assoc, leftUnitor_inv_hom, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, comp_hom, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, groupHomology.H0π_comp_map, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, rightDual_ρ, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, groupCohomology.comp_d₁₂_eq, groupCohomology.mem_cocycles₁_of_addMonoidHom, groupCohomology.cocycles₂.d₂₃_apply, groupCohomology.d₀₁_hom_apply, Rep.linearization_single, groupHomology.d₃₂_single_one_thd, whiskerRight_hom, groupHomology.isoCycles₁_inv_comp_iCycles_apply, groupCohomology.dArrowIso₀₁_inv_right, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.d₁₂_comp_d₂₃_apply, groupCohomology.H0IsoOfIsTrivial_inv_apply, groupCohomology.eq_d₂₃_comp_inv_assoc, Rep.finsuppToCoinvariantsTensorFree_single, groupCohomology.eq_d₂₃_comp_inv_apply, CategoryTheory.Functor.mapContActionCongr_inv, groupCohomology.eq_d₁₂_comp_inv_apply, groupHomology.chains₁ToCoinvariantsKer_surjective, FunctorCategoryEquivalence.functor_obj_obj, Rep.coinvariantsTensorFreeLEquiv_symm_apply, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, groupHomology.cycles₁_eq_top_of_isTrivial, groupHomology.π_comp_H0Iso_hom_assoc, Rep.resCoindAdjunction_unit_app_hom_hom, groupHomology.d₃₂_comp_d₂₁_assoc, groupCohomology.mem_cocycles₁_def, Rep.instEpiModuleCatHom, Rep.homEquiv_apply_hom, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupHomology.d₁₀ArrowIso_hom_left, Rep.norm_comm_apply, forget₂_preservesZeroMorphisms, groupHomology.cycles₁IsoOfIsTrivial_hom_apply, smul_hom, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, groupCohomology.coboundaries₁_eq_bot_of_isTrivial, groupHomology.d₂₁_single_inv_mul_ρ_add_single, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, groupCohomology.cocycles₂_map_one_fst, Rep.indCoindIso_inv_hom_hom, groupCohomology.mapCocycles₂_comp_i_assoc, groupHomology.d₁₀_comp_coinvariantsMk_apply, Rep.ρ_hom, Rep.diagonalSuccIsoFree_inv_hom_single_single, groupCohomology.H1IsoOfIsTrivial_inv_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃, groupHomology.mapCycles₁_id_comp_assoc, groupHomology.eq_d₂₁_comp_inv, CategoryTheory.Functor.mapContActionCongr_hom, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, groupCohomology.H2π_comp_map_apply, groupHomology.mapCycles₁_comp, FunctorCategoryEquivalence.unitIso_inv_app_hom, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.ihom_ev_app_hom, FunctorCategoryEquivalence.functor_map_app, groupCohomology.dArrowIso₀₁_hom_right, Rep.MonoidalClosed.linearHomEquivComm_hom, groupCohomology.toCocycles_comp_isoCocycles₂_hom, Rep.coe_linearization_obj, ContinuousCohomology.I_obj_ρ_apply, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, groupHomology.mapCycles₁_comp_i, groupCohomology.shortComplexH0_f, groupCohomology.cocyclesOfIsCocycle₁_coe, groupCohomology.coboundaries₂_le_cocycles₂, Rep.standardComplex.εToSingle₀_comp_eq, Rep.coindVEquiv_symm_apply_coe, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, Rep.indCoindIso_hom_hom_hom, groupCohomology.comp_d₂₃_eq, groupCohomology.coboundaries₂.val_eq_coe, hom_inv_hom, Rep.ofModuleMonoidAlgebra_obj_coe, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupCohomology.infNatTrans_app, groupCohomology.d₁₂_apply_mem_cocycles₂, Rep.invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, groupCohomology.d₀₁_apply_mem_cocycles₁, Rep.indToCoindAux_fst_mul_inv, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, Rep.coinvariantsFunctor_obj_carrier, Rep.applyAsHom_comm_apply, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, groupHomology.chainsMap_f_single, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, groupCohomology.subtype_comp_d₀₁_apply, ContinuousCohomology.Iobj_ρ_apply, groupCohomology.H2π_eq_iff, groupCohomology.comp_d₀₁_eq, mkIso_hom_hom, groupCohomology.cocycles₂_map_one_snd, Rep.coinvariantsTensorFreeLEquiv_apply, groupHomology.toCycles_comp_isoCycles₁_hom_apply, TannakaDuality.FiniteGroup.sumSMulInv_apply, groupHomology.mapCycles₂_comp_i, groupCohomology.map_H0Iso_hom_f, groupHomology.boundariesOfIsBoundary₁_coe, resId_inv_app_hom, FDRep.instFiniteDimensionalCarrierVFGModuleCat, Rep.indToCoindAux_comm, groupCohomology.dArrowIso₀₁_inv_left, groupCohomology.π_comp_H1Iso_hom, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, ContinuousCohomology.I_obj_V_isModule, groupHomology.cyclesIso₀_comp_H0π_apply, groupHomology.eq_d₃₂_comp_inv_apply, FDRep.average_char_eq_finrank_invariants, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, Rep.toAdditive_symm_apply, groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂, instIsIsoHomInv, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, Rep.ofMulDistribMulAction_ρ_apply_apply, Rep.instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ, groupCohomology.instEpiModuleCatH1π, groupCohomology.H2π_comp_map, groupHomology.π_comp_H2Iso_hom, Rep.indResAdjunction_counit_app_hom_hom, FDRep.hom_hom_action_ρ, CategoryTheory.Functor.mapAction_obj_ρ_apply, FintypeCat.toEndHom_apply, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, Rep.coindToInd_apply, groupHomology.mapCycles₁_comp_i_apply, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, ContAction.resCongr_hom, Rep.coe_of, groupCohomology.isoCocycles₂_hom_comp_i, groupCohomology.π_comp_H0Iso_hom_apply, groupHomology.coe_mapCycles₂, hom_injective, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, nsmul_hom, groupHomology.comp_d₁₀_eq, groupHomology.H1π_comp_map_apply, groupHomology.H0π_comp_map_assoc, groupCohomology.dArrowIso₀₁_hom_left, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, groupHomology.π_comp_H0Iso_hom_apply, groupCohomology.eq_d₀₁_comp_inv_apply, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.cocycles₁_map_inv, Rep.freeLiftLEquiv_apply, groupCohomology.mapCocycles₁_one, groupHomology.H2π_comp_map_assoc, Rep.indToCoindAux_mul_fst, groupHomology.π_comp_H0IsoOfIsTrivial_hom_apply, id_hom, Rep.ihom_obj_ρ_apply, sub_hom, groupHomology.d₁₀ArrowIso_inv_right, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, TannakaDuality.FiniteGroup.equivApp_inv, Rep.finsuppTensorRight_hom_hom, groupCohomology.norm_ofAlgebraAutOnUnits_eq, groupCohomology.π_comp_H0Iso_hom_assoc, CategoryTheory.Functor.mapAction_obj_V, groupCohomology.mem_cocycles₂_iff, Rep.tensor_ρ, Rep.toAdditive_apply, groupCohomology.H2π_comp_map_assoc, groupHomology.d₁₀_comp_coinvariantsMk, groupHomology.d₂₁_comp_d₁₀_apply, groupHomology.mapCycles₂_comp_apply, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, Rep.ofDistribMulAction_ρ_apply_apply, groupCohomology.d₀₁_ker_eq_invariants, Rep.linearization_η_hom_apply, res_obj_V, Rep.leftRegularHomEquiv_symm_apply, TannakaDuality.FiniteGroup.equivApp_hom, FDRep.char_linHom, forget_obj, groupHomology.H2π_eq_iff, groupHomology.H1AddEquivOfIsTrivial_single, groupCohomology.mem_cocycles₁_iff, groupHomology.range_d₁₀_eq_coinvariantsKer, groupCohomology.inhomogeneousCochains.d_comp_d, groupHomology.isoCycles₂_hom_comp_i_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, rightDual_v, Rep.coinvariantsShortComplex_f, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, Hom.id_hom, groupCohomology.isoCocycles₁_inv_comp_iCocycles, groupHomology.π_comp_H0IsoOfIsTrivial_hom, leftRegularTensorIso_hom_hom, groupHomology.eq_d₂₁_comp_inv_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, ContinuousCohomology.I_map_hom, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, groupHomology.inhomogeneousChains.d_single, groupCohomology.coboundariesOfIsCoboundary₁_coe, groupHomology.cyclesIso₀_inv_comp_iCycles, CategoryTheory.Functor.mapAction_μ_hom, Representation.coind'_apply_apply, groupCohomology.d₁₂_comp_d₂₃_assoc, FintypeCat.quotientToEndHom_mk, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.π_comp_H1Iso_hom_apply, Rep.coindIso_inv_hom_hom, zero_hom, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.cocycles₁_map_mul_of_isTrivial, groupCohomology.subtype_comp_d₀₁_assoc, groupHomology.chainsMap_id_f_hom_eq_mapRange, groupHomology.toCycles_comp_isoCycles₂_hom, groupCohomology.map_id_comp_H0Iso_hom, groupHomology.cyclesMap_comp_isoCycles₂_hom_apply, groupHomology.mapCycles₁_id_comp, Rep.trivialFunctor_obj_V, Rep.indToCoindAux_mul_snd, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, groupCohomology.cocyclesOfIsMulCocycle₂_coe, groupHomology.eq_d₁₀_comp_inv, Rep.diagonalSuccIsoTensorTrivial_hom_hom_single, groupHomology.isoShortComplexH1_inv, res_map_hom, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, groupHomology.eq_d₁₀_comp_inv_assoc, groupCohomology.d₁₂_comp_d₂₃, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, Rep.linearization_obj_ρ, Rep.toCoinvariantsMkQ_hom, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, groupHomology.isoCycles₁_hom_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, instIsIsoHomHom, groupCohomology.H1π_eq_zero_iff, groupHomology.H1AddEquivOfIsTrivial_symm_apply, Rep.invariantsAdjunction_counit_app_hom, groupHomology.cyclesMap_comp_cyclesIso₀_hom, groupCohomology.cochainsMap_f, groupCohomology.coboundaries₁.val_eq_coe, groupHomology.d₃₂_single_one_fst, inhomogeneousCochains.d_hom_apply, Rep.coind'_ext_iff, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, groupHomology.d₂₁_comp_d₁₀, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, groupHomology.H1ToTensorOfIsTrivial_H1π_single, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, groupCohomology.cocyclesMk₁_eq, ρ_self_inv_apply, Rep.linearizationTrivialIso_inv_hom, groupHomology.cyclesOfIsCycle₁_coe, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, Rep.quotientToInvariantsFunctor_obj_V, FDRep.char_one, groupHomology.inhomogeneousChains.ext_iff, ρ_one, groupHomology.d₂₁_apply_mem_cycles₁, groupCohomology.coboundariesToCocycles₂_apply, add_hom, ρAut_apply_hom, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, groupHomology.cyclesMap_comp_isoCycles₁_hom_apply, groupHomology.toCycles_comp_isoCycles₂_hom_apply, groupCohomology.cocyclesOfIsMulCocycle₁_coe, groupCohomology.H2π_eq_zero_iff, groupCohomology.mapCocycles₁_comp_i_assoc, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, groupCohomology.cocycles₁.val_eq_coe, TannakaDuality.FiniteGroup.sumSMulInv_single_id, groupCohomology.H1π_comp_map_apply, Rep.leftRegularHom_hom_single, groupCohomology.cocycles₁_map_one, groupHomology.eq_d₃₂_comp_inv_assoc, CategoryTheory.FintypeCat.Action.isConnected_iff_transitive, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, CategoryTheory.Functor.mapActionCongr_inv, groupCohomology.π_comp_H2Iso_hom_assoc, Hom.comm_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, Rep.finsuppTensorRight_inv_hom, Rep.coinvariantsMk_app_hom, Rep.ihom_obj_V_isAddCommGroup, groupHomology.mapCycles₂_hom, groupHomology.isoCycles₂_inv_comp_iCycles_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, Rep.coindVEquiv_apply_hom, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, FunctorCategoryEquivalence.inverse_obj_V, groupHomology.H1π_eq_zero_iff, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, groupHomology.π_comp_H1Iso_hom_assoc, groupHomology.chainsMap_f_2_comp_chainsIso₂, groupHomology.d₂₁_single_one_fst, resComp_inv_app_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.H2π_comp_map, groupCohomology.cocycles₂.val_eq_coe, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, groupCohomology.eq_d₂₃_comp_inv, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, FunctorCategoryEquivalence.unitIso_hom_app_hom, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.H1π_comp_map_assoc, hom_inv_hom_assoc, Rep.ihom_map_hom, groupHomology.instEpiModuleCatH1π, tensorHom_hom, inv_hom_hom, groupHomology.H1AddEquivOfIsTrivial_apply, groupCohomology.isoCocycles₂_inv_comp_iCocycles, Rep.coinvariantsTensor_hom_ext_iff, Rep.finsuppTensorLeft_inv_hom, associator_hom_hom, res_obj_ρ, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, Rep.unit_iso_comm, Rep.leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, groupHomology.instEpiModuleCatH2π, CategoryTheory.Functor.mapActionCongr_hom, groupCohomology.cocyclesMk₂_eq, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, groupHomology.H1π_comp_map, groupHomology.chainsMap_f_hom, groupHomology.d₃₂_apply_mem_cycles₂, mkIso_inv_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, Rep.indResAdjunction_unit_app_hom_hom, Rep.ofHom_ρ, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, groupHomology.map_id_comp_H0Iso_hom_apply, groupHomology.boundariesOfIsBoundary₂_coe, FintypeCat.quotientToQuotientOfLE_hom_mk, groupHomology.cyclesMk₁_eq, groupHomology.cyclesIso₀_comp_H0π_assoc, groupHomology.mapCycles₂_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i, Rep.Action_ρ_eq_ρ, Rep.linearization_δ_hom, groupHomology.instEpiModuleCatH0π, ContAction.resCongr_inv, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, whiskerLeft_hom, groupCohomology.mapCocycles₁_comp_i_apply, Rep.coindMap_hom, groupHomology.mapCycles₂_id_comp_apply, zsmul_hom, Rep.trivial_def, groupCohomology.cocycles₂_ext_iff, Rep.MonoidalClosed.linearHomEquiv_hom, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, Rep.invariantsAdjunction_homEquiv_apply_hom, Rep.hom_comm_apply, groupHomology.H2π_comp_map_apply, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, groupCohomology.cochainsMap_f_hom, groupCohomology.coboundaries₁_ext_iff, Rep.finsuppTensorLeft_hom_hom, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.inhomogeneousChains.d_comp_d, groupHomology.π_comp_H0Iso_hom, groupCohomology.π_comp_H2Iso_hom_apply, Rep.coinvariantsTensorMk_apply, groupHomology.cyclesIso₀_inv_comp_cyclesMap, Rep.indMap_hom, tensorUnit_V, ContinuousCohomology.I_obj_V_topologicalSpace, groupHomology.H0π_comp_H0Iso_hom, groupHomology.isoCycles₁_hom_comp_i_assoc, Rep.homEquiv_symm_apply_hom, Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, FDRep.forget₂_ρ, Rep.invariantsFunctor_map_hom, groupHomology.d₁₀_eq_zero_of_isTrivial, groupCohomology.π_comp_H1Iso_hom_apply, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupCohomology.d₀₁_comp_d₁₂_assoc, tensor_ρ, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, groupHomology.d₂₁_single_one_snd, groupHomology.π_comp_H0IsoOfIsTrivial_hom_assoc, FDRep.instFiniteCarrierVFGModuleCat, groupHomology.d₃₂_comp_d₂₁, groupHomology.d₃₂_single_one_snd, groupHomology.π_comp_H2Iso_hom_apply, FDRep.Iso.conj_ρ, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Rep.ihom_coev_app_hom, groupHomology.mapCycles₁_hom, β_inv_hom, Rep.leftRegularHomEquiv_apply, groupHomology.isoCycles₁_inv_comp_iCycles, diagonalSuccIsoTensorDiagonal_hom_hom, FDRep.char_dual, resId_hom_app_hom, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, groupHomology.isoShortComplexH2_inv, groupHomology.coe_mapCycles₁, rightUnitor_hom_hom, groupHomology.toCycles_comp_isoCycles₁_hom, groupCohomology.d₀₁_comp_d₁₂_apply, leftDual_v, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, Representation.linHom.mem_invariants_iff_comm, groupHomology.mapCycles₂_comp_i_apply, groupCohomology.cocyclesIso₀_hom_comp_f_apply, groupHomology.boundariesToCycles₂_apply, groupCohomology.subtype_comp_d₀₁, groupHomology.cyclesOfIsCycle₂_coe, Rep.freeLift_hom, groupHomology.isoCycles₂_hom_comp_i, isContinuous_def, groupHomology.π_comp_H1Iso_hom, groupHomology.isoCycles₂_inv_comp_iCycles, CategoryTheory.Functor.mapAction_map_hom, groupHomology.d₁₀_single_inv, groupHomology.mkH1OfIsTrivial_apply, Rep.indToCoindAux_snd_mul_inv, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, Rep.res_obj_ρ, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, associator_inv_hom, groupCohomology.coboundaries₁_le_cocycles₁, Rep.ihom_obj_V_isModule, groupHomology.d₁₀ArrowIso_hom_right, Rep.freeLift_hom_single_single, Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, groupHomology.single_one_mem_boundaries₁, leftDual_ρ, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, groupHomology.cyclesIso₀_comp_H0π, groupCohomology.isoCocycles₂_hom_comp_i_apply, Rep.diagonalHomEquiv_apply, groupHomology.d₂₁_single, Rep.freeLiftLEquiv_symm_apply, groupHomology.inhomogeneousChains.d_eq, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, groupHomology.eq_d₂₁_comp_inv_apply, Rep.epi_iff_surjective, groupCohomology.coboundaries₂_ext_iff, groupHomology.d₁₀_comp_coinvariantsMk_assoc, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, Rep.indToCoindAux_of_not_rel, groupCohomology.cocyclesOfIsCocycle₂_coe, groupHomology.cyclesMk₀_eq, groupHomology.isoCycles₁_hom_comp_i, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, Rep.applyAsHom_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupHomology.H0π_comp_H0Iso_hom_assoc, groupCohomology.H1π_comp_map, Iso.conj_ρ, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, rightUnitor_inv_hom, Rep.indResHomEquiv_apply_hom, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupCohomology.cocyclesMk₀_eq, groupHomology.lsingle_comp_chainsMap_f_assoc, Rep.linearizationTrivialIso_hom_hom, groupHomology.single_mem_cycles₂_iff, groupCohomology.isoShortComplexH1_inv, groupHomology.boundaries₁_le_cycles₁, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, Rep.diagonalSuccIsoFree_hom_hom_single, Rep.ihom_obj_ρ, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, Rep.free_ext_iff, resComp_hom_app_hom, Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, groupCohomology.cocycles₁_ext_iff, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV, TannakaDuality.FiniteGroup.ofRightFDRep_hom, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, groupCohomology.eq_d₁₂_comp_inv_assoc, Representation.linHom.invariantsEquivRepHom_apply_hom, groupCohomology.H1InfRes_f, forget₂_linear, FunctorCategoryEquivalence.functor_obj_map, groupHomology.d₁₀ArrowIso_inv_left, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, groupHomology.single_mem_cycles₁_iff, Rep.coinvariantsFunctor_map_hom, ρAut_apply_inv, groupHomology.d₂₁_single_ρ_add_single_inv_mul, Hom.comm, ρ_inv_self_apply, Rep.linearization_map_hom_single, comp_hom_assoc, groupCohomology.isoShortComplexH2_inv, groupCohomology.map_id_comp_H0Iso_hom_assoc, groupCohomology.isoCocycles₂_hom_comp_i_assoc, groupHomology.eq_d₁₀_comp_inv_apply, Rep.ihom_obj_V_carrier, ContinuousCohomology.const_app_hom, ofMulAction_V, Rep.coindIso_hom_hom_hom, groupHomology.H0π_comp_H0Iso_hom_apply, Rep.barComplex.d_single, FDRep.hom_action_ρ, Rep.mono_iff_injective, FDRep.dualTensorIsoLinHom_hom_hom, Rep.instMonoModuleCatHom, groupHomology.d₂₁_comp_d₁₀_assoc, groupCohomology.coe_mapCocycles₂, groupCohomology.eq_d₀₁_comp_inv_assoc, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, groupCohomology.H1π_eq_iff, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, groupCohomology.isoCocycles₁_hom_comp_i_assoc, resCongr_hom, CategoryTheory.PreGaloisCategory.instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, groupHomology.mapCycles₁_quotientGroupMk'_epi, groupHomology.mapCycles₁_comp_i_assoc, groupHomology.H0π_comp_map_apply, trivial_V, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, groupCohomology.coboundariesOfIsCoboundary₂_coe, Rep.FiniteCyclicGroup.resolution.π_f, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, FDRep.endRingEquiv_comp_ρ, Rep.linearization_map_hom, β_hom_hom, groupHomology.mem_cycles₁_iff, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, groupCohomology.mapCocycles₁_comp_i, groupHomology.boundariesToCycles₁_apply, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, leftUnitor_hom_hom, groupCohomology.cocycles₁.d₁₂_apply, Rep.indResHomEquiv_symm_apply_hom, forget₂_additive, groupHomology.isoCycles₂_hom_comp_i_assoc, groupHomology.comp_d₃₂_eq, groupCohomology.π_comp_H2Iso_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀, groupHomology.H2π_eq_zero_iff, Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, Rep.linearization_μ_hom, FintypeCat.ofMulAction_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.H1π_eq_iff, groupHomology.d₃₂_comp_d₂₁_apply, groupHomology.chainsMap_f, Rep.quotientToCoinvariantsFunctor_obj_V, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupHomology.cyclesMap_comp_isoCycles₁_hom, groupCohomology.d₀₁_eq_zero, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
actionPUnitEquivalence 📖	CompOp	—
actionPunitEquivalence 📖	CompOp	—
forget 📖	CompOp	44 math math: forget_η, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget, instReflectsLimitsOfShapeForget, groupHomology.π_comp_H0Iso_hom_assoc, forget_preservesZeroMorphisms, instPreservesColimitForgetOfHasColimitComp, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, preservesColimits_forget, groupHomology.coinvariantsMk_comp_H0Iso_inv, instPreservesFiniteLimitsForgetOfHasFiniteLimits, Rep.coinvariantsFunctor_hom_ext_iff, instFaithfulForget, Rep.instEpiModuleCatAppActionCoinvariantsMk, forget_δ, preservesLimits_forget, groupHomology.d₁₀_comp_coinvariantsMk, instPreservesLimitForgetOfHasLimitComp, forget_obj, forget_additive, instPreservesFiniteColimitsForgetOfHasFiniteColimits, instReflectsColimitsForget, instReflectsColimitsOfShapeForget, instPreservesLimitsOfShapeForgetOfHasLimitsOfShape, Rep.coinvariantsMk_app_hom, forget_ε, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, instReflectsLimitsForget, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, groupHomology.π_comp_H0Iso_hom, groupHomology.H0π_comp_H0Iso_hom, forget_linear, forget_μ, groupHomology.shortComplexH0_g, Rep.coinvariantsAdjunction_unit_app_hom, instReflectsLimitForget, groupHomology.d₁₀_comp_coinvariantsMk_assoc, groupHomology.H0π_comp_H0Iso_hom_assoc, Iso.conj_ρ, instPreservesColimitsOfShapeForgetOfHasColimitsOfShape, Rep.coinvariantsAdjunction_homEquiv_apply_hom, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, instReflectsColimitForget, forget_map
functorCategoryEquivalence 📖	CompOp	25 math math: Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, functorCategoryEquivalence_inverse, functorCategoryEquivalence_unitIso, leftUnitor_inv_hom, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, whiskerRight_hom, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, Rep.homEquiv_apply_hom, Rep.MonoidalClosed.linearHomEquivComm_hom, functorCategoryEquivalence_functor, diagonalSuccIsoTensorTrivial_inv_hom_apply, functorCategoryEquivalence_counitIso, tensorHom_hom, associator_hom_hom, whiskerLeft_hom, Rep.MonoidalClosed.linearHomEquiv_hom, Rep.homEquiv_symm_apply_hom, Rep.ihom_coev_app_hom, rightUnitor_hom_hom, associator_inv_hom, functorCategoryEquivalence_linear, functorCategoryEquivalence_preservesZeroMorphisms, rightUnitor_inv_hom, functorCategoryEquivalence_additive, leftUnitor_hom_hom
functorCategoryEquivalenceCompEvaluation 📖	CompOp	—
hasForgetToV 📖	CompOp	10 math math: forget₂_preservesZeroMorphisms, Rep.standardComplex.εToSingle₀_comp_eq, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV, forget₂_linear, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, forget₂_additive, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
inhabited' 📖	CompOp	—
instCategory 📖	CompOp	582 math math: resCongr_inv, forget_η, Rep.resCoindHomEquiv_symm_apply_hom, Representation.repOfTprodIso_inv_apply, Rep.resCoindHomEquiv_apply_hom, DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, Rep.invariantsAdjunction_homEquiv_symm_apply_hom, Rep.coe_linearization_obj_ρ, groupHomology.mapCycles₂_comp_assoc, instIsEquivalenceFunctorSingleObjInverse, Rep.MonoidalClosed.linearHomEquiv_symm_hom, leftRegularTensorIso_inv_hom, neg_hom, groupHomology.map₁_quotientGroupMk'_epi, ContinuousCohomology.I_obj_V_isAddCommGroup, groupHomology.coinfNatTrans_app, groupHomology.mapShortComplexH2_id, inv_hom_hom_assoc, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, sum_hom, Rep.diagonalSuccIsoFree_inv_hom_single, groupCohomology.cocyclesMap_id_comp_assoc, Representation.repOfTprodIso_apply, Rep.coindResAdjunction_counit_app, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, ContinuousCohomology.I_obj_V_carrier, Rep.resCoindAdjunction_counit_app_hom_hom, groupHomology.mapCycles₁_comp_apply, groupHomology.mapShortComplexH1_zero, groupHomology.cyclesMap_id_comp, Rep.indFunctor_obj, groupHomology.mapShortComplexH2_zero, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget, Rep.indCoindNatIso_hom_app, groupHomology.chainsMap_id, diagonalSuccIsoTensorDiagonal_inv_hom, Rep.coe_res_obj_ρ, Rep.invariantsFunctor_obj_carrier, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, Rep.barComplex.d_def, CategoryTheory.Functor.mapAction_δ_hom, Functor.mapActionPreservesLimitsOfShapeOfPreserves, Rep.diagonalHomEquiv_symm_apply, tensorObj_V, Rep.coindFunctor_map, functorCategoryEquivalence_inverse, instHasLimits, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, FunctorCategoryEquivalence.counitIso_inv_app_app, functorCategoryEquivalence_unitIso, Rep.instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, Rep.instIsRightAdjointCoindFunctor, groupHomology.mapCycles₁_comp_assoc, leftUnitor_inv_hom, comp_hom, Rep.instIsTrivialObjModuleCatTrivialFunctor, instHasFiniteProducts, groupHomology.H0π_comp_map, Rep.coinvariantsAdjunction_counit_app, rightDual_ρ, groupHomology.map_id, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, instHasFiniteCoproducts, groupCohomology.cochainsMap_comp, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, Rep.linearization_single, whiskerRight_hom, groupHomology.coresNatTrans_app, groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.congr, CategoryTheory.Functor.mapActionComp_hom, FunctorCategoryEquivalence.functor_obj_obj, Rep.coinvariantsTensorFreeLEquiv_symm_apply, Rep.standardComplex.d_eq, instReflectsLimitsOfShapeForget, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, groupHomology.π_comp_H0Iso_hom_assoc, Rep.resCoindAdjunction_unit_app_hom_hom, Rep.trivial_projective_of_subsingleton, groupHomology.H1CoresCoinfOfTrivial_X₁, Rep.homEquiv_apply_hom, groupCohomology.mapShortComplexH2_comp_assoc, Rep.FiniteCyclicGroup.chainComplexFunctor_obj, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, groupCohomology.mapCocycles₂_comp_i_apply, Functor.mapActionPreservesLimit_of_preserves, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, Rep.norm_comm_apply, forget₂_preservesZeroMorphisms, smul_hom, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, Rep.coinvariantsAdjunction_homEquiv_symm_apply_hom, Rep.indCoindIso_inv_hom_hom, Rep.free_projective, groupHomology.d₁₀_comp_coinvariantsMk_apply, Rep.diagonalSuccIsoFree_inv_hom_single_single, forget_preservesZeroMorphisms, Rep.instPreservesProjectiveObjectsActionModuleCatSubtypeMemSubgroupResSubtype, groupHomology.mapCycles₁_id_comp_assoc, Rep.instLinearModuleCatObjFunctorCoinvariantsTensor, groupHomology.mapCycles₁_comp, groupHomology.map_comp, FunctorCategoryEquivalence.unitIso_inv_app_hom, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.ihom_ev_app_hom, CategoryTheory.Functor.mapActionComp_inv, FunctorCategoryEquivalence.functor_map_app, Rep.MonoidalClosed.linearHomEquivComm_hom, Rep.coe_linearization_obj, Rep.instIsRightAdjointModuleCatInvariantsFunctor, groupCohomology.map_comp, groupHomology.map_id_comp, ContinuousCohomology.I_obj_ρ_apply, Rep.coinvariantsTensorIndIso_inv, groupHomology.functor_obj, instPreservesColimitForgetOfHasColimitComp, FunctorCategoryEquivalence.functor_δ, Rep.standardComplex.εToSingle₀_comp_eq, ContAction.resEquiv_inverse, Rep.coindVEquiv_symm_apply_coe, Rep.homEquiv_def, Rep.indCoindIso_hom_hom_hom, hom_inv_hom, CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction, groupHomology.H1CoresCoinf_X₁, Rep.ofModuleMonoidAlgebra_obj_coe, CategoryTheory.FintypeCat.instMonoActionFintypeCatImageComplementIncl, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupCohomology.infNatTrans_app, ContinuousCohomology.instLinearActionTopModuleCatInvariants, Rep.invariantsAdjunction_unit_app, groupHomology.mapCycles₂_id_comp, Rep.diagonal_succ_projective, groupHomology.cyclesMap_comp_assoc, Rep.instIsLeftAdjointActionModuleCatRes, Functor.mapActionPreservesColimit_of_preserves, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, Rep.coinvariantsFunctor_obj_carrier, Rep.applyAsHom_comm_apply, isIso_of_hom_isIso, groupHomology.chainsMap_f_single, CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, mkIso_hom_hom, preservesColimits_forget, Rep.instProjective, Rep.coinvariantsTensorFreeLEquiv_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv, CategoryTheory.PreGaloisCategory.functorToContAction_map, Rep.coinvariantsTensorIndIso_hom, groupCohomology.map_H0Iso_hom_f, Rep.barResolution_complex, CategoryTheory.Equivalence.mapAction_functor, resId_inv_app_hom, groupCohomology.cochainsMap_zero, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, Rep.coinvariantsTensorIndNatIso_inv_app, ContinuousCohomology.I_obj_V_isModule, CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction, Rep.instAdditiveModuleCatObjFunctorCoinvariantsTensor, Rep.coindResAdjunction_unit_app, instIsIsoHomInv, groupHomology.mapCycles₁_id_comp_apply, tensorUnit_ρ, groupCohomology.cochainsMap_id_comp, functorCategoryEquivalence_functor, groupCohomology.map_id, CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, groupCohomology.mapShortComplexH2_comp, Functor.instPreservesFiniteLimitsMapActionOfHasFiniteLimits, CategoryTheory.PreGaloisCategory.exists_lift_of_continuous, CategoryTheory.Functor.mapAction_η_hom, groupCohomology.cochainsMap_comp_assoc, instPreservesFiniteLimitsForgetOfHasFiniteLimits, Rep.indResAdjunction_counit_app_hom_hom, CategoryTheory.Functor.mapAction_obj_ρ_apply, FintypeCat.toEndHom_apply, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, groupHomology.mapCycles₁_comp_i_apply, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.mapCycles₂_comp, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, ContAction.resCongr_hom, Rep.resIndAdjunction_homEquiv_symm_apply, Rep.coinvariantsFunctor_hom_ext_iff, ContinuousCohomology.instAdditiveActionTopModuleCatInvariants, nsmul_hom, instFaithfulForget, classifyingSpaceUniversalCover_map, diagonalSuccIsoTensorTrivial_inv_hom_apply, Rep.instLinearModuleCatCoinvariantsFunctor, Rep.coindMap'_hom, preservesLimitsOfShape_of_preserves, CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected, CategoryTheory.Functor.mapAction_linear, Rep.normNatTrans_app, groupHomology.H0π_comp_map_assoc, CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCat, instIsEquivalenceFunctorSingleObjFunctor, res_additive, groupHomology.π_comp_H0Iso_hom_apply, groupCohomology.H1InfRes_X₃, Rep.applyAsHom_comm_assoc, Rep.instEpiModuleCatAppActionCoinvariantsMk, Rep.freeLiftLEquiv_apply, groupHomology.chainsFunctor_obj, Rep.instEnoughProjectives, groupCohomology.functor_obj, groupCohomology.cocyclesMap_comp, forget_δ, ContinuousCohomology.MultiInd.d_comp_d_assoc, FunctorCategoryEquivalence.inverse_obj_ρ_apply, hasLimitsOfShape, ContAction.res_obj_obj, id_hom, Rep.ihom_obj_ρ_apply, sub_hom, Rep.instPreservesZeroMorphismsModuleCatInvariantsFunctor, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, hasColimitsOfShape, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.finsuppTensorRight_hom_hom, groupCohomology.resNatTrans_app, preservesLimits_forget, CategoryTheory.Functor.mapAction_ε_hom, CategoryTheory.Functor.mapAction_obj_V, groupCohomology.mapShortComplexH2_zero, Rep.tensor_ρ, Rep.resIndAdjunction_homEquiv_apply, groupHomology.d₁₀_comp_coinvariantsMk, instPreservesLimitForgetOfHasLimitComp, groupHomology.mapCycles₂_comp_apply, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, Rep.linearization_η_hom_apply, res_obj_V, Rep.quotientToInvariantsFunctor_map_hom, groupHomology.chainsMap_id_comp, Rep.leftRegularHomEquiv_symm_apply, forget_obj, Rep.quotientToCoinvariantsFunctor_map_hom, groupCohomology.mapShortComplexH1_id, Rep.coinvariantsShortComplex_g, groupHomology.mapShortComplexH1_id_comp, groupHomology.mapShortComplexH1_comp, Rep.coindResAdjunction_homEquiv_apply, Rep.Tor_map, Rep.ofModuleMonoidAlgebra_obj_ρ, rightDual_v, Rep.coinvariantsShortComplex_f, Rep.resIndAdjunction_counit_app, ContAction.resComp_hom, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, CategoryTheory.Functor.mapAction_preadditive, leftRegularTensorIso_hom_hom, preservesColimitsOfSize_of_preserves, Rep.ofMulActionSubsingletonIsoTrivial_inv_hom, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, Rep.instIsLeftAdjointModuleCatCoinvariantsFunctor, ContinuousCohomology.I_map_hom, CategoryTheory.Functor.mapAction_μ_hom, Representation.coind'_apply_apply, Rep.diagonalOneIsoLeftRegular_inv_hom, FintypeCat.quotientToEndHom_mk, CategoryTheory.Functor.instFullActionMapActionOfFaithful, forget_additive, groupHomology.map_id_comp_H0Iso_hom_assoc, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupCohomology.mapShortComplexH2_id_comp_assoc, groupHomology.mapCycles₂_id_comp_assoc, Rep.coindIso_inv_hom_hom, zero_hom, groupHomology.mapShortComplexH2_comp, groupCohomology.map_id_comp_H0Iso_hom, groupHomology.mapCycles₁_id_comp, Rep.trivialFunctor_obj_V, Functor.instPreservesFiniteColimitsMapActionOfHasFiniteColimits, instPreservesFiniteColimitsForgetOfHasFiniteColimits, ContAction.resEquiv_functor, Rep.diagonalSuccIsoTensorTrivial_hom_hom_single, res_map_hom, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, Rep.linearization_obj_ρ, groupHomology.lsingle_comp_chainsMap_f, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, instIsIsoHomHom, Rep.invariantsAdjunction_counit_app_hom, groupHomology.cyclesMap_comp_cyclesIso₀_hom, groupCohomology.cochainsMap_f, Rep.coind'_ext_iff, instReflectsColimitsForget, groupHomology.chainsMap_comp, CategoryTheory.PreGaloisCategory.functorToAction_map, Rep.instLinearModuleCatInvariantsFunctor, instReflectsColimitsOfShapeForget, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, Rep.ofMulActionSubsingletonIsoTrivial_hom_hom, groupCohomology.map_id_comp_assoc, Rep.linearizationTrivialIso_inv_hom, Rep.isZero_Tor_succ_of_projective, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, Rep.quotientToInvariantsFunctor_obj_V, instPreservesLimitsOfShapeForgetOfHasLimitsOfShape, add_hom, Rep.coinvariantsTensorIndNatIso_hom_app, groupHomology.congr, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, Rep.applyAsHom_comm, instHasFiniteColimits, CategoryTheory.FintypeCat.Action.isConnected_iff_transitive, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, CategoryTheory.Functor.mapActionCongr_inv, groupCohomology.H1InfRes_g, Rep.standardComplex.d_comp_ε, Rep.finsuppTensorRight_inv_hom, CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction, Rep.coinvariantsMk_app_hom, Rep.ihom_obj_V_isAddCommGroup, Rep.indCoindNatIso_inv_app, functorCategoryEquivalence_counitIso, groupCohomology.mapShortComplexH1_id_comp, groupCohomology.cocyclesMap_comp_assoc, forget_ε, groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor, Rep.coindResAdjunction_homEquiv_symm_apply, Rep.coindVEquiv_apply_hom, groupCohomology.mapShortComplexH1_comp, FunctorCategoryEquivalence.inverse_obj_V, resComp_inv_app_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom, Rep.trivialFunctor_map_hom, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, FunctorCategoryEquivalence.unitIso_hom_app_hom, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupHomology.mapShortComplexH1_id, groupCohomology.map_id_comp, hom_inv_hom_assoc, Rep.ihom_map_hom, tensorHom_hom, inv_hom_hom, Rep.coinvariantsTensor_hom_ext_iff, Rep.finsuppTensorLeft_inv_hom, associator_hom_hom, res_obj_ρ, CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction, Functor.preservesLimitsOfSize_of_preserves, Rep.unit_iso_comm, full_res, Rep.leftRegularHomEquiv_symm_single, instReflectsLimitsForget, inhomogeneousCochains.d_eq, CategoryTheory.PreGaloisCategory.has_decomp_quotients, Rep.FiniteCyclicGroup.resolution_complex, CategoryTheory.Functor.mapActionCongr_hom, groupHomology.chainsFunctor_map, Rep.leftRegularTensorTrivialIsoFree_inv_hom, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomCarrierAutFunctorFunctorToContAction, groupHomology.chainsMap_f_hom, mkIso_inv_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, Rep.indResAdjunction_unit_app_hom_hom, groupHomology.map_id_comp_H0Iso_hom_apply, groupHomology.H1CoresCoinfOfTrivial_f, Rep.coindFunctor'_obj, FunctorCategoryEquivalence.inverse_map_hom, Rep.linearization_δ_hom, groupHomology.functor_map, ContAction.resCongr_inv, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, whiskerLeft_hom, groupCohomology.mapCocycles₁_comp_i_apply, groupHomology.mapCycles₂_id_comp_apply, Rep.standardComplex.instQuasiIsoNatεToSingle₀, zsmul_hom, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomCarrierAutFunctorFunctorToContActionOfFiberFunctor, Rep.standardComplex.x_projective, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction, Rep.MonoidalClosed.linearHomEquiv_hom, Rep.invariantsAdjunction_homEquiv_apply_hom, preservesLimitsOfSize_of_preserves, Rep.instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, Rep.FiniteCyclicGroup.resolution_quasiIso, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, groupCohomology.H1Map_id, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, groupCohomology.cochainsMap_f_hom, Rep.finsuppTensorLeft_hom_hom, Rep.indFunctor_map, groupHomology.H1CoresCoinfOfTrivial_g, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, FunctorCategoryEquivalence.counitIso_hom_app_app, groupHomology.π_comp_H0Iso_hom, groupCohomology.mapShortComplexH1_id_comp_assoc, groupCohomology.mapShortComplexH1_zero, ContinuousCohomology.instLinearActionTopModuleCatI, groupCohomology.mapShortComplexH1_comp_assoc, Rep.coinvariantsTensorMk_apply, groupHomology.cyclesIso₀_inv_comp_cyclesMap, tensorUnit_V, ContinuousCohomology.I_obj_V_topologicalSpace, groupHomology.H0π_comp_H0Iso_hom, Rep.coinvariantsShortComplex_X₁, Rep.homEquiv_symm_apply_hom, Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, instMonoidalPreadditive, FDRep.forget₂_ρ, Rep.invariantsFunctor_map_hom, groupHomology.map_id_comp_H0Iso_hom, FunctorCategoryEquivalence.functor_μ, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupCohomology.cocyclesMap_id, Rep.instIsRightAdjointActionModuleCatRes, tensor_ρ, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, Rep.norm_comm_assoc, groupCohomology.mapShortComplexH2_id_comp, ContinuousCohomology.MultiInd.d_comp_d, Rep.resIndAdjunction_unit_app, resEquiv_inverse, Rep.diagonalOneIsoLeftRegular_hom_hom, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Functor.preservesColimitsOfSize_of_preserves, Rep.ihom_coev_app_hom, β_inv_hom, Rep.leftRegularHomEquiv_apply, Rep.leftRegular_projective, groupHomology.chainsMap_zero, forget_linear, CategoryTheory.PreGaloisCategory.exists_lift_of_mono, diagonalSuccIsoTensorDiagonal_hom_hom, resId_hom_app_hom, instHasColimits, groupHomology.mapShortComplexH2_id_comp, rightUnitor_hom_hom, forget_μ, diagonalSuccIsoTensorTrivial_hom_hom_apply, leftDual_v, CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj, groupHomology.mapCycles₂_comp_i_apply, isContinuous_def, CategoryTheory.Functor.mapAction_map_hom, Functor.mapActionPreservesColimitsOfShapeOfPreserves, groupCohomology.cocyclesMap_id_comp, Rep.res_obj_ρ, associator_inv_hom, resEquiv_functor, groupHomology.shortComplexH0_g, Rep.ihom_obj_V_isModule, groupCohomology.mapShortComplexH2_id, Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, leftDual_ρ, instFaithfulRes, Rep.diagonalHomEquiv_apply, functorCategoryEquivalence_linear, Rep.coinvariantsAdjunction_unit_app_hom, CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup, Rep.freeLiftLEquiv_symm_apply, groupHomology.inhomogeneousChains.d_eq, instReflectsLimitForget, Rep.epi_iff_surjective, groupCohomology.cochainsFunctor_map, groupHomology.d₁₀_comp_coinvariantsMk_assoc, CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, Rep.coinvariantsShortComplex_X₂, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, functorCategoryEquivalence_preservesZeroMorphisms, groupHomology.H0π_comp_H0Iso_hom_assoc, Iso.conj_ρ, groupHomology.cyclesMap_comp, preservesColimit_of_preserves, rightUnitor_inv_hom, Rep.indResHomEquiv_apply_hom, groupHomology.mapShortComplexH1_τ₃, res_linear, instPreservesColimitsOfShapeForgetOfHasColimitsOfShape, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupHomology.lsingle_comp_chainsMap_f_assoc, Rep.linearizationTrivialIso_hom_hom, Rep.instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, ContinuousCohomology.MultiInd.d_succ, Rep.coinvariantsAdjunction_homEquiv_apply_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, groupHomology.H1CoresCoinf_f, Rep.diagonalSuccIsoFree_hom_hom_single, Rep.ihom_obj_ρ, instMonoidalLinear, resComp_hom_app_hom, Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, groupCohomology.cochainsMap_id_comp_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, functorCategoryEquivalence_additive, preservesColimitsOfShape_of_preserves, Rep.instIsLeftAdjointIndFunctor, Rep.instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, Representation.linHom.invariantsEquivRepHom_apply_hom, groupHomology.cyclesMap_id, Rep.instAdditiveModuleCatInvariantsFunctor, forget₂_linear, isIso_hom_mk, FunctorCategoryEquivalence.functor_obj_map, CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, Rep.coindFunctor'_map, Rep.coinvariantsFunctor_map_hom, Rep.coindFunctor_obj, Rep.linearization_map_hom_single, comp_hom_assoc, groupCohomology.map_id_comp_H0Iso_hom_assoc, Rep.ihom_obj_ρ_def, Rep.ihom_obj_V_carrier, ContinuousCohomology.const_app_hom, ContAction.resComp_inv, instHasFiniteLimits, Rep.coinvariantsShortComplex_X₃, Rep.coindIso_hom_hom_hom, Rep.leftRegularTensorTrivialIsoFree_hom_hom, ContAction.res_map, groupHomology.H0π_comp_H0Iso_hom_apply, Rep.mono_iff_injective, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, groupCohomology.functor_map, Rep.linearization_ε_hom, CategoryTheory.Equivalence.mapAction_inverse, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, Rep.Tor_obj, Rep.coinvariantsShortComplex_shortExact, resCongr_hom, CategoryTheory.PreGaloisCategory.instIsPretransitiveAutCarrierVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, Rep.FiniteCyclicGroup.resolution_π, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, groupHomology.mapCycles₁_quotientGroupMk'_epi, groupHomology.H0π_comp_map_apply, groupCohomology.mapShortComplexH1_τ₁, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.FiniteCyclicGroup.resolution.π_f, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, Rep.instAdditiveModuleCatCoinvariantsFunctor, groupCohomology.cochainsFunctor_obj, Rep.linearization_map_hom, β_hom_hom, CategoryTheory.FintypeCat.Action.isConnected_of_transitive, instReflectsColimitForget, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, CategoryTheory.PreGaloisCategory.functorToAction_full, leftUnitor_hom_hom, FunctorCategoryEquivalence.functor_η, Rep.indResHomEquiv_symm_apply_hom, ContinuousCohomology.instAdditiveActionTopModuleCatI, forget₂_additive, forget_map, groupHomology.chainsMap_f_0_comp_chainsIso₀, classifyingSpaceUniversalCover_obj, FintypeCat.toEndHom_trivial_of_mem, CategoryTheory.Functor.instFaithfulActionMapAction, Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single, Rep.norm_comm, FunctorCategoryEquivalence.functor_ε, Rep.linearization_μ_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction, preservesLimit_of_preserves, groupHomology.chainsMap_f, Rep.quotientToCoinvariantsFunctor_obj_V, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc, groupCohomology.cochainsMap_id, Rep.instInjective, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
instConcreteCategoryHomSubtypeV 📖	CompOp	19 math math: CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV, Rep.norm_comm_apply, forget₂_preservesZeroMorphisms, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.standardComplex.εToSingle₀_comp_eq, Rep.applyAsHom_comm_apply, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, FDRep.forget₂_ρ, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, isContinuous_def, Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV, forget₂_linear, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, forget₂_additive, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq
instFunLikeHomSubtypeV 📖	CompOp	20 math math: DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomCarrierV, Rep.norm_comm_apply, forget₂_preservesZeroMorphisms, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.standardComplex.εToSingle₀_comp_eq, Rep.applyAsHom_comm_apply, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, FDRep.forget₂_ρ, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, isContinuous_def, Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomCarrierV, forget₂_linear, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, 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	161 math math: resCongr_inv, Rep.resCoindHomEquiv_symm_apply_hom, Rep.resCoindHomEquiv_apply_hom, groupHomology.mapCycles₂_comp_assoc, groupHomology.map₁_quotientGroupMk'_epi, groupCohomology.cocyclesMap_id_comp_assoc, Rep.coindResAdjunction_counit_app, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, Rep.resCoindAdjunction_counit_app_hom_hom, groupHomology.mapCycles₁_comp_apply, groupHomology.mapShortComplexH1_zero, groupHomology.cyclesMap_id_comp, groupHomology.mapShortComplexH2_zero, Rep.coe_res_obj_ρ, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, groupHomology.mapCycles₁_comp_assoc, groupHomology.H0π_comp_map, groupCohomology.cochainsMap_comp, groupHomology.coresNatTrans_app, groupCohomology.map_H0Iso_hom_f_apply, groupCohomology.congr, Rep.resCoindAdjunction_unit_app_hom_hom, groupHomology.H1CoresCoinfOfTrivial_X₁, groupCohomology.mapShortComplexH2_comp_assoc, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, Rep.instPreservesProjectiveObjectsActionModuleCatSubtypeMemSubgroupResSubtype, groupHomology.mapCycles₁_id_comp_assoc, groupHomology.mapCycles₁_comp, groupHomology.map_comp, groupCohomology.map_comp, groupHomology.map_id_comp, Rep.coinvariantsTensorIndIso_inv, Rep.coindVEquiv_symm_apply_coe, groupHomology.H1CoresCoinf_X₁, groupHomology.mapCycles₂_id_comp, groupHomology.cyclesMap_comp_assoc, Rep.instIsLeftAdjointActionModuleCatRes, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, groupHomology.chainsMap_f_single, Rep.coinvariantsTensorIndIso_hom, groupCohomology.map_H0Iso_hom_f, resId_inv_app_hom, groupCohomology.cochainsMap_zero, groupHomology.map_comp_assoc, Rep.coinvariantsTensorIndNatIso_inv_app, Rep.coindResAdjunction_unit_app, groupHomology.mapCycles₁_id_comp_apply, groupCohomology.cochainsMap_id_comp, groupCohomology.mapShortComplexH2_comp, groupCohomology.cochainsMap_comp_assoc, Rep.indResAdjunction_counit_app_hom_hom, groupHomology.mapCycles₁_comp_i_apply, groupHomology.mapCycles₂_comp, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, ContAction.resCongr_hom, Rep.resIndAdjunction_homEquiv_symm_apply, Rep.coindMap'_hom, groupHomology.H0π_comp_map_assoc, res_additive, groupCohomology.H1InfRes_X₃, groupCohomology.cocyclesMap_comp, ContAction.res_obj_obj, groupCohomology.resNatTrans_app, groupCohomology.mapShortComplexH2_zero, Rep.resIndAdjunction_homEquiv_apply, groupHomology.mapCycles₂_comp_apply, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, res_obj_V, Rep.quotientToInvariantsFunctor_map_hom, groupHomology.chainsMap_id_comp, Rep.quotientToCoinvariantsFunctor_map_hom, groupHomology.mapShortComplexH1_id_comp, groupHomology.mapShortComplexH1_comp, Rep.coindResAdjunction_homEquiv_apply, Rep.resIndAdjunction_counit_app, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, Representation.coind'_apply_apply, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, groupCohomology.mapShortComplexH2_id_comp_assoc, groupHomology.mapCycles₂_id_comp_assoc, Rep.coindIso_inv_hom_hom, groupHomology.mapShortComplexH2_comp, groupHomology.mapCycles₁_id_comp, res_map_hom, groupHomology.lsingle_comp_chainsMap_f, groupHomology.cyclesMap_comp_cyclesIso₀_hom, groupCohomology.cochainsMap_f, Rep.coind'_ext_iff, groupHomology.chainsMap_comp, groupCohomology.map_id_comp_assoc, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, Rep.coinvariantsTensorIndNatIso_hom_app, groupHomology.congr, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, groupCohomology.H1InfRes_g, groupCohomology.mapShortComplexH1_id_comp, groupCohomology.cocyclesMap_comp_assoc, Rep.coindResAdjunction_homEquiv_symm_apply, Rep.coindVEquiv_apply_hom, groupCohomology.mapShortComplexH1_comp, resComp_inv_app_hom, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, groupCohomology.map_id_comp, res_obj_ρ, full_res, groupHomology.chainsMap_f_hom, Rep.indResAdjunction_unit_app_hom_hom, groupHomology.H1CoresCoinfOfTrivial_f, ContAction.resCongr_inv, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, groupCohomology.mapCocycles₁_comp_i_apply, groupHomology.mapCycles₂_id_comp_apply, groupCohomology.cochainsMap_f_hom, groupHomology.H1CoresCoinfOfTrivial_g, groupCohomology.mapShortComplexH1_id_comp_assoc, groupCohomology.mapShortComplexH1_zero, groupCohomology.mapShortComplexH1_comp_assoc, groupHomology.cyclesIso₀_inv_comp_cyclesMap, Rep.instIsRightAdjointActionModuleCatRes, groupCohomology.mapShortComplexH2_id_comp, Rep.resIndAdjunction_unit_app, resEquiv_inverse, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, groupHomology.chainsMap_zero, resId_hom_app_hom, groupHomology.mapShortComplexH2_id_comp, groupHomology.mapCycles₂_comp_i_apply, groupCohomology.cocyclesMap_id_comp, Rep.res_obj_ρ, resEquiv_functor, instFaithfulRes, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupHomology.cyclesMap_comp, Rep.indResHomEquiv_apply_hom, groupHomology.mapShortComplexH1_τ₃, res_linear, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupHomology.lsingle_comp_chainsMap_f_assoc, groupHomology.H1CoresCoinf_f, resComp_hom_app_hom, groupCohomology.cochainsMap_id_comp_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, Rep.coindIso_hom_hom_hom, ContAction.res_map, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, resCongr_hom, groupHomology.mapCycles₁_quotientGroupMk'_epi, groupHomology.H0π_comp_map_apply, groupCohomology.mapShortComplexH1_τ₁, Rep.indResHomEquiv_symm_apply_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀, groupHomology.chainsMap_f, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc
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	6 math math: leftRegularTensorIso_inv_hom, diagonalSuccIsoTensorTrivial_inv_hom_apply, leftRegularTensorIso_hom_hom, trivial_ρ, diagonalSuccIsoTensorTrivial_hom_hom_apply, trivial_V
ρ 📖	CompOp	40 math math: Rep.coe_linearization_obj_ρ, leftRegularTensorIso_inv_hom, ofMulAction_apply, FDRep.endRingEquiv_symm_comp_ρ, rightDual_ρ, Rep.linearization_single, Rep.ρ_hom, 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_ρ, res_map_hom, Rep.linearization_obj_ρ, ρ_self_inv_apply, ρ_one, ρAut_apply_hom, trivial_ρ, Hom.comm_assoc, res_obj_ρ, Rep.ofHom_ρ, Rep.Action_ρ_eq_ρ, tensor_ρ, FDRep.of_ρ, isContinuous_def, CategoryTheory.Functor.mapAction_map_hom, leftDual_ρ, Iso.conj_ρ, Rep.ihom_obj_ρ, FunctorCategoryEquivalence.functor_obj_map, ρAut_apply_inv, Hom.comm, ρ_inv_self_apply, FDRep.hom_action_ρ, 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	218 math math: Rep.resCoindHomEquiv_symm_apply_hom, Representation.repOfTprodIso_inv_apply, Rep.resCoindHomEquiv_apply_hom, Rep.invariantsAdjunction_homEquiv_symm_apply_hom, Rep.MonoidalClosed.linearHomEquiv_symm_hom, Action.leftRegularTensorIso_inv_hom, Action.neg_hom, Action.inv_hom_hom_assoc, Action.sum_hom, Rep.diagonalSuccIsoFree_inv_hom_single, Representation.repOfTprodIso_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, Rep.resCoindAdjunction_counit_app_hom_hom, Rep.leftRegularHom_hom, Action.diagonalSuccIsoTensorDiagonal_inv_hom, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, CategoryTheory.Functor.mapAction_δ_hom, Rep.diagonalHomEquiv_symm_apply, comp_hom, Action.leftUnitor_inv_hom, Action.comp_hom, groupHomology.H0π_comp_map, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, Action.whiskerRight_hom, groupCohomology.map_H0Iso_hom_f_apply, Rep.standardComplex.d_eq, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, Rep.resCoindAdjunction_unit_app_hom_hom, Rep.instEpiModuleCatHom, Rep.homEquiv_apply_hom, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_zero_iff, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, groupCohomology.mapCocycles₂_comp_i_apply, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, Action.smul_hom, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, Rep.indCoindIso_inv_hom_hom, Rep.diagonalSuccIsoFree_inv_hom_single_single, Action.FunctorCategoryEquivalence.unitIso_inv_app_hom, Rep.ihom_ev_app_hom, Action.FunctorCategoryEquivalence.functor_map_app, Rep.MonoidalClosed.linearHomEquivComm_hom, Rep.subtype_hom, Rep.coindVEquiv_symm_apply_coe, Rep.indCoindIso_hom_hom_hom, Action.hom_inv_hom, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.cyclesMap_comp_cyclesIso₀_hom_apply, groupHomology.chainsMap_f_single, Action.mkIso_hom_hom, groupCohomology.map_H0Iso_hom_f, Action.resId_inv_app_hom, Rep.indToCoindAux_comm, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, Action.instIsIsoHomInv, CategoryTheory.Functor.mapAction_η_hom, Rep.indResAdjunction_counit_app_hom_hom, Action.FintypeCat.toEndHom_apply, Action.hom_ext_iff, groupHomology.mapCycles₁_comp_i_apply, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, Action.hom_injective, Action.nsmul_hom, Action.diagonalSuccIsoTensorTrivial_inv_hom_apply, Rep.coindMap'_hom, groupHomology.H0π_comp_map_assoc, Rep.freeLiftLEquiv_apply, Action.id_hom, Action.sub_hom, Rep.finsuppTensorRight_hom_hom, groupCohomology.norm_ofAlgebraAutOnUnits_eq, CategoryTheory.Functor.mapAction_ε_hom, TannakaDuality.FiniteGroup.forget_map, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, Rep.linearization_η_hom_apply, Rep.quotientToInvariantsFunctor_map_hom, Rep.quotientToCoinvariantsFunctor_map_hom, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, id_hom, Action.leftRegularTensorIso_hom_hom, Rep.ofMulActionSubsingletonIsoTrivial_inv_hom, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, ContinuousCohomology.I_map_hom, CategoryTheory.Functor.mapAction_μ_hom, Rep.diagonalOneIsoLeftRegular_inv_hom, Action.FintypeCat.quotientToEndHom_mk, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, Rep.coindIso_inv_hom_hom, Action.zero_hom, groupCohomology.map_id_comp_H0Iso_hom_apply, groupHomology.chainsMap_id_f_hom_eq_mapRange, Rep.diagonalSuccIsoTensorTrivial_hom_hom_single, Action.res_map_hom, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, Rep.toCoinvariantsMkQ_hom, groupHomology.lsingle_comp_chainsMap_f, Action.instIsIsoHomHom, Rep.invariantsAdjunction_counit_app_hom, groupHomology.cyclesMap_comp_cyclesIso₀_hom, groupCohomology.cochainsMap_f, Rep.coind'_ext_iff, CategoryTheory.PreGaloisCategory.functorToAction_map, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, Rep.ofMulActionSubsingletonIsoTrivial_hom_hom, Rep.linearizationTrivialIso_inv_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, Action.add_hom, Rep.leftRegularHom_hom_single, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, comm_assoc, Rep.finsuppTensorRight_inv_hom, Rep.coindVEquiv_apply_hom, Action.resComp_inv_app_hom, Rep.trivialFunctor_map_hom, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, Action.FunctorCategoryEquivalence.unitIso_hom_app_hom, Action.hom_inv_hom_assoc, Rep.ihom_map_hom, ext_iff, Action.tensorHom_hom, Action.inv_hom_hom, Rep.finsuppTensorLeft_inv_hom, Action.associator_hom_hom, Rep.leftRegularHomEquiv_symm_single, Rep.leftRegularTensorTrivialIsoFree_inv_hom, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, groupHomology.chainsMap_f_hom, Rep.norm_hom, Action.mkIso_inv_hom, Rep.indResAdjunction_unit_app_hom_hom, groupHomology.map_id_comp_H0Iso_hom_apply, Action.FintypeCat.quotientToQuotientOfLE_hom_mk, Action.FunctorCategoryEquivalence.inverse_map_hom, Rep.linearization_δ_hom, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, Action.whiskerLeft_hom, groupCohomology.mapCocycles₁_comp_i_apply, Rep.coindMap_hom, Action.zsmul_hom, Rep.MonoidalClosed.linearHomEquiv_hom, Rep.invariantsAdjunction_homEquiv_apply_hom, Rep.hom_comm_apply, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, groupCohomology.cochainsMap_f_hom, Rep.finsuppTensorLeft_hom_hom, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.cyclesIso₀_inv_comp_cyclesMap, Rep.indMap_hom, Rep.homEquiv_symm_apply_hom, Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, Rep.invariantsFunctor_map_hom, Rep.diagonalOneIsoLeftRegular_hom_hom, Rep.ihom_coev_app_hom, Action.β_inv_hom, Rep.leftRegularHomEquiv_apply, Action.diagonalSuccIsoTensorDiagonal_hom_hom, Action.resId_hom_app_hom, Action.rightUnitor_hom_hom, Action.diagonalSuccIsoTensorTrivial_hom_hom_apply, groupHomology.mapCycles₂_comp_i_apply, Rep.freeLift_hom, CategoryTheory.Functor.mapAction_map_hom, Action.associator_inv_hom, Rep.freeLift_hom_single_single, Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, Rep.diagonalHomEquiv_apply, Rep.coinvariantsAdjunction_unit_app_hom, Rep.epi_iff_surjective, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, Rep.applyAsHom_hom, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, Action.rightUnitor_inv_hom, Rep.indResHomEquiv_apply_hom, groupHomology.mapShortComplexH1_τ₃, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupHomology.lsingle_comp_chainsMap_f_assoc, Rep.linearizationTrivialIso_hom_hom, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, Rep.coinvariantsAdjunction_homEquiv_apply_hom, Rep.diagonalSuccIsoFree_hom_hom_single, Rep.free_ext_iff, Action.resComp_hom_app_hom, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, TannakaDuality.FiniteGroup.ofRightFDRep_hom, Representation.linHom.invariantsEquivRepHom_apply_hom, Rep.mkQ_hom, Rep.coinvariantsFunctor_map_hom, comm, Rep.linearization_map_hom_single, Action.comp_hom_assoc, ContinuousCohomology.const_app_hom, Rep.coindIso_hom_hom_hom, Rep.leftRegularTensorTrivialIsoFree_hom_hom, Rep.barComplex.d_single, Rep.mono_iff_injective, FDRep.dualTensorIsoLinHom_hom_hom, Rep.instMonoModuleCatHom, Rep.linearization_ε_hom, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, groupHomology.H0π_comp_map_apply, groupCohomology.mapShortComplexH1_τ₁, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, Rep.linearization_map_hom, Action.β_hom_hom, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, Action.leftUnitor_hom_hom, Rep.indResHomEquiv_symm_apply_hom, Action.forget_map, groupHomology.chainsMap_f_0_comp_chainsIso₀, Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single, Rep.linearization_μ_hom, groupHomology.chainsMap_f, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply
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	25 math math: mapAction_δ_hom, Action.Functor.mapActionPreservesLimitsOfShapeOfPreserves, mapActionComp_hom, Action.Functor.mapActionPreservesLimit_of_preserves, mapActionComp_inv, Action.Functor.mapActionPreservesColimit_of_preserves, CategoryTheory.Equivalence.mapAction_functor, Action.Functor.instPreservesFiniteLimitsMapActionOfHasFiniteLimits, mapAction_η_hom, 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, 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