chore(RepresentationTheory/Homological/ContCohomology): refactor functoriality

[rmhi]

Currently, functoriality of continuous cohomology is given by ContCohomology.map, which takes
a continuous group homomorphism \phi and an intertwining map f: res \phi X \to Y and returns a map from the
continuous cohomology of X to the continuous cohomology of Y.
The problem with this is that ContCohomology.map does not have a natural type such as Functor or NatTrans.

In this PR, we split ContCohomology.map as a composition of (continuousCohomologyFunctor _ _ _).map and a restriction map in continuous cohomology, which is defined as a natural transformation resNatTrans.

co-authored-by: Edison Xie @Whysoserioushah

---

[github-actions]

PR summary 699fc19bf8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ ResMap_eq
+ ResMap_id_left
+ ResMap_id_right
+ _root_.TopRep.resolutionXRes
+ _root_.continuousCohomologyFunctor
+ cochainsResMap
+ cochainsResMap_comp
+ cochainsResMap_eq
+ cochainsResMap_f_eq
+ cochainsResMap_id
+ cochainsResMap_id_left
+ cochainsResMap_id_right
+ cocyclesResMap
+ cocyclesResMap_comp
+ cocyclesResMap_id
+ coind₁Res_id
+ comp_id
+ continuousCohomologyFunctor_obj
+ homogeneousCochainsFunctor
+ homogeneousCochainsFunctor_obj
+ homogeneousCochainsResNatTrans
+ homogeneousCochainsResNatTrans_app_f
+ homogeneousCochainsXRes
+ homogeneousCochainsXRes_succ
+ homogeneousCochainsXRes_zero
+ id_comp
+ instance {H : Type*} [Monoid H] (φ : H →* G) : (resFunctor (k := k) φ).Additive
+ invariantsRes
+ invariantsResMap_eq
+ invariantsResMap_id
+ invariantsResNatTrans
+ ofHom_comp
+ resMap
+ resMap_comp
+ resMap_id
+ resNatTrans
+ resNatTrans_app
+ resolution'Functor
+ resolution'Res
+ resolution'ResNatTrans
+ resolutionResMap
+ resolutionResMap_comp
+ resolutionResMap_comp_d
+ resolutionResMap_eq
+ resolutionResMap_id
+ resolutionResMap_id_fst
+ resolutionResMap_id_snd
+ resolutionResMap_succ
+ resolutionResMap_zero
+ resolutionXRes_comp
+ resolutionXRes_comp_d
+ resolutionXRes_id
+ resolutionXRes_naturality
+ resolutionXRes_succ
+ resolutionXRes_zero
+ π_resMap
- cochainsMap
- cochainsMap_comp
- cochainsMap_id
- cocyclesMap
- cocyclesMap_comp
- cocyclesMap_id
- map
- map_comp
- map_id
- π_map

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 699fc19).

• +73 new declarations
• −16 removed declarations

+ContIntertwiningMap.comp_id
+ContIntertwiningMap.id_comp
+ContRepresentation.coind₁Res_id
+ContinuousCohomology.ResMap_eq
+ContinuousCohomology.ResMap_eq_assoc
+ContinuousCohomology.ResMap_id_left
+ContinuousCohomology.ResMap_id_right
-ContinuousCohomology.cochainsMap
-ContinuousCohomology.cochainsMap_comp
-ContinuousCohomology.cochainsMap_comp_assoc
-ContinuousCohomology.cochainsMap_f
-ContinuousCohomology.cochainsMap_f_hom
-ContinuousCohomology.cochainsMap_id
+ContinuousCohomology.cochainsResMap
+ContinuousCohomology.cochainsResMap_comp
+ContinuousCohomology.cochainsResMap_comp_assoc
+ContinuousCohomology.cochainsResMap_eq
+ContinuousCohomology.cochainsResMap_eq_assoc
+ContinuousCohomology.cochainsResMap_f
+ContinuousCohomology.cochainsResMap_f_eq
+ContinuousCohomology.cochainsResMap_f_eq_assoc
+ContinuousCohomology.cochainsResMap_f_hom
+ContinuousCohomology.cochainsResMap_id
+ContinuousCohomology.cochainsResMap_id_left
+ContinuousCohomology.cochainsResMap_id_right
-ContinuousCohomology.cocyclesMap
-ContinuousCohomology.cocyclesMap_comp
-ContinuousCohomology.cocyclesMap_comp_assoc
-ContinuousCohomology.cocyclesMap_id
+ContinuousCohomology.cocyclesResMap
+ContinuousCohomology.cocyclesResMap_comp
+ContinuousCohomology.cocyclesResMap_comp_assoc
+ContinuousCohomology.cocyclesResMap_id
+ContinuousCohomology.continuousCohomologyFunctor_obj
+ContinuousCohomology.homogeneousCochainsFunctor
+ContinuousCohomology.homogeneousCochainsFunctor_obj
+ContinuousCohomology.homogeneousCochainsResNatTrans
+ContinuousCohomology.homogeneousCochainsResNatTrans_app_f
+ContinuousCohomology.homogeneousCochainsXRes
+ContinuousCohomology.homogeneousCochainsXRes_succ
+ContinuousCohomology.homogeneousCochainsXRes_zero
-ContinuousCohomology.map
-ContinuousCohomology.map_comp
-ContinuousCohomology.map_comp_assoc
-ContinuousCohomology.map_id
+ContinuousCohomology.resMap
+ContinuousCohomology.resMap_comp
+ContinuousCohomology.resMap_comp_assoc
+ContinuousCohomology.resMap_id
+ContinuousCohomology.resNatTrans
+ContinuousCohomology.resNatTrans_app
+ContinuousCohomology.resolution'Functor
+ContinuousCohomology.resolution'Functor_map_f
+ContinuousCohomology.resolution'Functor_obj_X_V
+ContinuousCohomology.resolution'Functor_obj_X_hV3
+ContinuousCohomology.resolution'Functor_obj_X_ρ
+ContinuousCohomology.resolution'Functor_obj_d
+ContinuousCohomology.resolution'Res
+ContinuousCohomology.resolution'ResNatTrans
+ContinuousCohomology.resolutionResMap
+ContinuousCohomology.resolutionResMap_comp
+ContinuousCohomology.resolutionResMap_comp_d
+ContinuousCohomology.resolutionResMap_eq
+ContinuousCohomology.resolutionResMap_eq_assoc
+ContinuousCohomology.resolutionResMap_id
+ContinuousCohomology.resolutionResMap_id_fst
+ContinuousCohomology.resolutionResMap_id_snd
+ContinuousCohomology.resolutionResMap_succ
+ContinuousCohomology.resolutionResMap_zero
+ContinuousCohomology.resolutionXRes_comp
+ContinuousCohomology.resolutionXRes_comp_d
+ContinuousCohomology.resolutionXRes_id
+ContinuousCohomology.resolutionXRes_naturality
+ContinuousCohomology.resolutionXRes_succ
+ContinuousCohomology.resolutionXRes_zero
+ContinuousCohomology.termHₜ
+ContinuousCohomology.termHₜFunct
-ContinuousCohomology.π_map
-ContinuousCohomology.π_map_assoc
+ContinuousCohomology.π_resMap
+ContinuousCohomology.π_resMap_assoc
+TopRep.instAdditiveResFunctor
+TopRep.invariantsRes
+TopRep.invariantsResMap_eq
+TopRep.invariantsResMap_id
+TopRep.invariantsResNatTrans
+TopRep.ofHom_comp
+TopRep.resolutionXRes
+continuousCohomologyFunctor

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 699fc19bf8
Reference commit 2d00c9242a

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).