Commit 2023-06-24 21:08 8bbc2aa8

View on Github →

feat: port RepresentationTheory.GroupCohomology.Resolution (#5391)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

added def GroupCohomology.Resolution.actionDiagonalSucc

added theorem GroupCohomology.Resolution.actionDiagonalSucc_hom_apply

added theorem GroupCohomology.Resolution.actionDiagonalSucc_inv_apply

added def GroupCohomology.Resolution.compForgetAugmentedIso

added def GroupCohomology.Resolution.d

added theorem GroupCohomology.Resolution.d_comp_ε

added theorem GroupCohomology.Resolution.d_eq

added theorem GroupCohomology.Resolution.d_of

added def GroupCohomology.Resolution.diagonalSucc

added theorem GroupCohomology.Resolution.diagonalSucc_hom_single

added theorem GroupCohomology.Resolution.diagonalSucc_inv_single_left

added theorem GroupCohomology.Resolution.diagonalSucc_inv_single_right

added theorem GroupCohomology.Resolution.diagonalSucc_inv_single_single

added def GroupCohomology.Resolution.forget₂ToModuleCat

added def GroupCohomology.Resolution.forget₂ToModuleCatHomotopyEquiv

added theorem GroupCohomology.Resolution.forget₂ToModuleCatHomotopyEquiv_f_0_eq

added def GroupCohomology.Resolution.ofMulActionBasis

added def GroupCohomology.Resolution.ofMulActionBasisAux

added theorem GroupCohomology.Resolution.ofMulAction_free

added theorem GroupCohomology.Resolution.quasiIsoOfForget₂εToSingle₀

added def GroupCohomology.Resolution.xIso

added theorem GroupCohomology.Resolution.x_projective

added def GroupCohomology.Resolution.ε

added def GroupCohomology.Resolution.εToSingle₀

added theorem GroupCohomology.Resolution.εToSingle₀_comp_eq

added def GroupCohomology.extIso

added def GroupCohomology.projectiveResolution

added def GroupCohomology.resolution

added theorem Rep.diagonalHomEquiv_apply

added theorem Rep.diagonalHomEquiv_symm_apply

added theorem Rep.diagonalHomEquiv_symm_partialProd_succ

added def classifyingSpaceUniversalCover.cechNerveTerminalFromIso

added def classifyingSpaceUniversalCover.cechNerveTerminalFromIsoCompForget

added def classifyingSpaceUniversalCover.compForgetAugmented.toModule

added def classifyingSpaceUniversalCover.compForgetAugmented

added def classifyingSpaceUniversalCover.extraDegeneracyAugmentedCechNerve

added def classifyingSpaceUniversalCover.extraDegeneracyCompForgetAugmented

added def classifyingSpaceUniversalCover.extraDegeneracyCompForgetAugmentedToModule

added def classifyingSpaceUniversalCover