ModuleCat

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

Statistics

Metric	Count
Definitions ModuleCat	1
Theorems	0
Total	1

(root)

Definitions

Name	Category	Theorems
ModuleCat 📖	CompData	1589 math math: ModuleCat.HasColimit.colimitCocone_pt_isAddCommGroup, ModuleCat.instIsRightAdjointCoextendScalars, ModuleCat.instPreservesMonomorphismsRestrictScalars, PresheafOfModules.Monoidal.tensorObj_obj, groupHomology.mapShortComplexH2_τ₁, Rep.resCoindHomEquiv_symm_apply_hom, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, Representation.repOfTprodIso_inv_apply, Rep.resCoindHomEquiv_apply_hom, groupCohomology.instEpiModuleCatH2π, groupCohomology.mapShortComplexH1_τ₂, ModuleCat.hom_zero, groupHomology.π_comp_H2Iso_hom_assoc, ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier, Rep.invariantsAdjunction_homEquiv_symm_apply_hom, LightCondensed.free_internallyProjective_iff_tensor_condition, CategoryTheory.linearCoyoneda_obj_additive, ModuleCat.instFullUliftFunctor, ModuleCat.forget_preservesLimits, ModuleCat.directLimitDiagram_obj_isModule, CommRingCat.KaehlerDifferential.map_d, CategoryTheory.preadditiveCoyonedaObj_map, ModuleCat.MonoidalCategory.braiding_hom_apply, Rep.coe_linearization_obj_ρ, ModuleCat.biproductIsoPi_inv_comp_π, simple_of_finrank_eq_one, ModuleCat.FilteredColimits.colimit_smul_mk_eq, groupHomology.mapCycles₂_comp_assoc, ModuleCat.restrictScalars.map_apply, Condensed.instAB4StarCondensedMod, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom, ModuleCat.forget₂_reflectsLimitsOfSize, CategoryTheory.additive_yonedaObj, groupCohomology.toCocycles_comp_isoCocycles₁_hom, CategoryTheory.linearCoyoneda_map_app, CategoryTheory.linearCoyoneda_obj_obj_carrier, Rep.MonoidalClosed.linearHomEquiv_symm_hom, ModuleCat.projective_of_free, groupCohomology.isoCocycles₁_hom_comp_i_apply, instEssentiallySmallFGModuleCat, groupHomology.map₁_quotientGroupMk'_epi, groupCohomology.mem_cocycles₂_def, TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, MoritaEquivalence.linear, groupHomology.coinfNatTrans_app, groupHomology.mapShortComplexH2_id, ModuleCat.forget_preservesLimitsOfSize, groupCohomology.d₂₃_hom_apply, ModuleCat.restrictScalarsCongr_symm, LightCondensed.ihomPoints_apply, LinearMap.id_fgModuleCat_comp, ModuleCat.restrictScalarsId'App_inv_naturality_assoc, groupHomology.d₁₀_single_one, groupHomology.shortComplexH1_f, FDRep.char_tensor, groupHomology.boundaries₂_le_cycles₂, groupHomology.coinvariantsMk_comp_H0Iso_inv_apply, ModuleCat.forget₂PreservesColimitsOfSize, groupCohomology.inhomogeneousCochains.d_def, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, PresheafOfModules.add_app, FGModuleCat.hom_hom_id, Rep.diagonalSuccIsoFree_inv_hom_single, CondensedMod.IsSolid.isIso_solidification_map, groupCohomology.cocyclesMap_id_comp_assoc, groupHomology.map₁_one, groupCohomology.d₀₁_comp_d₁₂, Representation.repOfTprodIso_apply, ModuleCat.freeHomEquiv_apply, ModuleCat.epi_as_hom''_mkQ, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply, Rep.coindResAdjunction_counit_app, ModuleCat.forget₂AddCommGroup_preservesLimitsOfSize, ModuleCat.toMatrixModCat_map, groupCohomology.toCocycles_comp_isoCocycles₂_hom_apply, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, LightCondensed.forget_obj_val_map, groupCohomology.cocyclesIso₀_hom_comp_f, Rep.resCoindAdjunction_counit_app_hom_hom, groupHomology.d₃₂_single, CategoryTheory.Abelian.FreydMitchell.instFaithfulModuleCatEmbeddingRingFunctor, groupCohomology.eq_d₀₁_comp_inv, ModuleCat.extendScalarsId_hom_app_one_tmul, groupCohomology.H1π_comp_map_assoc, groupHomology.mapCycles₁_comp_apply, groupHomology.cyclesIso₀_inv_comp_iCycles_apply, Rep.leftRegularHom_hom, PresheafOfModules.restrictScalars_map_app, groupHomology.mapShortComplexH1_zero, groupCohomology.π_comp_H0Iso_hom, FDRep.endRingEquiv_symm_comp_ρ, ModuleCat.ofHom_comp, groupHomology.H0IsoOfIsTrivial_inv_eq_π, groupCohomology.π_comp_H1Iso_hom_assoc, ModuleCat.ι_coprodIsoDirectSum_hom_apply, ModuleCat.restrictScalarsComp'App_hom_apply, PresheafOfModules.epi_iff_surjective, groupHomology.cyclesMap_id_comp, LightCondensed.ihomPoints_symm_comp, Rep.indFunctor_obj, ModuleCat.isZero_iff_subsingleton, groupHomology.mapShortComplexH2_zero, groupCohomology.eq_d₁₂_comp_inv, CategoryTheory.whiskering_linearCoyoneda, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply, CategoryTheory.ShortComplex.moduleCatMk_X₁_carrier, Rep.indToCoindAux_self, Condensed.instAB5CondensedMod, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, groupCohomology.mapCocycles₂_comp_i, PresheafOfModules.evaluation_preservesColimitsOfShape, ModuleCat.AlternatingMap.postcomp_apply, groupHomology.H1CoresCoinf_exact, groupHomology.eq_d₃₂_comp_inv, FGModuleCat.instHasColimitsOfShapeOfFinCategory, PresheafOfModules.comp_app, CategoryTheory.ShortComplex.moduleCatMk_X₁_isAddCommGroup, Rep.indCoindNatIso_hom_app, groupHomology.chainsMap_id, instSmallUnitsSkeletonModuleCat, Rep.coe_res_obj_ρ, Rep.invariantsFunctor_obj_carrier, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, Rep.barComplex.d_def, ModuleCat.monoidalClosed_uncurry, Rep.diagonalHomEquiv_symm_apply, groupCohomology.H0IsoOfIsTrivial_hom, ModuleCat.matrixEquivalence_inverse, TannakaDuality.FiniteGroup.forget_obj, CondensedMod.isDiscrete_tfae, CategoryTheory.linearYoneda_obj_map, Rep.coindFunctor_map, ModuleCat.hasLimits', CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom, groupCohomology.coe_mapCocycles₁, groupHomology.mem_cycles₂_iff, ModuleCat.Iso.homCongr_eq_arrowCongr, ModuleCat.CoextendScalars.smul_apply', groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_g, groupHomology.cyclesMap_comp_isoCycles₂_hom, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_isModule, ModuleCat.directLimitCocone_pt_carrier, ModuleCat.toMatrixModCat_obj_carrier, groupCohomology.d₁₂_hom_apply, ModuleCat.preservesFiniteLimits_extendScalars_of_flat, ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule, instAB4StarModuleCat, groupHomology.comp_d₂₁_eq, PresheafOfModules.pushforward_map_app_apply, Rep.instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype, CategoryTheory.preadditiveYonedaObj_obj_carrier, groupCohomology.coboundariesToCocycles₁_apply, Rep.instIsRightAdjointCoindFunctor, groupHomology.mapCycles₁_comp_assoc, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, CategoryTheory.ShortComplex.moduleCatMk_X₂_isModule, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, CondensedMod.LocallyConstant.instFullModuleCatFunctor, FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, Rep.instIsTrivialObjModuleCatTrivialFunctor, PresheafOfModules.sections_property, groupHomology.H0π_comp_map, linearEquivIsoModuleIso_hom, groupHomology.H1CoresCoinf_X₃, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, groupCohomology.mapShortComplexH1_τ₃, AlgebraicGeometry.instIsLeftAdjointModuleCatCarrierModulesSpecOfFunctor, PresheafOfModules.toSheafify_app_apply', AlgebraicGeometry.tilde.map_id, PresheafOfModules.instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct, Rep.coinvariantsAdjunction_counit_app, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, LightCondMod.instPreservesEpimorphismsLightCondSetForget, ModuleCat.forget_preservesEpimorphisms, PresheafOfModules.Derivation.d_map, groupHomology.map_id, QuadraticModuleCat.forget₂_map_associator_inv, LinearMap.comp_id_fgModuleCat, ModuleCat.HasColimit.instHasColimit, ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction_hom_apply, groupCohomology.cochainsMap_comp, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, AlgebraicGeometry.tilde.map_sub, groupCohomology.comp_d₁₂_eq, ModuleCat.toMatrixModCat_obj_isAddCommGroup, groupCohomology.mem_cocycles₁_of_addMonoidHom, groupCohomology.cocycles₂.d₂₃_apply, groupCohomology.d₀₁_hom_apply, Rep.linearization_single, ModuleCat.extendRestrictScalarsAdj_homEquiv_apply, groupHomology.π_comp_H1Iso_inv, groupHomology.d₃₂_single_one_thd, CategoryTheory.ShortComplex.moduleCatMk_g, LightCondMod.isDiscrete_tfae, ModuleCat.restrictScalarsComp'_inv_app, ModuleCat.hom_tensorHom, groupHomology.isoCycles₁_inv_comp_iCycles_apply, groupHomology.coresNatTrans_app, PresheafOfModules.free_map_app, groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor, ModuleCat.forget₂_addCommGrp_essSurj, groupCohomology.dArrowIso₀₁_inv_right, groupCohomology.map_H0Iso_hom_f_apply, ModuleCat.shortExact_projectiveShortComplex, groupCohomology.d₁₂_comp_d₂₃_apply, groupCohomology.H0IsoOfIsTrivial_inv_apply, groupCohomology.eq_d₂₃_comp_inv_assoc, PresheafOfModules.congr_map_apply, groupCohomology.congr, CategoryTheory.Abelian.freyd_mitchell, PresheafOfModules.freeYonedaEquiv_symm_app, Rep.finsuppToCoinvariantsTensorFree_single, groupCohomology.eq_d₂₃_comp_inv_apply, groupCohomology.eq_d₁₂_comp_inv_apply, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, groupHomology.mapShortComplexH1_τ₂, PresheafOfModules.restrictScalarsObj_map, PresheafOfModules.forgetToPresheafModuleCatObj_map, groupHomology.chains₁ToCoinvariantsKer_surjective, ModuleCat.enoughProjectives, ModuleCat.restrictScalarsId'App_hom_naturality, Rep.coinvariantsTensorFreeLEquiv_symm_apply, Rep.standardComplex.d_eq, LinearEquiv.toModuleIso_inv, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app, SheafOfModules.evaluationPreservesLimitsOfShape, Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, ModuleCat.forget₂AddCommGroup_reflectsLimitOfShape, ModuleCat.exteriorPower.iso₀_hom_naturality, ModuleCat.forget_reflectsLimitsOfSize, groupHomology.cycles₁_eq_top_of_isTrivial, instIsEquivalenceFGModuleCatUlift, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_hom_apply, groupHomology.π_comp_H0Iso_hom_assoc, Rep.resCoindAdjunction_unit_app_hom_hom, ModuleCat.restrictScalars_isEquivalence_of_ringEquiv, groupHomology.d₃₂_comp_d₂₁_assoc, groupCohomology.mem_cocycles₁_def, CoalgCat.comonEquivalence_inverse, Rep.trivial_projective_of_subsingleton, ModuleCat.endRingEquiv_symm_apply_hom, FGModuleCat.instFiniteHomModuleCatObjIsFG, Rep.instEpiModuleCatHom, ModuleCat.restrictScalarsComp'_hom_app, groupHomology.H1CoresCoinfOfTrivial_X₁, Rep.homEquiv_apply_hom, groupHomology.chainsMap_id_f_map_mono, ModuleCat.FilteredColimits.colimit_zero_eq, 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, ModuleCat.forget_preservesMonomorphisms, groupCohomology.mapCocycles₂_comp_i_apply, ModuleCat.instHasFiniteColimits, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_apply, PresheafOfModules.id_app, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.full, ModuleCat.MonoidalCategory.associator_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, AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor, groupHomology.cycles₁IsoOfIsTrivial_hom_apply, ModuleCat.HasLimit.productLimitCone_cone_π, ModuleCat.HasColimit.colimitCocone_ι_app, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, PresheafOfModules.restrictScalarsObj_obj, groupCohomology.coboundaries₁_eq_bot_of_isTrivial, instHasSeparatorModuleCatOfSmall, Rep.coinvariantsAdjunction_homEquiv_symm_apply_hom, ModuleCat.instAdditiveLocalizationLocalizedModule_functor, ModuleCat.MonoidalCategory.tensorHom_tmul, groupHomology.d₂₁_single_inv_mul_ρ_add_single, QuadraticModuleCat.forget₂_map, groupCohomology.instMonoModuleCatFH1InfRes, ModuleCat.smulShortComplex_X₃_isAddCommGroup, ModuleCat.forget₂_addCommGroup_full, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, ModuleCat.hasLimitsOfSize, groupCohomology.cocycles₂_map_one_fst, Rep.indCoindIso_inv_hom_hom, PresheafOfModules.sectionsMap_coe, groupCohomology.mapCocycles₂_comp_i_assoc, Rep.free_projective, groupHomology.d₁₀_comp_coinvariantsMk_apply, ModuleCat.ExtendRestrictScalarsAdj.Counit.map_hom_apply, Rep.ρ_hom, Rep.diagonalSuccIsoFree_inv_hom_single_single, groupCohomology.H1IsoOfIsTrivial_inv_apply, Rep.instPreservesProjectiveObjectsActionModuleCatSubtypeMemSubgroupResSubtype, groupHomology.π_comp_H2Iso_inv_assoc, ModuleCat.instPreservesFiniteColimitsUliftFunctor, PresheafOfModules.map_comp_apply, ModuleCat.biprodIsoProd_inv_comp_snd_apply, ModuleCat.RestrictionCoextensionAdj.counit'_app, groupHomology.chainsMap_f_3_comp_chainsIso₃, PresheafOfModules.pushforward_map_app_apply', groupHomology.mapCycles₁_id_comp_assoc, groupHomology.eq_d₂₁_comp_inv, groupHomology.shortComplexH2_f, CoalgCat.comonEquivalence_counitIso, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, CategoryTheory.linearYoneda_obj_obj_carrier, Rep.instLinearModuleCatObjFunctorCoinvariantsTensor, ModuleCat.MonoidalCategory.whiskerLeft_def, groupCohomology.H2π_comp_map_apply, groupHomology.mapCycles₁_comp, groupHomology.map_comp, FDRep.instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, Rep.ihom_ev_app_hom, ModuleCat.homLinearEquiv_symm_apply, Profinite.NobelingProof.succ_exact, ModuleCat.hom_smul, groupCohomology.dArrowIso₀₁_hom_right, FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite, ModuleCat.uliftFunctorForgetIso_hom_app, groupCohomology.π_map_assoc, Rep.MonoidalClosed.linearHomEquivComm_hom, CompHausLike.LocallyConstantModule.functorToPresheaves_map_app, ModuleCat.smul_naturality, CategoryTheory.ShortComplex.moduleCat_zero_apply, groupCohomology.toCocycles_comp_isoCocycles₂_hom, CompHausLike.LocallyConstantModule.functor_map_val, Rep.coe_linearization_obj, Rep.instIsRightAdjointModuleCatInvariantsFunctor, groupCohomology.map_comp, FGModuleCat.hom_comp, SheafOfModules.evaluationPreservesLimitsOfSize, groupHomology.map_id_comp, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, CategoryTheory.faithful_linearYoneda, ModuleCat.imageIsoRange_hom_subtype, groupHomology.mapCycles₁_comp_i, ModuleCat.CoextendScalars.smul_apply, Rep.coinvariantsTensorIndIso_inv, groupCohomology.shortComplexH0_f, ModuleCat.binaryProductLimitCone_cone_π_app_right, groupCohomology.shortComplexH0_g, groupCohomology.cocyclesOfIsCocycle₁_coe, ModuleCat.exteriorPower.desc_mk, PresheafOfModules.unit_map_one, groupHomology.functor_obj, PresheafOfModules.zsmul_app, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom, ModuleCat.matrixEquivalence_functor, ModuleCat.HasColimit.colimitCocone_pt_isModule, groupCohomology.shortComplexH1_f, ModuleCat.hasLimits, groupCohomology.coboundaries₂_le_cocycles₂, CategoryTheory.preadditiveYoneda_obj, CategoryTheory.linearCoyoneda_obj_obj_isAddCommGroup, Rep.standardComplex.εToSingle₀_comp_eq, ModuleCat.MonoidalCategory.tensorHom_def, groupHomology.inhomogeneousChains.d_def, PresheafOfModules.isoMk_hom_app, Rep.coindVEquiv_symm_apply_coe, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId, ModuleCat.restrictScalarsId'App_inv_naturality, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, ModuleCat.imageIsoRange_inv_image_ι_apply, Rep.homEquiv_def, Rep.indCoindIso_hom_hom_hom, CategoryTheory.preadditiveYonedaMap_app, groupCohomology.comp_d₂₃_eq, CondensedMod.isDiscrete_iff_isDiscrete_forget, PresheafOfModules.map_smul, FGModuleCat.FGModuleCatEvaluation_apply, ModuleCat.epi_iff_surjective, ModuleCat.restrictScalarsId'_inv_app, groupCohomology.coboundaries₂.val_eq_coe, AlgebraicGeometry.instFullModuleCatCarrierModulesSpecOfFunctor, PresheafOfModules.Monoidal.tensorObj_map_tmul, ModuleCat.exteriorPower.map_mk, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom, ModuleCat.extendScalars_assoc_assoc, groupHomology.H1CoresCoinf_X₁, Rep.ofModuleMonoidAlgebra_obj_coe, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, ModuleCat.id_apply, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_iff, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, groupCohomology.infNatTrans_app, FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂LinearMapIdCarrierObjIsFG, groupCohomology.d₁₂_apply_mem_cocycles₂, Rep.invariantsAdjunction_unit_app, ModuleCat.hom_inv_apply, groupHomology.mapCycles₂_id_comp, Rep.diagonal_succ_projective, CategoryTheory.ShortComplex.moduleCatMk_X₃_isAddCommGroup, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, ModuleCat.monoidalClosed_curry, groupCohomology.d₀₁_apply_mem_cocycles₁, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc, ModuleCat.exteriorPower.iso₁_hom_naturality, ModuleCat.hasColimitsOfSize, PresheafOfModules.instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation, Module.Flat.iff_rTensor_preserves_shortComplex_exact, groupHomology.cyclesMap_comp_assoc, ModuleCat.MonoidalCategory.leftUnitor_hom_apply, Rep.indToCoindAux_fst_mul_inv, Rep.instIsLeftAdjointActionModuleCatRes, CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj, ModuleCat.exteriorPower.iso₀_hom_apply, 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, ModuleCat.restrictScalarsId'App_hom_apply, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, groupCohomology.subtype_comp_d₀₁_apply, SheafOfModules.pushforwardComp_inv_app_val_app, LightCondensed.internallyProjective_iff_tensor_condition, ModuleCat.FilteredColimits.forget_preservesFilteredColimits, groupCohomology.H2π_eq_iff, CoalgCat.toComonObj_X, groupCohomology.cochainsMap_f_map_epi, groupCohomology.comp_d₀₁_eq, FGModuleCat.instIsMonoidalClosedModuleCatIsFG, Rep.instProjective, groupCohomology.cocycles₂_map_one_snd, ModuleCat.restrictScalarsId'App_hom_naturality_assoc, ModuleCat.homAddEquiv_symm_apply_hom, LinearMap.shortExact_shortComplexKer, Rep.coinvariantsTensorFreeLEquiv_apply, groupHomology.coinvariantsMk_comp_H0Iso_inv, ModuleCat.image.lift_fac, groupHomology.toCycles_comp_isoCycles₁_hom_apply, TannakaDuality.FiniteGroup.sumSMulInv_apply, Module.Flat.iff_lTensor_preserves_shortComplex_exact, CategoryTheory.ShortComplex.moduleCatMk_X₃_carrier, groupHomology.mapCycles₂_comp_i, Rep.coinvariantsTensorIndIso_hom, groupCohomology.map_H0Iso_hom_f, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_zero_iff, PresheafOfModules.mono_iff_surjective, Rep.barResolution_complex, ModuleCat.ExtendScalars.map'_id, groupHomology.boundariesOfIsBoundary₁_coe, PresheafOfModules.freeObj_map, ModuleCat.instPreservesFiniteColimitsLocalizationLocalizedModule_functor, FDRep.instFiniteDimensionalCarrierVFGModuleCat, FGModuleCat.instFiniteHom, groupCohomology.cochainsMap_zero, Rep.indToCoindAux_comm, ModuleCat.smulShortComplex_X₁, groupCohomology.dArrowIso₀₁_inv_left, groupCohomology.π_comp_H1Iso_hom, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff, groupHomology.map_comp_assoc, Rep.coinvariantsTensorIndNatIso_inv_app, AlgebraicGeometry.tilde.isoTop_hom, ModuleCat.Tilde.toOpen_res, groupHomology.cyclesIso₀_comp_H0π_apply, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, groupHomology.eq_d₃₂_comp_inv_apply, CondensedMod.epi_iff_surjective_on_stonean, FDRep.average_char_eq_finrank_invariants, ModuleCat.hom_whiskerRight, Rep.instAdditiveModuleCatObjFunctorCoinvariantsTensor, groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv, ModuleCat.hom_inv_associator, PresheafOfModules.instEpiModuleCatCarrierObjOppositeRingCatApp, FGModuleCat.hom_id, Rep.toAdditive_symm_apply, groupCohomology.H1InfRes_X₂, ModuleCat.lof_coprodIsoDirectSum_inv, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, groupCohomology.map₁_one, Rep.coindResAdjunction_unit_app, groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂, CategoryTheory.linearYoneda_map_app, instAB4ModuleCat, CommRingCat.moduleCatRestrictScalarsPseudofunctor_map, CoalgCat.comul_def, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i, ModuleCat.inv_hom_apply, ModuleCat.forget₂AddCommGroup_preservesLimits, CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj, ModuleCat.directLimitIsColimit_desc, CategoryTheory.preadditiveYonedaObj_obj_isModule, groupHomology.mapCycles₁_id_comp_apply, ModuleCat.MonoidalCategory.rightUnitor_def, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_assoc, groupHomology.H1CoresCoinf_g, CategoryTheory.Iso.toLinearEquiv_symm, groupCohomology.cochainsMap_id_comp, PresheafOfModules.presheaf_map_apply_coe, ModuleCat.smulShortComplex_g, ModuleCat.directLimitCocone_pt_isAddCommGroup, Rep.ofMulDistribMulAction_ρ_apply_apply, groupCohomology.map_id, CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding, groupCohomology.mapShortComplexH2_comp, ModuleCat.ExtendScalars.map'_comp, groupCohomology.shortComplexH2_f, CategoryTheory.linearYoneda_obj_obj_isAddCommGroup, simple_iff_isSimpleModule, ModuleCat.restrictScalarsComp'App_hom_naturality_assoc, Rep.instIsTrivialCarrierVModuleCatOfCompLinearMapIdρ, groupCohomology.instEpiModuleCatH1π, ModuleCat.MonoidalCategory.associator_def, groupHomology.H1CoresCoinfOfTrivial_X₂, groupHomology.H1CoresCoinf_X₂, IsProjective.iff_projective, groupCohomology.H2π_comp_map, groupCohomology.cochainsMap_comp_assoc, TopModuleCat.instIsRightAdjointModuleCatIndiscrete, FGModuleCat.instFiniteCarrierLimitModuleCatCompForget₂LinearMapIdObjIsFG, ModuleCat.mono_iff_injective, groupHomology.π_comp_H2Iso_hom, ModuleCat.forget₂_obj, CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj', TopModuleCat.instIsLeftAdjointModuleCatWithModuleTopology, Rep.indResAdjunction_counit_app_hom_hom, FDRep.hom_hom_action_ρ, CompHausLike.LocallyConstantModule.functor_obj_val, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects, FGModuleCat.FGModuleCatDual_obj, AlgebraicGeometry.tilde.functor_map, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, Rep.coindToInd_apply, PresheafOfModules.forgetToPresheafModuleCatObjMap_apply, groupHomology.mapCycles₁_comp_i_apply, SheafOfModules.pushforwardCongr_hom_app_val_app, ModuleCat.hom_whiskerLeft, groupHomology.chainsMap_f_map_epi, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_iff, AlgCat.forget₂Module_preservesLimitsOfSize, groupHomology.mapCycles₂_comp, ModuleCat.comp_apply, ModuleCat.restrictScalarsCongr_hom_app, ModuleCat.MonoidalCategory.tensorUnit_carrier, ModuleCat.kernelIsoKer_inv_kernel_ι_apply, groupHomology.isoShortComplexH1_hom, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply, groupHomology.cyclesIso₀_inv_comp_cyclesMap_apply, CategoryTheory.whiskering_linearYoneda, Rep.coe_of, ModuleCat.MonoidalCategory.rightUnitor_hom_apply, groupCohomology.mono_map_0_of_mono, Condensed.instHasLimitsOfSizeModuleCat, groupCohomology.isoCocycles₂_hom_comp_i, CoalgCat.MonoidalCategory.inducingFunctorData_μIso, CoalgCat.MonoidalCategory.inducingFunctorData_εIso, ModuleCat.FilteredColimits.M.mk_map, groupCohomology.π_comp_H0Iso_hom_apply, ModuleCat.instIsRightAdjointRestrictScalars, Rep.resIndAdjunction_homEquiv_symm_apply, groupHomology.coe_mapCycles₂, Rep.coinvariantsFunctor_hom_ext_iff, LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim, CategoryTheory.whiskering_linearCoyoneda₂, FGModuleCat.obj_carrier, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.comp_d₁₀_eq, groupHomology.H1π_comp_map_apply, ModuleCat.localizedModule_functor_map, Rep.instLinearModuleCatCoinvariantsFunctor, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', FGModuleCat.FGModuleCatCoevaluation_apply_one, Rep.coindMap'_hom, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₂, Rep.normNatTrans_app, groupHomology.H0π_comp_map_assoc, instHasExtModuleCatOfSmall, groupCohomology.dArrowIso₀₁_hom_left, instHasLimitsCondensedMod, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, groupHomology.π_comp_H0Iso_hom_apply, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, groupCohomology.eq_d₀₁_comp_inv_apply, groupCohomology.H1InfRes_X₃, ModuleCat.MonoidalCategory.tensorLift_tmul, simple_of_isSimpleModule, Rep.applyAsHom_comm_assoc, MatrixModCat.toModuleCat_obj_carrier, Rep.instEpiModuleCatAppActionCoinvariantsMk, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, groupCohomology.cocycles₁_map_inv, Rep.freeLiftLEquiv_apply, ModuleCat.hom_hom_leftUnitor, groupHomology.chainsFunctor_obj, groupCohomology.mapCocycles₁_one, Rep.instEnoughProjectives, PresheafOfModules.surjective_of_epi, groupCohomology.instMonoModuleCatFShortComplexH0, FGModuleCat.instFiniteCarrierPiObjModuleCatOfFinite, ModuleCat.adj_homEquiv, groupCohomology.functor_obj, groupCohomology.cocyclesMap_comp, CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective, groupHomology.H2π_comp_map_assoc, AlgebraicGeometry.tilde.map_comp_assoc, Rep.indToCoindAux_mul_fst, ModuleCat.hom_hom_rightUnitor, LightCondensed.forget_map_val_app, ModuleCat.biprodIsoProd_inv_comp_snd, groupHomology.π_comp_H0IsoOfIsTrivial_hom_apply, ModuleCat.piIsoPi_inv_kernel_ι_apply, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, Rep.ihom_obj_ρ_apply, Rep.instPreservesZeroMorphismsModuleCatInvariantsFunctor, AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_app_assoc, CondensedMod.hom_naturality_apply, ModuleCat.instIsLeftAdjointRestrictScalars, ModuleCat.lof_coprodIsoDirectSum_inv_apply, Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, groupHomology.d₁₀ArrowIso_inv_right, FDRep.instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, ModuleCat.Derivation.desc_d, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv, TannakaDuality.FiniteGroup.equivApp_inv, Rep.finsuppTensorRight_hom_hom, QuadraticModuleCat.forget₂_map_associator_hom, ModuleCat.exteriorPower.iso₀_hom_naturality_assoc, groupCohomology.resNatTrans_app, PresheafOfModules.injective_of_mono, ModuleCat.free_ε_one, PresheafOfModules.isoMk_inv_app, groupCohomology.norm_ofAlgebraAutOnUnits_eq, groupCohomology.π_comp_H0Iso_hom_assoc, groupCohomology.π_map, CategoryTheory.full_linearCoyoneda, TannakaDuality.FiniteGroup.forget_map, ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier, ModuleCat.imageIsoRange_hom_subtype_assoc, groupCohomology.mem_cocycles₂_iff, groupCohomology.mapShortComplexH2_zero, CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj, Rep.tensor_ρ, Rep.resIndAdjunction_homEquiv_apply, Rep.toAdditive_apply, PresheafOfModules.pushforward_obj_map_apply, groupHomology.chainsMap_id_f_map_epi, groupCohomology.H2π_comp_map_assoc, groupHomology.d₁₀_comp_coinvariantsMk, groupHomology.d₂₁_comp_d₁₀_apply, AlgebraicGeometry.tilde.isIso_toOpen_top, 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, CategoryTheory.faithful_linearCoyoneda, ModuleCat.smulNatTrans_apply_app, FGModuleCat.ihom_obj, groupCohomology.cochainsMap_id_f_map_mono, CoalgCat.comonEquivalence_functor, Rep.quotientToInvariantsFunctor_map_hom, groupHomology.chainsMap_id_comp, ModuleCat.forget_reflectsLimits, Rep.leftRegularHomEquiv_symm_apply, TannakaDuality.FiniteGroup.equivApp_hom, ModuleCat.uliftFunctorForgetIso_inv_app, FDRep.char_linHom, Rep.quotientToCoinvariantsFunctor_map_hom, groupHomology.instEpiModuleCatGH1CoresCoinf, groupCohomology.mapShortComplexH1_id, CommRingCat.moduleCatExtendScalarsPseudofunctor_map, Rep.coinvariantsShortComplex_g, groupHomology.H2π_eq_iff, FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, ModuleCat.reflectsIsomorphisms_extendScalars_of_faithfullyFlat, ModuleCat.ExtendRestrictScalarsAdj.homEquiv_symm_apply, groupHomology.H1AddEquivOfIsTrivial_single, LightCondMod.instReflectsEpimorphismsLightCondSetForget, CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective, groupCohomology.mem_cocycles₁_iff, groupHomology.mapShortComplexH1_id_comp, CoalgCat.ofComonObjCoalgebraStruct_comul, ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, groupHomology.mapShortComplexH1_comp, groupHomology.range_d₁₀_eq_coinvariantsKer, PresheafOfModules.unitHomEquiv_apply_coe, Rep.coindResAdjunction_homEquiv_apply, groupCohomology.inhomogeneousCochains.d_comp_d, ModuleCat.FreeMonoidal.εIso_inv_freeMk, groupHomology.isoCycles₂_hom_comp_i_apply, Rep.Tor_map, Rep.ofModuleMonoidAlgebra_obj_ρ, PresheafOfModules.freeObj_obj, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, Rep.coinvariantsShortComplex_f, SheafOfModules.pushforwardCongr_inv_app_val_app, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, Rep.resIndAdjunction_counit_app, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, groupCohomology.isoCocycles₁_inv_comp_iCocycles, groupHomology.π_comp_H0IsoOfIsTrivial_hom, ModuleCat.RestrictionCoextensionAdj.unit'_app, ModuleCat.matrixEquivalence_unitIso, groupHomology.eq_d₂₁_comp_inv_assoc, ModuleCat.imageIsoRange_inv_image_ι, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom, Rep.ofMulActionSubsingletonIsoTrivial_inv_hom, ModuleCat.smulShortComplex_X₃_carrier, RingCat.moduleCatRestrictScalarsPseudofunctor_mapId, ModuleCat.free_η_freeMk, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective, Rep.instIsLeftAdjointModuleCatCoinvariantsFunctor, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom, ModuleCat.Algebra.instLinearRestrictScalars, groupHomology.inhomogeneousChains.d_single, groupCohomology.coboundariesOfIsCoboundary₁_coe, groupCohomology.mapShortComplexH2_τ₁, FGModuleRepr.instIsEquivalenceFGModuleCatEmbed, groupHomology.cyclesIso₀_inv_comp_iCycles, ModuleCat.instReflectsIsomorphismsRestrictScalars, ModuleCat.exteriorPower.iso₁_hom_apply, FGModuleCat.instHasFiniteColimits, Representation.coind'_apply_apply, groupCohomology.d₁₂_comp_d₂₃_assoc, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_map, SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app, Rep.diagonalOneIsoLeftRegular_inv_hom, ModuleCat.hom_inv_rightUnitor, ModuleCat.ExtendScalars.smul_tmul, LightCondensed.free_internallyProjective_iff_tensor_condition', groupHomology.map_id_comp_H0Iso_hom_assoc, instHasLimitsOfSizeCondensedMod, ModuleCat.hom_sum, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_mon, ModuleCat.restrictScalarsComp'App_hom_naturality, QuadraticModuleCat.forget₂_obj, FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, CommRingCat.moduleCatExtendScalarsPseudofunctor_obj, groupCohomology.mapShortComplexH2_id_comp_assoc, groupHomology.mapCycles₂_id_comp_assoc, groupHomology.π_comp_H1Iso_hom_apply, Rep.coindIso_inv_hom_hom, ModuleCat.hom_nsmul, groupHomology.mapShortComplexH2_comp, groupCohomology.map_id_comp_H0Iso_hom_apply, groupCohomology.cocycles₁_map_mul_of_isTrivial, ModuleCat.forget_obj, ModuleCat.directLimitDiagram_obj_isAddCommGroup, groupCohomology.subtype_comp_d₀₁_assoc, groupHomology.chainsMap_id_f_hom_eq_mapRange, CategoryTheory.preservesLimits_preadditiveYonedaObj, PresheafOfModules.toPresheaf_map_app_apply, groupHomology.toCycles_comp_isoCycles₂_hom, CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact, groupCohomology.map_id_comp_H0Iso_hom, CoalgCat.comonEquivalence_unitIso, groupHomology.cyclesMap_comp_isoCycles₂_hom_apply, PresheafOfModules.neg_app, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply, ModuleCat.HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, groupHomology.mapShortComplexH2_τ₂, groupHomology.mapCycles₁_id_comp, Rep.trivialFunctor_obj_V, Rep.indToCoindAux_mul_snd, ModuleCat.FilteredColimits.forget₂AddCommGroup_preservesFilteredColimits, ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier, ModuleCat.homEquiv_extendScalarsComp, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, QuadraticModuleCat.toModuleCat_tensor, ModuleCat.ExtendScalars.map_tmul, ModuleCat.FilteredColimits.colimit_add_mk_eq', PresheafOfModules.map_comp, ModuleCat.FilteredColimits.forget_reflectsFilteredColimits, RingCat.moduleCatRestrictScalarsPseudofunctor_map, groupCohomology.cocyclesOfIsMulCocycle₂_coe, groupHomology.chainsMap_f_map_mono, LinearMap.id_moduleCat_comp, ModuleCat.restrictScalarsComp'App_inv_naturality, ModuleCat.free_μ_freeMk_tmul_freeMk, ModuleCat.forget₂_obj_moduleCat_of, groupHomology.shortComplexH0_f, groupHomology.eq_d₁₀_comp_inv, CategoryTheory.Iso.toLinearEquiv_apply, Rep.diagonalSuccIsoTensorTrivial_hom_hom_single, FDRep.instHasKernels, ModuleCat.instHasZeroObject, PresheafOfModules.evaluation_preservesColimitsOfSize, groupHomology.isoShortComplexH1_inv, groupCohomology.coboundariesOfIsMulCoboundary₁_coe, SheafOfModules.pushforwardComp_hom_app_val_app, 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, ModuleCat.MonoidalCategory.tensorObj, ModuleCat.restrictScalarsComp'App_inv_naturality_assoc, groupHomology.isoCycles₁_hom_comp_i_apply, LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, groupHomology.mapShortComplexH1_τ₁, PresheafOfModules.evaluation_preservesFiniteLimits, SheafOfModules.Presentation.map_relations_I, FGModuleCat.Iso.conj_eq_conj, ModuleCat.instPreservesColimitsOfSizeAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrierOfHasColimitsOfSizeAddCommGrpMax, ModuleCat.hasCokernels_moduleCat, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, ModuleCat.FreeMonoidal.μIso_hom_freeMk_tmul_freeMk, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, CategoryTheory.ShortComplex.exact_iff_surjective_moduleCatToCycles, ModuleCat.imageIsoRange_inv_image_ι_assoc, ModuleCat.MonoidalCategory.rightUnitor_inv_apply, groupCohomology.H1π_eq_zero_iff, groupHomology.H1AddEquivOfIsTrivial_symm_apply, Rep.invariantsAdjunction_counit_app_hom, PresheafOfModules.sub_app, groupHomology.cyclesMap_comp_cyclesIso₀_hom, Profinite.NobelingProof.GoodProducts.square_commutes, groupCohomology.cochainsMap_f, groupCohomology.coboundaries₁.val_eq_coe, groupHomology.d₃₂_single_one_fst, inhomogeneousCochains.d_hom_apply, Rep.coind'_ext_iff, CoalgCat.counit_def, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d, groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply, groupHomology.chainsMap_comp, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, groupHomology.d₂₁_comp_d₁₀, PresheafOfModules.Elements.fromFreeYoneda_app_apply, ModuleCat.binaryProductLimitCone_cone_π_app_left, ModuleCat.HasColimit.coconePointSMul_apply, PresheafOfModules.pushforward_obj_obj, Rep.instLinearModuleCatInvariantsFunctor, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, ModuleCat.kernelIsoKer_hom_ker_subtype, ModuleCat.projective_of_categoryTheory_projective, ModuleCat.smulShortComplex_f, SheafOfModules.Presentation.mapRelations_mapGenerators, ModuleCat.hasLimitsOfShape, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, ModuleCat.hom_add, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, groupHomology.H1ToTensorOfIsTrivial_H1π_single, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc_apply, FGModuleCat.hom_hom_comp, Rep.FiniteCyclicGroup.groupHomologyπEven_eq_zero_iff, Rep.ofMulActionSubsingletonIsoTrivial_hom_hom, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_carrier, instEnoughInjectivesModuleCatOfSmall, groupCohomology.cocyclesMk₁_eq, AlgCat.forget₂_module_obj, isZero_groupCohomology_succ_of_subsingleton, ModuleCat.MonoidalCategory.leftUnitor_inv_apply, groupCohomology.map_id_comp_assoc, ModuleCat.ι_coprodIsoDirectSum_hom, ModuleCat.instReflectsIsomorphismsAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, SheafOfModules.relationsOfIsCokernelFree_I, ModuleCat.MonModuleEquivalenceAlgebra.algebraMap, ModuleCat.MonoidalCategory.tensorμ_apply, Rep.linearizationTrivialIso_inv_hom, Rep.isZero_Tor_succ_of_projective, groupHomology.cyclesOfIsCycle₁_coe, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, groupCohomology.H1InfRes_X₁, Rep.quotientToInvariantsFunctor_obj_V, FDRep.char_one, groupHomology.shortComplexH0_exact, ModuleCat.MonoidalCategory.tensorObj_isModule, groupHomology.inhomogeneousChains.ext_iff, FGModuleCat.hom_ext_iff, CategoryTheory.Abelian.FreydMitchell.instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor, ModuleCat.MonoidalCategory.tensorObj_isAddCommGroup, groupHomology.d₂₁_apply_mem_cycles₁, groupCohomology.coboundariesToCocycles₂_apply, ModuleCat.ihom_map_apply, LightCondMod.LocallyConstant.instFaithfulModuleCatLightCondensedDiscrete, ModuleCat.instAdditiveRestrictScalars, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul, ModuleCat.ihom_coev_app, 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, Rep.coinvariantsTensorIndNatIso_hom_app, groupHomology.π_map_assoc, PresheafOfModules.instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation, groupHomology.congr, groupCohomology.mapCocycles₁_comp_i_assoc, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, Rep.applyAsHom_comm, groupCohomology.cocycles₁.val_eq_coe, ModuleCat.instAdditiveUliftFunctor, TannakaDuality.FiniteGroup.sumSMulInv_single_id, PresheafOfModules.Hom.naturality_assoc, groupCohomology.H1π_comp_map_apply, Rep.leftRegularHom_hom_single, groupCohomology.cocycles₁_map_one, groupHomology.eq_d₃₂_comp_inv_assoc, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, ModuleCat.hom_hom_associator, CoalgCat.forget₂_obj, groupCohomology.π_comp_H2Iso_hom_assoc, groupCohomology.H1InfRes_g, instHasLimitsOfSizeLightCondMod_1, CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective, CategoryTheory.linearCoyoneda_obj_map, Rep.standardComplex.d_comp_ε, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₃, FDRep.simple_iff_end_is_rank_one, Rep.finsuppTensorRight_inv_hom, ModuleCat.matrixEquivalence_counitIso, Rep.coinvariantsMk_app_hom, Rep.ihom_obj_V_isAddCommGroup, CategoryTheory.linearYoneda_obj_additive, Rep.indCoindNatIso_inv_app, groupHomology.shortComplexH2_g, AddCommGrpCat.injective_as_module_iff, PresheafOfModules.restriction_app, groupCohomology.mapShortComplexH1_id_comp, PresheafOfModules.ι_fromFreeYonedaCoproduct_apply, CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range, CategoryTheory.ShortComplex.moduleCat_exact_iff, groupCohomology.cocyclesMap_comp_assoc, groupHomology.mapCycles₂_hom, groupHomology.isoCycles₂_inv_comp_iCycles_apply, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, ModuleCat.mkOfSMul_smul, groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor, groupHomology.isoShortComplexH2_hom, Rep.coindResAdjunction_homEquiv_symm_apply, LightCondMod.LocallyConstant.instFaithfulModuleCatFunctor, ModuleCat.instMonoι, ModuleCat.restrictScalars.smul_def, ModuleCat.kernelIsoKer_hom_ker_subtype_apply, ModuleCat.exteriorPower.iso₁_hom_naturality_assoc, CategoryTheory.preadditiveYonedaObj_obj_isAddCommGroup, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, ModuleCat.restrictScalarsId'_hom_app, Rep.coindVEquiv_apply_hom, groupCohomology.mapShortComplexH1_comp, groupCohomology.cocyclesMap_comp_isoCocycles₂_hom_assoc, groupHomology.H1π_eq_zero_iff, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, groupHomology.π_comp_H1Iso_hom_assoc, LightCondMod.hom_naturality_apply, PresheafOfModules.forgetToPresheafModuleCat_obj, groupHomology.chainsMap_f_2_comp_chainsIso₂, groupHomology.d₂₁_single_one_fst, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, ModuleCat.HasLimit.productLimitCone_cone_pt_isModule, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, PresheafOfModules.forgetToPresheafModuleCatObj_obj, groupHomology.pOpcycles_comp_opcyclesIso_hom, groupHomology.H2π_comp_map, Rep.trivialFunctor_map_hom, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, Module.injective_iff_injective_object, groupCohomology.cocycles₂.val_eq_coe, groupHomology.cyclesIso₀_inv_comp_cyclesMap_assoc, groupHomology.π_comp_H2Iso_inv, groupCohomology.eq_d₂₃_comp_inv, ModuleCat.instMonoidalLinear, Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_iff, groupCohomology.cochainsMap_f_map_mono, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_f, LightCondensed.ihomPoints_symm_apply, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, groupCohomology.isoShortComplexH1_hom, groupHomology.mapShortComplexH1_id, PresheafOfModules.Monoidal.tensorHom_app, ModuleCat.instFaithfulUliftFunctor, groupHomology.H1π_comp_map_assoc, groupCohomology.map_id_comp, Rep.ihom_map_hom, groupHomology.instEpiModuleCatH1π, ModuleCat.piIsoPi_hom_ker_subtype_apply, ModuleCat.reflectsColimitsOfShape, FGModuleCat.instHasLimitsOfShapeOfFinCategory, RingCat.moduleCatRestrictScalarsPseudofunctor_obj, groupHomology.H1AddEquivOfIsTrivial_apply, ModuleCat.MonoidalCategory.whiskerRight_apply, groupCohomology.isoCocycles₂_inv_comp_iCocycles, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, Rep.coinvariantsTensor_hom_ext_iff, Rep.finsuppTensorLeft_inv_hom, ModuleCat.instPreservesLimitsOfSizeUliftFunctor, ModuleCat.free_δ_freeMk, FGModuleCat.instFullUlift, ModuleCat.forget₂AddCommGroup_reflectsLimitOfSize, PresheafOfModules.instMonoModuleCatCarrierObjOppositeRingCatApp, ModuleCat.FilteredColimits.ι_colimitDesc, CoalgCat.forget₂_map, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, Rep.unit_iso_comm, Rep.leftRegularHomEquiv_symm_single, ModuleCat.restrictScalarsEquivalenceOfRingEquiv_additive, inhomogeneousCochains.d_eq, ModuleCat.HasLimit.productLimitCone_cone_pt_carrier, groupHomology.instEpiModuleCatH2π, groupHomology.H1CoresCoinfOfTrivial_exact, MoritaEquivalence.instAdditiveModuleCatFunctorEqv, Rep.FiniteCyclicGroup.resolution_complex, ModuleCat.piIsoPi_hom_ker_subtype, ModuleCat.directLimitDiagram_obj_carrier, groupHomology.chainsFunctor_map, ModuleCat.hom_id, groupCohomology.cocyclesMk₂_eq, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, Rep.leftRegularTensorTrivialIsoFree_inv_hom, ModuleCat.extendScalars_id_comp_assoc, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_norm, LinearEquiv.toFGModuleCatIso_hom, TopModuleCat.instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, AlgebraicGeometry.instFaithfulModuleCatCarrierModulesSpecOfFunctor, groupCohomology.cochainsMap_id_f_map_epi, instAB5ModuleCat, groupHomology.H1π_comp_map, groupHomology.chainsMap_f_hom, AlgCat.forget₂Module_preservesLimits, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles, groupHomology.d₃₂_apply_mem_cycles₂, ModuleCat.MonoidalCategory.tensorUnit_isModule, ModuleCat.extendScalars_assoc', ModuleCat.piIsoPi_inv_kernel_ι, LightCondMod.LocallyConstant.instFullModuleCatFunctor, Rep.norm_hom, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt_apply, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, TopModuleCat.instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, Rep.indResAdjunction_unit_app_hom_hom, CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaObj, Rep.ofHom_ρ, groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply, groupHomology.map_id_comp_H0Iso_hom_apply, ModuleCat.extendScalars_id_comp, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom, groupHomology.boundariesOfIsBoundary₂_coe, AlgebraicGeometry.tilde.map_add, RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, groupHomology.cyclesMk₁_eq, groupHomology.H1CoresCoinfOfTrivial_f, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, groupHomology.cyclesIso₀_comp_H0π_assoc, Rep.coindFunctor'_obj, LightCondensed.ihom_map_val_app, groupHomology.mapCycles₂_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i, ModuleCat.wellPowered_moduleCat, FGModuleCat.tensorObj_obj, FGModuleCat.tensorUnit_obj, ModuleCat.FreeMonoidal.μIso_inv_freeMk, ModuleCat.uliftFunctor_map, Rep.Action_ρ_eq_ρ, Rep.linearization_δ_hom, groupHomology.functor_map, groupHomology.instEpiModuleCatH0π, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, groupCohomology.H1InfRes_exact, ModuleCat.instPreservesFiniteLimitsUliftFunctor, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup, groupCohomology.mapShortComplexH2_τ₂, groupCohomology.mapCocycles₁_comp_i_apply, ModuleCat.hom_zsmul, Rep.coindMap_hom, instHasFiniteLimitsLightCondMod, groupHomology.mapCycles₂_id_comp_apply, ChainComplex.linearYonedaObj_d, Rep.standardComplex.instQuasiIsoNatεToSingle₀, Rep.trivial_def, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc, groupCohomology.cocycles₂_ext_iff, ModuleCat.finite_ext, Rep.standardComplex.x_projective, ModuleCat.ExtendRestrictScalarsAdj.counit_app, ModuleCat.directLimitCocone_ι_app, AlgebraicGeometry.tilde.toOpen_res, AlgebraicGeometry.tilde.toOpen_res_assoc, CategoryTheory.ShortComplex.moduleCatMk_X₁_isModule, FGModuleCat.instHasFiniteLimits, CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, instFiniteCarrierObjModuleCatIsFG, Rep.MonoidalClosed.linearHomEquiv_hom, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, Rep.invariantsAdjunction_homEquiv_apply_hom, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, isZero_Ext_succ_of_projective, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, CategoryTheory.full_linearYoneda, CategoryTheory.Abelian.preadditiveCoyonedaObj_map_surjective, Rep.hom_comm_apply, SheafOfModules.pushforwardNatTrans_app_val_app, groupHomology.H2π_comp_map_apply, ModuleCat.Hom.hom₂_apply, Rep.instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype, ModuleCat.HasColimit.colimitCocone_pt_carrier, CondensedMod.epi_iff_locallySurjective_on_compHaus, CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker, Rep.FiniteCyclicGroup.resolution_quasiIso, ModuleCat.uliftFunctor_obj, ModuleCat.forget₂_addCommGrp_additive, Module.Flat.iff_preservesFiniteLimits_tensorLeft, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, groupCohomology.H1Map_id, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, groupCohomology.cochainsMap_f_hom, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₁, groupCohomology.coboundaries₁_ext_iff, Rep.finsuppTensorLeft_hom_hom, Rep.indFunctor_map, groupHomology.H1CoresCoinfOfTrivial_g, Rep.FiniteCyclicGroup.groupHomologyπOdd_eq_iff, groupHomology.inhomogeneousChains.d_comp_d, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K, ModuleCat.instFaithfulRestrictScalars, MatrixModCat.toModuleCat_map, groupHomology.π_comp_H0Iso_hom, PresheafOfModules.map_id, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp, ModuleCat.MonoidalCategory.leftUnitor_def, groupCohomology.mapShortComplexH1_id_comp_assoc, groupCohomology.π_comp_H2Iso_hom_apply, ModuleCat.HasLimit.lift_hom_apply, groupCohomology.mapShortComplexH1_zero, ModuleCat.binaryProductLimitCone_isLimit_lift, IsSMulRegular.smulShortComplex_shortExact, CategoryTheory.ShortComplex.moduleCatMk_f, ModuleCat.homLinearEquiv_apply, groupCohomology.mapShortComplexH1_comp_assoc, Rep.coinvariantsTensorMk_apply, groupHomology.cyclesIso₀_inv_comp_cyclesMap, ModuleCat.localizedModule_functor_obj, instHasLimitsOfSizeLightCondMod, ModuleCat.instProjectiveObjFree, Rep.indMap_hom, groupHomology.H0π_comp_H0Iso_hom, CategoryTheory.Abelian.FreydMitchell.instPreservesFiniteColimitsModuleCatEmbeddingRingFunctor, groupHomology.isoCycles₁_hom_comp_i_assoc, Rep.coinvariantsShortComplex_X₁, Rep.homEquiv_symm_apply_hom, Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_sub, CategoryTheory.linearYoneda_obj_obj_isModule, AlgCat.forget₂_module_map, ModuleCat.FilteredColimits.M.mk_surjective, FDRep.forget₂_ρ, ModuleCat.extendScalarsComp_hom_app_one_tmul, Rep.invariantsFunctor_map_hom, ModuleCat.Iso.conj_eq_conj, instHasColimitsCondensedMod, groupHomology.map_id_comp_H0Iso_hom, groupCohomology.isoShortComplexH2_hom, linearEquivIsoModuleIso_inv, groupHomology.d₁₀_eq_zero_of_isTrivial, CoalgCat.toComon_map_hom, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc, groupCohomology.π_comp_H1Iso_hom_apply, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, groupCohomology.d₀₁_comp_d₁₂_assoc, groupCohomology.cocyclesMap_id, Rep.instIsRightAdjointActionModuleCatRes, ModuleCat.MonoidalCategory.tensorObj_def, AlgebraicGeometry.tilde.map_zero, ModuleCat.preservesFiniteLimits_tensorLeft_of_ringHomFlat, FDRep.instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing, groupHomology.d₂₁_single_one_snd, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, Rep.norm_comm_assoc, groupCohomology.mapShortComplexH2_id_comp, groupHomology.π_comp_H0IsoOfIsTrivial_hom_assoc, CategoryTheory.ShortComplex.moduleCatMk_X₃_isModule, FDRep.instFiniteCarrierVFGModuleCat, ModuleCat.biprodIsoProd_inv_comp_fst, groupHomology.π_map_apply, CategoryTheory.Abelian.FreydMitchell.instFullModuleCatEmbeddingRingFunctor, Rep.resIndAdjunction_unit_app, ModuleCat.instIsLeftAdjointExtendScalars, groupHomology.d₃₂_comp_d₂₁, groupHomology.d₃₂_single_one_snd, groupHomology.instEpiModuleCatGShortComplexH0, CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj, ModuleCat.extendScalars_comp_id_assoc, ModuleCat.instPreservesFiniteLimitsLocalizationLocalizedModule_functor, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_apply, groupHomology.π_comp_H2Iso_hom_apply, SheafOfModules.relationsOfIsCokernelFree_s, ModuleCat.forget₂_reflectsLimits, FDRep.Iso.conj_ρ, FDRep.of_ρ, ModuleCat.forget₂PreservesColimitsOfShape, CondensedMod.instHasLimitsOfSizeModuleCat, MatrixModCat.toModuleCat_obj_isAddCommGroup, Rep.diagonalOneIsoLeftRegular_hom_hom, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, Rep.ihom_coev_app_hom, ModuleCat.biproductIsoPi_inv_comp_π_apply, groupHomology.mapCycles₁_hom, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, Rep.leftRegularHomEquiv_apply, Rep.leftRegular_projective, CondensedMod.LocallyConstant.instFaithfulModuleCatFunctor, ModuleCat.restrictScalars.smul_def', PresheafOfModules.pushforward_obj_map_apply', groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.chainsMap_zero, groupHomology.H1CoresCoinfOfTrivial_g_epi, Module.injective_object_of_injective_module, FDRep.char_dual, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, PresheafOfModules.Hom.naturality, groupHomology.mapShortComplexH2_id_comp, FGModuleCat.FGModuleCatEvaluation_apply', ModuleCat.forget₂AddCommGroup_reflectsLimit, groupHomology.isoShortComplexH2_inv, groupHomology.coe_mapCycles₁, groupHomology.toCycles_comp_isoCycles₁_hom, ModuleCat.HasLimit.productLimitCone_cone_pt_isAddCommGroup, ModuleCat.hom_inv_leftUnitor, SheafOfModules.forgetToSheafModuleCat_map_val, groupCohomology.d₀₁_comp_d₁₂_apply, Module.Flat.instPreservesFiniteLimitsModuleCatTensorLeftOfCarrier, ModuleCat.free_map_apply, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, Representation.linHom.mem_invariants_iff_comm, groupHomology.mapCycles₂_comp_i_apply, ModuleCat.binaryProductLimitCone_cone_pt, LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat, AlgebraicGeometry.tilde.functor_obj, groupCohomology.cocyclesIso₀_hom_comp_f_apply, ModuleCat.ofHom₂_hom_apply_hom, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, groupHomology.boundariesToCycles₂_apply, groupCohomology.subtype_comp_d₀₁, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier, groupHomology.cyclesOfIsCycle₂_coe, Rep.freeLift_hom, groupHomology.isoCycles₂_hom_comp_i, ModuleCat.instPreservesInjectiveObjectsUliftFunctorOfSmall, AlgebraicGeometry.tilde.toOpen_map_app_assoc, groupHomology.π_comp_H1Iso_hom, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply, groupHomology.isoCycles₂_inv_comp_iCycles, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, groupHomology.d₁₀_single_inv, groupHomology.mkH1OfIsTrivial_apply, groupCohomology.π_map_apply, Rep.indToCoindAux_snd_mul_inv, LightCondensed.instCountableAB4StarLightCondMod, ModuleCat.hom_sub, localCohomology.hasColimitDiagram, CoalgCat.ofComonObjCoalgebraStruct_counit, groupCohomology.cocyclesMap_id_comp, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, Rep.res_obj_ρ, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_aux, ModuleCat.instHasLimitsOfSize, ModuleCat.ofHom₂_compr₂, LightCondMod.LocallyConstant.instFullModuleCatLightCondensedDiscrete, ModuleCat.extendScalars_comp_id, PresheafOfModules.freeYonedaEquiv_comp, ModuleCat.forget₂AddCommGroup_preservesLimit, groupCohomology.coboundaries₁_le_cocycles₁, ModuleCat.hasKernels_moduleCat, groupHomology.shortComplexH0_g, Rep.ihom_obj_V_isModule, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff, ModuleCat.FreeMonoidal.εIso_hom_one, CategoryTheory.preadditiveCoyonedaObj_obj_carrier, groupCohomology.mapShortComplexH2_id, groupHomology.d₁₀ArrowIso_hom_right, groupCohomology.shortComplexH0_exact, Rep.freeLift_hom_single_single, Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, groupHomology.single_one_mem_boundaries₁, ModuleCat.mono_iff_ker_eq_bot, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, groupHomology.π_comp_H1Iso_inv_apply, groupHomology.cyclesIso₀_comp_H0π, FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG, groupCohomology.isoCocycles₂_hom_comp_i_apply, ModuleCat.extendRestrictScalarsAdj_unit_app_apply, ModuleCat.instMonoidalPreadditive, groupHomology.H1CoresCoinfOfTrivial_X₃, Rep.diagonalHomEquiv_apply, AlgebraicGeometry.tilde.map_comp, groupHomology.d₂₁_single, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply, SheafOfModules.Presentation.IsFinite.finite_relations, Rep.coinvariantsAdjunction_unit_app_hom, Rep.freeLiftLEquiv_symm_apply, groupHomology.inhomogeneousChains.d_eq, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, groupHomology.eq_d₂₁_comp_inv_apply, Rep.epi_iff_surjective, SheafOfModules.pushforwardNatTrans_app_val_app_apply, CategoryTheory.whiskering_linearYoneda₂, CategoryTheory.ShortComplex.moduleCatMk_X₂_carrier, groupCohomology.cochainsFunctor_map, groupCohomology.coboundaries₂_ext_iff, groupHomology.d₁₀_comp_coinvariantsMk_assoc, ModuleCat.MonoidalCategory.whiskerLeft_apply, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, PresheafOfModules.Finite.evaluation_preservesFiniteColimits, 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, groupCohomology.shortComplexH2_g, ModuleCat.forget_map, instIsGrothendieckAbelianModuleCat, Rep.coinvariantsShortComplex_X₂, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId, CategoryTheory.preadditiveCoyonedaObj_obj_isModule, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, groupHomology.H0π_comp_H0Iso_hom_assoc, groupCohomology.H1π_comp_map, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, groupHomology.cyclesMap_comp, LightCondensed.internallyProjective_iff_tensor_condition', ModuleCat.smulShortComplex_X₃_isModule, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, Rep.indResHomEquiv_apply_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, ModuleCat.homAddEquiv_apply, PresheafOfModules.ofPresheaf_map, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule, ModuleCat.hasLimit, CategoryTheory.preservesLimits_preadditiveCoyonedaObj, ModuleCat.instPreservesProjectiveObjectsUliftFunctorOfSmall, groupHomology.epi_map_0_of_epi, groupHomology.mapShortComplexH1_τ₃, ModuleCat.directLimitCocone_pt_isModule, ModuleCat.instLinearUliftFunctor, CommRingCat.KaehlerDifferential.ext_iff, AlgebraicGeometry.instIsIsoFunctorModuleCatCarrierUnitModulesSpecOfAdjunction, groupHomology.cyclesMap_comp_cyclesIso₀_hom_assoc, groupCohomology.cocyclesMk₀_eq, AlgebraicGeometry.tilde.map_neg, ModuleCat.endRingEquiv_apply, groupHomology.lsingle_comp_chainsMap_f_assoc, ModuleCat.directLimitDiagram_map, Rep.linearizationTrivialIso_hom_hom, ModuleCat.ofHom_id, LightCondensed.instIsGrothendieckAbelianLightCondMod, ModuleCat.HasColimit.reflectsColimit, PresheafOfModules.naturality_apply, groupHomology.single_mem_cycles₂_iff, Rep.instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype, groupCohomology.isoShortComplexH1_inv, ModuleCat.image.fac, CategoryTheory.additive_coyonedaObj, groupHomology.boundaries₁_le_cycles₁, LightCondMod.isDiscrete_iff_isDiscrete_forget, ModuleCat.mono_as_hom'_subtype, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, ModuleCat.FilteredColimits.ι_colimitDesc_assoc, ModuleCat.extendScalarsId_inv_app_apply, ModuleCat.semilinearMapAddEquiv_symm_apply_apply, ModuleCat.hasColimitsOfShape, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc, Rep.coinvariantsAdjunction_homEquiv_apply_hom, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, ModuleCat.hom_comp, ModuleCat.MonoidalCategory.braiding_inv_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, groupHomology.H1CoresCoinf_f, Rep.diagonalSuccIsoFree_hom_hom_single, AlgebraicGeometry.structurePresheafInModuleCat_obj_carrier, ModuleCat.hom_neg, Rep.ihom_obj_ρ, instInvertibleCarrierOutModuleCatValSkeleton, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, Rep.free_ext_iff, ModuleCat.MonoidalCategory.whiskerRight_def, AlgebraicGeometry.isIso_fromTildeΓ_iff, FGModuleCat.instFaithfulUlift, Rep.instPreservesLimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, groupCohomology.cochainsMap_id_comp_assoc, ModuleCat.preservesLimit_restrictScalars, groupCohomology.cocycles₁_ext_iff, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, groupCohomology.map_H0Iso_hom_f_assoc, ModuleCat.ofHom_apply, CategoryTheory.ShortComplex.Exact.moduleCat_of_range_eq_ker, TannakaDuality.FiniteGroup.ofRightFDRep_hom, CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj, ModuleCat.kernelIsoKer_inv_kernel_ι, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, AlgebraicGeometry.tilde.map_id_assoc, simple_iff_isSimpleModule', Rep.instIsLeftAdjointIndFunctor, groupHomology.shortComplexH1_g, Rep.instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, ModuleCat.restrictScalarsCongr_inv_app, groupCohomology.eq_d₁₂_comp_inv_assoc, Representation.linHom.invariantsEquivRepHom_apply_hom, groupHomology.cyclesMap_id, CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding, groupCohomology.H1InfRes_f, Rep.instAdditiveModuleCatInvariantsFunctor, ModuleCat.imageIsoRange_hom_subtype_apply, LinearMap.comp_id_moduleCat, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, FGModuleCat.Iso.conj_hom_eq_conj, ModuleCat.smulShortComplex_X₂, MatrixModCat.toModuleCat_obj_isModule, ModuleCat.epi_iff_range_eq_top, instFreeCarrierX₂ModuleCatProjectiveShortComplex, ModuleCat.forget₂AddCommGroupIsEquivalence, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, groupHomology.d₁₀ArrowIso_inv_left, ModuleCat.monoidalClosed_pre_app, SheafOfModules.forgetToSheafModuleCat_obj_val, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, Rep.coindFunctor'_map, groupHomology.single_mem_cycles₁_iff, Rep.coinvariantsFunctor_map_hom, Rep.coindFunctor_obj, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π, groupHomology.d₂₁_single_ρ_add_single_inv_mul, PresheafOfModules.evaluation_obj, groupCohomology.mapShortComplexH2_τ₃, LinearEquiv.toModuleIso_hom, ModuleCat.HasLimit.productLimitCone_isLimit_lift, ModuleCat.MonoidalCategory.tensorObj_carrier, Rep.linearization_map_hom_single, isZero_groupHomology_succ_of_subsingleton, groupCohomology.isoShortComplexH2_inv, ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear, CategoryTheory.preadditiveCoyoneda_obj, groupCohomology.map_id_comp_H0Iso_hom_assoc, groupCohomology.isoCocycles₂_hom_comp_i_assoc, Rep.ihom_obj_ρ_def, groupHomology.eq_d₁₀_comp_inv_apply, Rep.ihom_obj_V_carrier, LinearEquiv.toFGModuleCatIso_inv, ModuleCat.semilinearMapAddEquiv_apply, ModuleCat.CoextendScalars.map'_hom_apply_apply, Rep.coinvariantsShortComplex_X₃, Rep.coindIso_hom_hom_hom, TannakaDuality.FiniteGroup.equivHom_surjective, ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction_hom_apply_apply, ModuleCat.freeHomEquiv_symm_apply, ModuleCat.ulift_injective_of_injective, Rep.leftRegularTensorTrivialIsoFree_hom_hom, CategoryTheory.preadditiveCoyonedaObj_obj_isAddCommGroup, TannakaDuality.FiniteGroup.equivHom_injective, SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app, groupHomology.H0π_comp_H0Iso_hom_apply, Rep.barComplex.d_single, ModuleCat.freeDesc_apply, groupHomology.mapShortComplexH2_τ₃, FDRep.hom_action_ρ, Rep.mono_iff_injective, ModuleCat.MonoidalCategory.tensorUnit_isAddCommGroup, PresheafOfModules.evaluation_map, CategoryTheory.linearCoyoneda_obj_obj_isModule, FDRep.dualTensorIsoLinHom_hom_hom, ModuleCat.homEquiv_extendScalarsId, ModuleCat.ExtendScalars.hom_ext_iff, Rep.instMonoModuleCatHom, groupHomology.d₂₁_comp_d₁₀_assoc, groupCohomology.coe_mapCocycles₂, groupCohomology.eq_d₀₁_comp_inv_assoc, groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc, ModuleCat.toKernelSubobject_arrow, groupCohomology.functor_map, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_isAddCommGroup, CategoryTheory.Iso.toLinearMap_toLinearEquiv, ModuleCat.instHasBinaryBiproducts, Rep.linearization_ε_hom, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc, Condensed.instAB4CondensedMod, groupCohomology.H1π_eq_iff, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, ModuleCat.smulShortComplex_g_epi, Rep.Tor_obj, groupCohomology.isoCocycles₁_hom_comp_i_assoc, Rep.coinvariantsShortComplex_shortExact, groupHomology.π_comp_H1Iso_inv_assoc, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, Rep.FiniteCyclicGroup.resolution_π, Rep.instPreservesColimitsModuleCatForget₂HomSubtypeLinearMapIdCarrierV, groupHomology.mapCycles₁_quotientGroupMk'_epi, PresheafOfModules.zero_app, groupHomology.π_map, groupHomology.mapCycles₁_comp_i_assoc, groupHomology.H0π_comp_map_apply, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc, PresheafOfModules.map_comp_assoc, ModuleCat.restrictScalarsId'App_inv_apply, groupCohomology.mapShortComplexH1_τ₁, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, ModuleCat.smulShortComplex_exact, groupHomology.π_comp_H2Iso_inv_apply, FDRep.instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV, groupCohomology.coboundariesOfIsCoboundary₂_coe, Rep.FiniteCyclicGroup.resolution.π_f, CoalgCat.toComon_obj, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, Rep.instAdditiveModuleCatCoinvariantsFunctor, PresheafOfModules.forgetToPresheafModuleCat_map, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one, groupCohomology.cochainsFunctor_obj, ModuleCat.restrictScalarsComp'App_inv_apply, FDRep.endRingEquiv_comp_ρ, Rep.linearization_map_hom, CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier, groupHomology.mem_cycles₁_iff, ModuleCat.isZero_of_subsingleton, ModuleCat.isZero_of_iff_subsingleton, Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff, groupCohomology.mapCocycles₁_comp_i, groupHomology.boundariesToCycles₁_apply, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, SheafOfModules.Finite.evaluationPreservesFiniteLimits, CategoryTheory.IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj, ModuleCat.instHasCoequalizers, ModuleCat.exteriorPower.functor_obj, TannakaDuality.FiniteGroup.equivHom_apply, ModuleCat.ihom_ev_app, groupCohomology.cocycles₁.d₁₂_apply, FDRep.simple_iff_char_is_norm_one, Rep.indResHomEquiv_symm_apply_hom, groupHomology.isoCycles₂_hom_comp_i_assoc, ModuleCat.FilteredColimits.colimit_add_mk_eq, groupHomology.comp_d₃₂_eq, groupCohomology.π_comp_H2Iso_hom, ModuleCat.free_hom_ext_iff, groupHomology.chainsMap_f_0_comp_chainsIso₀, groupHomology.H2π_eq_zero_iff, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, CategoryTheory.ShortComplex.moduleCatMk_X₂_isAddCommGroup, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology, ModuleCat.enoughInjectives, FGModuleCat.instIsMonoidalModuleCatIsFG, ModuleCat.extendScalars_assoc, ModuleCat.MonoidalCategory.associator_inv_apply, ModuleCat.preservesColimit_restrictScalars, Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, ModuleCat.isSeparator, ModuleCat.instHasFiniteBiproducts, Rep.norm_comm, ModuleCat.exteriorPower.functor_map, instEnoughInjectivesModuleCatInt, Rep.linearization_μ_hom, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.H1π_eq_iff, ModuleCat.ExtendRestrictScalarsAdj.unit_app, ModuleCat.biprodIsoProd_inv_comp_fst_apply, groupHomology.d₃₂_comp_d₂₁_apply, FGModuleCat.instIsIsoCoimageImageComparison, ModuleCat.CoextendScalars.map_apply, groupCohomology.shortComplexH1_g, groupHomology.chainsMap_f, Rep.quotientToCoinvariantsFunctor_obj_V, SheafOfModules.unitHomEquiv_apply_coe, CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding, Profinite.NobelingProof.succ_mono, CategoryTheory.preadditiveYonedaObj_map, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, groupCohomology.map_comp_assoc, groupHomology.cyclesMap_comp_isoCycles₁_hom, groupCohomology.cochainsMap_id, ModuleCat.forget₂_map, AlgebraicGeometry.tilde.toOpen_map_app, groupCohomology.d₀₁_eq_zero, Rep.instInjective, ChainComplex.linearYonedaObj_X, ModuleCat.toMatrixModCat_obj_isModule

---

← Back to Index