From 08913a1b099bf498cdb27bf5465b01785ec15871 Mon Sep 17 00:00:00 2001
From: Richard Hill <r.m.hill@ucl.ac.uk>
Date: Thu, 9 Jul 2026 13:50:55 +0100
Subject: [PATCH 01/10] initial commit

---
 .../Continuous/Basic.lean                     |  10 +
 .../Continuous/TopRep.lean                    |  38 +-
 .../ContCohomology/Functoriality.lean         | 380 +++++++++++++++---
 3 files changed, 373 insertions(+), 55 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Continuous/Basic.lean b/Mathlib/RepresentationTheory/Continuous/Basic.lean
index 81d7d2a93610de..a41ddc72bd12bc 100644
--- a/Mathlib/RepresentationTheory/Continuous/Basic.lean
+++ b/Mathlib/RepresentationTheory/Continuous/Basic.lean
@@ -156,6 +156,12 @@ lemma toContinuousLinearMap_comp {π₁ : ContRepresentation R G V} {π₂ : Con
     {π₃ : ContRepresentation R G U} (f : π₂ →ⁱL π₃) (g : π₁ →ⁱL π₂) :
     (f.comp g).toContinuousLinearMap = f.toContinuousLinearMap.comp g.toContinuousLinearMap := rfl
 
+@[simp]
+lemma comp_id (f : π₁ →ⁱL π₂) : f.comp .id = f := rfl
+
+@[simp]
+lemma id_comp (f : π₁ →ⁱL π₂) : ContIntertwiningMap.id.comp f = f := rfl
+
 instance : Add (π₁ →ⁱL π₂) where
   add f g := ⟨f.toContinuousLinearMap + g.toContinuousLinearMap, by simp [g.2, f.2]⟩
 
@@ -619,6 +625,10 @@ def coind₁Res (φ : H →ₜ* G) (π : ContRepresentation R G V) :
 lemma coind₁Res_apply (φ : H →ₜ* G) (π : ContRepresentation R G V) (F : C(G, V)) (x : H) :
     coind₁Res φ π F x = F (φ x) := rfl
 
+@[simp]
+lemma coind₁Res_id (π : ContRepresentation R G V) :
+    coind₁Res (ContinuousMonoidHom.id G) π = .id := rfl
+
 /-- Given a continuous group homomorphism `φ : H →ₜ* G`, a continuous intertwining map
 `f : π.restrict φ →ⁱL π'` induces a continuous intertwining map
 `π.coind₁.restrict φ →ⁱL π'.coind₁`, sending `F : C(G, V)` to `f ∘ F ∘ φ : C(H, W)`. -/
diff --git a/Mathlib/RepresentationTheory/Continuous/TopRep.lean b/Mathlib/RepresentationTheory/Continuous/TopRep.lean
index 54963a10aee64a..8f4ef363bc0caa 100644
--- a/Mathlib/RepresentationTheory/Continuous/TopRep.lean
+++ b/Mathlib/RepresentationTheory/Continuous/TopRep.lean
@@ -17,8 +17,9 @@ topological ring `k`, and shows that it is equivalent to the category `Action (T
 
 For a topological group `G` we define the invariants functor `TopRep.invariantsFunctor`, the
 coinduction functor `TopRep.coind₁Functor`, the restriction functor `TopRep.resFunctor` along a
-group homomorphism `φ : H →* G`, and the morphism `TopRep.invariantsResMap φ f` between invariant
-submodules induced by a morphism `f : res φ X ⟶ Y`.
+group homomorphism `φ : H →* G`, the morphism `TopRep.invariantsResMap φ f` between invariant
+submodules induced by a morphism `f : res φ X ⟶ Y`, and the natural transformation
+`TopRep.invariantsResNatTrans φ` given by the restriction maps `TopRep.invariantsRes φ`.
 -/
 
 @[expose] public section
@@ -106,6 +107,12 @@ abbrev ofHom (f : ρ →ⁱL σ) : of ρ ⟶ of σ :=
 
 @[simp] lemma ofHom_hom (f : A ⟶ B) : ofHom f.hom = f := rfl
 
+@[simp]
+lemma ofHom_comp {Z : Type w} [AddCommGroup Z] [Module k Z] [TopologicalSpace Z]
+    [IsTopologicalAddGroup Z] [ContinuousSMul k Z] {τ : ContRepresentation k G Z}
+    (f : ρ →ⁱL σ) (g : σ →ⁱL τ) :
+    ofHom (g.comp f) = ofHom f ≫ ofHom g := rfl
+
 variable {A B} in
 /-- The morphism of topological modules underlying a morphism in `TopRep k G`. -/
 abbrev Hom.toTopModuleCatHom (f : Hom A B) :
@@ -271,6 +278,8 @@ abbrev resFunctor {H : Type*} [Monoid H] (φ : H →* G) :
   obj := res φ
   map f := ofHom <| f.hom.restrict φ
 
+instance {H : Type*} [Monoid H] (φ : H →* G) : (resFunctor (k := k) φ).Additive where
+
 section invariantsResMap
 
 variable {G H : Type*} [Group G]
@@ -296,6 +305,31 @@ lemma invariantsResMap_map_comp {X X' : TopRep k G} {Y : TopRep k H} (φ : H →
     invariantsResMap φ ((resFunctor φ).map f ≫ g) =
       (invariantsFunctor k G).map f ≫ invariantsResMap φ g := rfl
 
+/-- The restriction map `X.invariants ⟶ (X.res φ).invariants` between invariant submodules
+along a group homomorphism `φ : H →* G`. -/
+def invariantsRes (φ : H →* G) (X : TopRep k G) :
+    X.invariants ⟶ (X.res φ).invariants :=
+  TopModuleCat.ofHom (ContIntertwiningMap.mapInvariantsOfRes φ ContIntertwiningMap.id)
+
+/-- The restriction maps `TopRep.invariantsRes φ` as a natural transformation
+`invariantsFunctor k G ⟶ resFunctor φ ⋙ invariantsFunctor k H`. -/
+abbrev invariantsResNatTrans (φ : H →* G) :
+    invariantsFunctor k G ⟶ resFunctor φ ⋙ invariantsFunctor k H where
+  app := invariantsRes φ
+  naturality X Y f := (eq_of_comp_right_eq'
+    (invariantsRes φ X ≫ (resFunctor φ ⋙ invariantsFunctor k H).map f)
+    ((invariantsFunctor k G).map f ≫ invariantsRes φ Y) rfl).symm
+
+/-- `invariantsResMap φ f` is the restriction map `invariantsRes φ` followed by the functorial
+map on invariants. -/
+lemma invariantsResMap_eq (φ : H →* G) {X : TopRep k G} {Y : TopRep k H} (f : res φ X ⟶ Y) :
+    invariantsResMap φ f = X.invariantsRes φ ≫ (invariantsFunctor k H).map f := rfl
+
+/-- `invariantsRes` is the special case of `invariantsResMap` where the coefficient map is the
+identity. -/
+lemma invariantsResMap_id (φ : H →* G) {X : TopRep k G} :
+    invariantsResMap φ (𝟙 (res φ X)) = X.invariantsRes φ := rfl
+
 end invariantsResMap
 
 end TopRep
diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
index 8e7e4e8a453839..3254b98e69f02f 100644
--- a/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
@@ -18,18 +18,18 @@ representation `X` of `G`, a topological representation `Y` of `H`, and a morphi
 
 ## Main definitions
 
-* `ContinuousCohomology.cochainsMap φ f` : the cochain map
+* `ContinuousCohomology.cochainsMap₂ φ f` : the cochain map
   `homogeneousCochains X ⟶ homogeneousCochains Y` induced by `φ : H →ₜ* G` and
   `f : res φ X ⟶ Y`, sending an invariant function `σ : C(G, C(G, ⋯))` to `f ∘ σ ∘ φ`.
-* `ContinuousCohomology.map φ f n` : the induced map `Hⁿ(G, X) ⟶ Hⁿ(H, Y)` on continuous
+* `ContinuousCohomology.map₂ φ f n` : the induced map `Hⁿ(G, X) ⟶ Hⁿ(H, Y)` on continuous
   cohomology.
 -/
 
 @[expose] public section
 
-universe u v
+universe u v w
 
-open CategoryTheory
+open CategoryTheory CategoryTheory.Functor
 
 namespace ContinuousCohomology
 
@@ -39,7 +39,184 @@ variable {k : Type u} {G H K : Type v} [Ring k] [TopologicalSpace k]
   [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
   [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
   [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
-  {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K}
+  {X X' X'' : TopRep k G} {Y : TopRep k H} {Z : TopRep k K}
+
+abbrev resolutionMap (f : X ⟶ X') :
+    (i : ℕ) → (resolutionX X i) ⟶ (resolutionX X' i)
+  | 0 => f
+  | i + 1 => ((coind₁Functor k G).map (resolutionMap f i))
+
+@[simp]
+lemma resolutionMap_zero (f : X ⟶ X') : resolutionMap f 0 = f := rfl
+
+lemma resolutionMap_succ (f : X ⟶ X') (n : ℕ) :
+    resolutionMap f (n + 1) = (coind₁Functor k G).map (resolutionMap f n) := rfl
+
+/-- The maps `resolutionMap f` commute with the differentials of the resolutions. -/
+lemma resolutionMap_comp_d (f : X ⟶ X') (i : ℕ) :
+    resolutionMap f i ≫ d X' i = (d X i) ≫ resolutionMap f (i + 1) := by
+  induction i with
+  | zero => rfl
+  | succ i ih =>
+    rw [d_succ, d_succ, resolutionMap_succ f (i + 1), Preadditive.comp_sub,
+      Preadditive.sub_comp]
+    congr 1
+    rw [resolutionMap_succ f i, ← Functor.map_comp, ← Functor.map_comp, ih]
+
+lemma resolutionMap_id (i : ℕ) : resolutionMap (𝟙 X) i = 𝟙 (resolutionX X i) := by
+  induction i with
+  | zero => rw [resolutionMap_zero]
+  | succ _ ih => rw [resolutionMap_succ, ih, map_id]
+
+lemma resolutionMap_comp (f : X ⟶ X') (f' : X' ⟶ X'') (i : ℕ) :
+    resolutionMap (f ≫ f') i = (resolutionMap f i) ≫ resolutionMap f' i := by
+  induction i with
+  | zero => rfl
+  | succ i ih => rw [resolutionMap_succ, resolutionMap_succ, resolutionMap_succ, ih,
+      map_comp]
+
+variable (k G)
+@[simps] abbrev resolution'Functor : TopRep k G ⥤ CochainComplex (TopRep k G) ℕ where
+  obj           := resolution'
+  map {X Y} f   := {
+    f n   := resolutionMap f (n + 1)
+    comm' := by simp +contextual [resolution'd_eq, resolutionMap_comp_d f _]
+  }
+  map_id _      := HomologicalComplex.hom_ext _ _ <| fun _ ↦ resolutionMap_id _
+  map_comp _ _  := HomologicalComplex.hom_ext _ _ <| fun _ ↦ resolutionMap_comp _ _ _
+
+abbrev homogeneousCochainsFunctor : TopRep k G ⥤ CochainComplex (TopModuleCat k) ℕ :=
+    resolution'Functor k G ⋙ (invariantsFunctor k G).mapHomologicalComplex (.up ℕ)
+
+lemma homogeneousCochainsFunctor_obj :
+    (homogeneousCochainsFunctor k G).obj = homogeneousCochains := rfl
+
+noncomputable abbrev Functor (n : ℕ) : TopRep k G ⥤ TopModuleCat k :=
+    homogeneousCochainsFunctor k G ⋙ HomologicalComplex.homologyFunctor _ _ n
+
+notation "Hₜ" => continuousCohomology
+
+lemma Functor_obj (n : ℕ) : (Functor k G n).obj = Hₜ n := rfl
+
+variable {k G}
+variable (X) in
+/-- The morphisms between the levels of the standard resolutions of `X` and `Y` induced by a
+continuous group homomorphism `φ : H →ₜ* G` and a morphism `f : res φ X ⟶ Y`, given by
+`F ↦ f ∘ F ∘ φ`. -/
+abbrev _root_.TopRep.resolutionXRes (φ : H →ₜ* G) :
+    (i : ℕ) → (res φ (resolutionX X i)) ⟶ (resolutionX (res φ.toMonoidHom X) i)
+  | 0 => 𝟙 _
+  | i + 1 => ofHom (coind₁ResMap φ (resolutionXRes φ i).hom)
+
+@[simp]
+lemma resolutionXRes_zero (φ : H →ₜ* G) : X.resolutionXRes φ 0 = 𝟙 _ := rfl
+
+lemma resolutionXRes_one (φ : H →ₜ* G) : X.resolutionXRes φ 1 = ofHom (coind₁ResMap φ .id) := rfl
+
+lemma resolutionXRes_succ (φ : H →ₜ* G) (i : ℕ) :
+    resolutionXRes X φ (i + 1) = ofHom (coind₁ResMap φ (resolutionXRes _ φ i).hom) := rfl
+
+@[simp]
+lemma resolutionXRes_id (X : TopRep k G) (i : ℕ) :
+    resolutionXRes X (ContinuousMonoidHom.id G) i = 𝟙 (resolutionX X i) := by
+  induction i with
+  | zero => rfl
+  | succ i ih =>
+    rw [resolutionXRes_succ, ih]
+    ext; rfl
+
+
+lemma resolutionXRes_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (i : ℕ) :
+    resolutionXRes X (φ.comp ψ) i =
+      (resFunctor ψ.toMonoidHom).map (resolutionXRes X φ i) ≫ resolutionXRes _ ψ i := by
+  induction i with
+  | zero => rfl
+  | succ i ih =>
+    rw [resolutionXRes_succ, resolutionXRes_succ, resolutionXRes_succ, ih]
+    ext; rfl
+
+/-- The maps `resolutionMap₂ φ f` commute with the differentials of the resolutions. -/
+lemma resolutionXRes_comp_d (φ : H →ₜ* G) (i : ℕ) :
+    resolutionXRes X φ i ≫ d _ i =
+      (resFunctor (φ : H →* G)).map (d X i) ≫ resolutionXRes X φ (i + 1) := by
+  induction i with
+  | zero => rfl
+  | succ i ih =>
+    ext : 1
+    replace ih := congr($(ih).hom)
+    simp only [TopRep.hom_comp, TopRep.hom_ofHom, hom_d_succ,
+      ContIntertwiningMap.restrict_sub, ContIntertwiningMap.sub_comp,
+      ContIntertwiningMap.comp_sub, coind₁Map_comp_coind₁ResMap,
+      coind₁ResMap_comp_coind₁Map_restrict] at ih ⊢
+    rw [ih, ← coind₁ResMap_comp_coind₁ι_restrict]
+
+/-- The maps `resolutionXRes X φ` are natural in `X`. -/
+lemma resolutionXRes_naturality (φ : H →ₜ* G) (f : X ⟶ X') (i : ℕ) :
+    (resFunctor (φ : H →* G)).map (resolutionMap f i) ≫ resolutionXRes X' φ i =
+      resolutionXRes X φ i ≫ resolutionMap ((resFunctor φ.toMonoidHom).map f) i := by
+  induction i with
+  | zero => rfl
+  | succ i ih =>
+    rw [resolutionXRes_succ, resolutionXRes_succ, resolutionMap_succ, resolutionMap_succ]
+    ext F x
+    exact congr($(ih).hom (F (φ x)))
+
+abbrev resolution'Res (φ : H →ₜ* G) :
+    ((resFunctor φ.toMonoidHom).mapHomologicalComplex (.up ℕ)).obj (resolution' X)
+    ⟶ resolution' (res φ.toMonoidHom X) where
+  f n := resolutionXRes X φ (n + 1)
+  comm' := by
+    intro _ _ rfl
+    simp only [mapHomologicalComplex_obj_d, ContinuousMonoidHom.coe_toMonoidHom,
+      CochainComplex.of_d, resolution'd_eq]
+    exact resolutionXRes_comp_d φ _
+
+def resolution'ResNatTrans (φ : H →ₜ* G) :
+    resolution'Functor k G ⋙ (resFunctor ↑φ).mapHomologicalComplex (.up ℕ)
+    ⟶ (resFunctor φ) ⋙ resolution'Functor k H where
+  app X := resolution'Res φ
+  naturality X Y f := by
+    ext n : 1
+    exact resolutionXRes_naturality φ f (n + 1)
+
+def _root_.TopRep.homogeneousCochainsXRes (φ : H →ₜ* G) (X : TopRep k G) (n : ℕ) :
+    X.homogeneousCochains.X n ⟶ (X.res φ.toMonoidHom).homogeneousCochains.X n :=
+  (X.resolutionX _).invariantsRes φ.toMonoidHom ≫ ((invariantsFunctor (k := k) (G := H)).map
+  (resolutionXRes X φ _))
+
+lemma _root_.TopRep.homogeneousCochainsXRes_zero (φ : H →ₜ* G) (X : TopRep k G) :
+    X.homogeneousCochainsXRes φ 0 =
+    X.coind₁.invariantsRes φ ≫ (invariantsFunctor k H).map (ofHom (coind₁ResMap φ .id)) := rfl
+
+lemma _root_.TopRep.homogeneousCochainsXRes_succ (φ : H →ₜ* G) (X : TopRep k G) (n : ℕ) :
+    X.homogeneousCochainsXRes φ (n + 1) =
+    (X.resolution'X n).coind₁.invariantsRes φ ≫ (invariantsFunctor k H).map
+    (ofHom (coind₁ResMap φ (X.resolutionXRes φ (n + 1)).hom)) := rfl
+
+variable (k) in
+def homogeneousCochainsResNatTrans (φ : H →ₜ* G) : homogeneousCochainsFunctor k G
+    ⟶ (resFunctor φ.toMonoidHom) ⋙ homogeneousCochainsFunctor k H :=
+  (𝟙 (resolution'Functor k G)
+    ◫ ((invariantsResNatTrans φ.toMonoidHom (k := k)).mapHomologicalComplex _
+    ≫ (mapHomologicalComplexCompIso (.refl _) _).inv))
+  ≫ (associator _ _ _).inv
+  ≫ (resolution'ResNatTrans φ ◫ (𝟙 _))
+  ≫ (associator _ _ _).hom
+
+lemma homogeneousCochainsResNatTrans_app_f (φ : H →ₜ* G) (X : TopRep k G) (n : ℕ) :
+    ((homogeneousCochainsResNatTrans k φ).app X).f n = homogeneousCochainsXRes φ X n := rfl
+
+variable (k) in
+noncomputable abbrev resNatTrans (φ : H →ₜ* G) (n : ℕ) :
+    (Functor k G n) ⟶ (resFunctor φ.toMonoidHom ⋙ Functor k H n) :=
+  homogeneousCochainsResNatTrans k φ ◫ 𝟙 _
+
+lemma resNatTrans_app (φ : H →ₜ* G) (n : ℕ) (X : TopRep k G) :
+    (resNatTrans k φ n).app X =
+      HomologicalComplex.homologyMap ((homogeneousCochainsResNatTrans k φ).app X) n := by
+  simp only [resNatTrans, NatTrans.hcomp_id_app, HomologicalComplex.homologyFunctor_map]
+
+
 
 set_option allowUnsafeReducibility true in
 attribute [local reducible] CategoryTheory.Functor.mapHomologicalComplex
@@ -47,49 +224,50 @@ attribute [local reducible] CategoryTheory.Functor.mapHomologicalComplex
 /-- The morphisms between the levels of the standard resolutions of `X` and `Y` induced by a
 continuous group homomorphism `φ : H →ₜ* G` and a morphism `f : res φ X ⟶ Y`, given by
 `F ↦ f ∘ F ∘ φ`. -/
-def resolutionMap (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
+def resolutionMap₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
     (i : ℕ) → res φ (resolutionX X i) ⟶ resolutionX Y i
   | 0 => f
-  | i + 1 => ofHom (coind₁ResMap φ (resolutionMap φ f i).hom)
+  | i + 1 => ofHom (coind₁ResMap φ (resolutionMap₂ φ f i).hom)
 
 @[simp]
-lemma resolutionMap_zero (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
-    resolutionMap φ f 0 = f := rfl
+lemma resolutionMap₂_zero (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
+    resolutionMap₂ φ f 0 = f := rfl
 
-lemma resolutionMap_succ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
-    resolutionMap φ f (i + 1) = ofHom (coind₁ResMap φ (resolutionMap φ f i).hom) := rfl
+lemma resolutionMap₂_succ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
+    resolutionMap₂ φ f (i + 1) = ofHom (coind₁ResMap φ (resolutionMap₂ φ f i).hom) := rfl
 
 @[simp]
-lemma resolutionMap_id (X : TopRep k G) (i : ℕ) :
-    resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (resolutionX X i) := by
+lemma resolutionMap₂_id (X : TopRep k G) (i : ℕ) :
+    resolutionMap₂ (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (resolutionX X i) := by
   induction i with
   | zero => rfl
   | succ i ih =>
-    rw [resolutionMap_succ, ih]
+    rw [resolutionMap₂_succ, ih]
     ext F x
     rfl
 
-lemma resolutionMap_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z)
+lemma resolutionMap₂_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z)
     (i : ℕ) :
-    resolutionMap (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) i =
-      (resFunctor (ψ : K →* H)).map (resolutionMap φ f i) ≫ resolutionMap ψ g i := by
+    resolutionMap₂ (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) i =
+      (resFunctor (ψ : K →* H)).map (resolutionMap₂ φ f i) ≫ resolutionMap₂ ψ g i := by
   induction i with
   | zero => rfl
   | succ i ih =>
-    rw [resolutionMap_succ, resolutionMap_succ, resolutionMap_succ, ih]
+    rw [resolutionMap₂_succ, resolutionMap₂_succ, resolutionMap₂_succ, ih]
     ext F x
     rfl
 
-/-- The maps `resolutionMap φ f` commute with the differentials of the resolutions. -/
-lemma resolutionMap_comp_d (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
-    resolutionMap φ f i ≫ d Y i =
-      (resFunctor (φ : H →* G)).map (d X i) ≫ resolutionMap φ f (i + 1) := by
+
+/-- The maps `resolutionMap₂ φ f` commute with the differentials of the resolutions. -/
+lemma resolutionMap₂_comp_d (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
+    resolutionMap₂ φ f i ≫ d Y i =
+      (resFunctor (φ : H →* G)).map (d X i) ≫ resolutionMap₂ φ f (i + 1) := by
   induction i with
   | zero => rfl
   | succ i ih =>
     ext : 1
     replace ih := congr($(ih).hom)
-    simp only [TopRep.hom_comp, resolutionMap_succ, TopRep.hom_ofHom, hom_d_succ,
+    simp only [TopRep.hom_comp, resolutionMap₂_succ, TopRep.hom_ofHom, hom_d_succ,
       ContIntertwiningMap.restrict_sub, ContIntertwiningMap.sub_comp,
       ContIntertwiningMap.comp_sub, coind₁Map_comp_coind₁ResMap,
       coind₁ResMap_comp_coind₁Map_restrict] at ih ⊢
@@ -99,67 +277,163 @@ lemma resolutionMap_comp_d (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
 group homomorphism `φ : H →ₜ* G` and a morphism of topological `H`-representations
 `f : res φ X ⟶ Y`, sending an invariant function `σ : C(G, C(G, ⋯))` to `f ∘ σ ∘ φ`. -/
 @[simps! -isSimp f f_hom]
-def cochainsMap (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
+def cochainsMap₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
     homogeneousCochains X ⟶ homogeneousCochains Y where
-  f i := invariantsResMap φ (resolutionMap φ f (i + 1))
+  f i := invariantsResMap φ (resolutionMap₂ φ f (i + 1))
   comm' i j (hij : _ = _) := by
     subst hij
     rw [homogeneousCochains.d_eq, homogeneousCochains.d_eq, ← invariantsResMap_comp,
-      resolutionMap_comp_d, invariantsResMap_map_comp]
+      resolutionMap₂_comp_d, invariantsResMap_map_comp]
 
 @[simp]
-lemma cochainsMap_id (X : TopRep k G) :
-    cochainsMap (ContinuousMonoidHom.id G) (𝟙 X) = 𝟙 (homogeneousCochains X) := by
+lemma cochainsMap₂_id (X : TopRep k G) :
+    cochainsMap₂ (ContinuousMonoidHom.id G) (𝟙 X) = 𝟙 (homogeneousCochains X) := by
   ext i : 1
-  rw [cochainsMap_f, resolutionMap_id]
+  rw [cochainsMap₂_f, resolutionMap₂_id]
   ext v
   rfl
 
 @[reassoc]
-lemma cochainsMap_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z) :
-    cochainsMap (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) =
-      cochainsMap φ f ≫ cochainsMap ψ g := by
+lemma cochainsMap₂_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z) :
+    cochainsMap₂ (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) =
+      cochainsMap₂ φ f ≫ cochainsMap₂ ψ g := by
   ext i v x
-  exact congr($(resolutionMap_comp φ ψ f g (i + 1)).hom v.1 x)
+  exact congr($(resolutionMap₂_comp φ ψ f g (i + 1)).hom v.1 x)
 
 /-- The map `Zⁿ(G, X) ⟶ Zⁿ(H, Y)` on cocycles induced by a continuous group homomorphism
 `φ : H →ₜ* G` and a morphism of topological `H`-representations `f : res φ X ⟶ Y`. -/
-noncomputable abbrev cocyclesMap (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+noncomputable abbrev cocyclesMap₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
     cocycles X n ⟶ cocycles Y n :=
-  HomologicalComplex.cyclesMap (cochainsMap φ f) n
+  HomologicalComplex.cyclesMap (cochainsMap₂ φ f) n
 
 @[simp]
-lemma cocyclesMap_id (X : TopRep k G) (n : ℕ) :
-    cocyclesMap (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 _ := by
-  simp [cocyclesMap]
+lemma cocyclesMap₂_id (X : TopRep k G) (n : ℕ) :
+    cocyclesMap₂ (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 _ := by
+  simp [cocyclesMap₂]
 
 @[reassoc]
-lemma cocyclesMap_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z)
+lemma cocyclesMap₂_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z)
     (n : ℕ) :
-    cocyclesMap (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) n =
-      cocyclesMap φ f n ≫ cocyclesMap ψ g n := by
-  simp [cocyclesMap, ← HomologicalComplex.cyclesMap_comp, ← cochainsMap_comp]
+    cocyclesMap₂ (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) n =
+      cocyclesMap₂ φ f n ≫ cocyclesMap₂ ψ g n := by
+  simp [cocyclesMap₂, ← HomologicalComplex.cyclesMap_comp, ← cochainsMap₂_comp]
 
 /-- The map `Hⁿ(G, X) ⟶ Hⁿ(H, Y)` on continuous cohomology induced by a continuous group
 homomorphism `φ : H →ₜ* G` and a morphism of topological `H`-representations
 `f : res φ X ⟶ Y`. -/
-noncomputable abbrev map (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+noncomputable abbrev map₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
     continuousCohomology n X ⟶ continuousCohomology n Y :=
-  HomologicalComplex.homologyMap (cochainsMap φ f) n
+  HomologicalComplex.homologyMap (cochainsMap₂ φ f) n
 
 @[reassoc]
-theorem π_map (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
-    π X n ≫ map φ f n = cocyclesMap φ f n ≫ π Y n := by
-  simp [map, cocyclesMap]
+theorem π_map₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+    π X n ≫ map₂ φ f n = cocyclesMap₂ φ f n ≫ π Y n := by
+  simp [map₂, cocyclesMap₂]
 
 @[simp]
-lemma map_id (X : TopRep k G) (n : ℕ) :
-    map (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 _ := by
-  simp [map]
+lemma map₂_id (X : TopRep k G) (n : ℕ) :
+    map₂ (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 _ := by
+  simp [map₂]
+
+@[reassoc]
+lemma map₂_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z) (n : ℕ) :
+    map₂ (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) n =
+      map₂ φ f n ≫ map₂ ψ g n := by
+  simp [map₂, ← HomologicalComplex.homologyMap_comp, ← cochainsMap₂_comp]
+
+/-!
+### Relation to the functorial constructions
+
+The maps `resolutionMap₂`, `cochainsMap₂` and `map₂` combine restriction along `φ : H →ₜ* G` with
+functoriality in the coefficient representation. The following lemmas express them in terms of
+the two constructions they combine: `resolutionXRes`, `homogeneousCochainsResNatTrans` and
+`resNatTrans` (pure restriction), and `resolutionMap` and the functors
+`homogeneousCochainsFunctor` and `Functor` (pure coefficient maps).
+-/
+
+/-- `resolutionMap₂ φ f` is the restriction map `resolutionXRes X φ` followed by the functorial
+map `resolutionMap f`. -/
+@[reassoc]
+lemma resolutionMap₂_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
+    resolutionMap₂ φ f i = resolutionXRes X φ i ≫ resolutionMap f i := by
+  induction i with
+  | zero => rfl
+  | succ i ih =>
+    rw [resolutionMap₂_succ, resolutionXRes_succ, resolutionMap_succ, ih]
+    ext F x
+    rfl
 
+/-- `resolutionXRes` is the special case of `resolutionMap₂` where the coefficient map is the
+identity. -/
+lemma resolutionMap₂_id_right (φ : H →ₜ* G) (i : ℕ) :
+    resolutionMap₂ φ (𝟙 (res φ.toMonoidHom X)) i = resolutionXRes X φ i := by
+  induction i with
+  | zero => rfl
+  | succ i ih => rw [resolutionMap₂_succ, resolutionXRes_succ, ih]
+
+/-- `resolutionMap` is the special case of `resolutionMap₂` along the identity of `G`. -/
+lemma resolutionMap₂_id_left (f : X ⟶ X') (i : ℕ) :
+    resolutionMap₂ (ContinuousMonoidHom.id G) f i = resolutionMap f i := by
+  induction i with
+  | zero => rfl
+  | succ i ih =>
+    rw [resolutionMap₂_succ, resolutionMap_succ, ih]
+    ext F x
+    rfl
+
+/-- `cochainsMap₂ φ f` is the component of the restriction natural transformation on homogeneous
+cochains followed by the functorial map on homogeneous cochains. -/
 @[reassoc]
-lemma map_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z) (n : ℕ) :
-    map (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) n = map φ f n ≫ map ψ g n := by
-  simp [map, ← HomologicalComplex.homologyMap_comp, ← cochainsMap_comp]
+lemma cochainsMap₂_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
+    cochainsMap₂ φ f = (homogeneousCochainsResNatTrans k φ).app X ≫
+      (homogeneousCochainsFunctor k H).map f := by
+  ext i v x
+  exact congr($(resolutionMap₂_eq φ f (i + 1)).hom v.1 x)
+
+/-- The levelwise form of `cochainsMap₂_eq`: the restriction part expressed via
+`homogeneousCochainsXRes` and the coefficient part via `resolutionMap`. -/
+@[reassoc]
+lemma cochainsMap₂_f_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+    (cochainsMap₂ φ f).f n = homogeneousCochainsXRes φ X n ≫
+      (invariantsFunctor k H).map (resolutionMap f (n + 1)) := by
+  rw [cochainsMap₂_eq]
+  rfl
+
+/-- The component of the restriction natural transformation on homogeneous cochains is the
+special case of `cochainsMap₂` where the coefficient map is the identity. -/
+lemma cochainsMap₂_id_right (φ : H →ₜ* G) :
+    cochainsMap₂ φ (𝟙 (res φ.toMonoidHom X)) = (homogeneousCochainsResNatTrans k φ).app X := by
+  ext i v x
+  exact congr($(resolutionMap₂_id_right φ (i + 1)).hom v.1 x)
+
+/-- The functorial map on homogeneous cochains is the special case of `cochainsMap₂` along the
+identity of `G`. -/
+lemma cochainsMap₂_id_left (f : X ⟶ X') :
+    cochainsMap₂ (ContinuousMonoidHom.id G) f = (homogeneousCochainsFunctor k G).map f := by
+  ext i v x
+  exact congr($(resolutionMap₂_id_left f (i + 1)).hom v.1 x)
+
+/-- `map₂ φ f n` is the component of the restriction natural transformation `resNatTrans`
+followed by the functorial map on continuous cohomology. -/
+@[reassoc]
+lemma map₂_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+    map₂ φ f n = (resNatTrans k φ n).app X ≫ (Functor k H n).map f := by
+  rw [resNatTrans_app]
+  exact (congrArg (HomologicalComplex.homologyMap · n) (cochainsMap₂_eq φ f)).trans
+    (HomologicalComplex.homologyMap_comp _ _ _)
+
+/-- The component of `resNatTrans` is the special case of `map₂` where the coefficient map is
+the identity. -/
+lemma map₂_id_right (φ : H →ₜ* G) (n : ℕ) :
+    map₂ φ (𝟙 (res φ.toMonoidHom X)) n = (resNatTrans k φ n).app X := by
+  rw [resNatTrans_app]
+  exact congrArg (HomologicalComplex.homologyMap · n) (cochainsMap₂_id_right φ)
+
+/-- The functorial map on continuous cohomology is the special case of `map₂` along the
+identity of `G`. -/
+lemma map₂_id_left (f : X ⟶ X') (n : ℕ) :
+    map₂ (ContinuousMonoidHom.id G) f n = (Functor k G n).map f := by
+  simp only [map₂, cochainsMap₂_id_left]
+  rfl
 
 end ContinuousCohomology

From dd345352faff13d9454781a3db59207938083bda Mon Sep 17 00:00:00 2001
From: Richard Hill <r.m.hill@ucl.ac.uk>
Date: Thu, 9 Jul 2026 14:10:10 +0100
Subject: [PATCH 02/10] notation for Functor

---
 .../Homological/ContCohomology/Functoriality.lean     | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
index 3254b98e69f02f..fc05933d110a97 100644
--- a/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
@@ -91,12 +91,13 @@ abbrev homogeneousCochainsFunctor : TopRep k G ⥤ CochainComplex (TopModuleCat
 lemma homogeneousCochainsFunctor_obj :
     (homogeneousCochainsFunctor k G).obj = homogeneousCochains := rfl
 
-noncomputable abbrev Functor (n : ℕ) : TopRep k G ⥤ TopModuleCat k :=
+noncomputable abbrev _root_.continuousCohomologyFunctor (n : ℕ) : TopRep k G ⥤ TopModuleCat k :=
     homogeneousCochainsFunctor k G ⋙ HomologicalComplex.homologyFunctor _ _ n
 
 notation "Hₜ" => continuousCohomology
+notation "Hₜ(" k "," G "," n ")" => continuousCohomologyFunctor k G n
 
-lemma Functor_obj (n : ℕ) : (Functor k G n).obj = Hₜ n := rfl
+lemma Functor_obj (n : ℕ) : Hₜ(k,G,n).obj = Hₜ n := rfl
 
 variable {k G}
 variable (X) in
@@ -208,7 +209,7 @@ lemma homogeneousCochainsResNatTrans_app_f (φ : H →ₜ* G) (X : TopRep k G) (
 
 variable (k) in
 noncomputable abbrev resNatTrans (φ : H →ₜ* G) (n : ℕ) :
-    (Functor k G n) ⟶ (resFunctor φ.toMonoidHom ⋙ Functor k H n) :=
+    Hₜ(k,G,n) ⟶ resFunctor φ.toMonoidHom ⋙ Hₜ(k,H,n) :=
   homogeneousCochainsResNatTrans k φ ◫ 𝟙 _
 
 lemma resNatTrans_app (φ : H →ₜ* G) (n : ℕ) (X : TopRep k G) :
@@ -417,7 +418,7 @@ lemma cochainsMap₂_id_left (f : X ⟶ X') :
 followed by the functorial map on continuous cohomology. -/
 @[reassoc]
 lemma map₂_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
-    map₂ φ f n = (resNatTrans k φ n).app X ≫ (Functor k H n).map f := by
+    map₂ φ f n = (resNatTrans k φ n).app X ≫ Hₜ(k,H,n).map f := by
   rw [resNatTrans_app]
   exact (congrArg (HomologicalComplex.homologyMap · n) (cochainsMap₂_eq φ f)).trans
     (HomologicalComplex.homologyMap_comp _ _ _)
@@ -432,7 +433,7 @@ lemma map₂_id_right (φ : H →ₜ* G) (n : ℕ) :
 /-- The functorial map on continuous cohomology is the special case of `map₂` along the
 identity of `G`. -/
 lemma map₂_id_left (f : X ⟶ X') (n : ℕ) :
-    map₂ (ContinuousMonoidHom.id G) f n = (Functor k G n).map f := by
+    map₂ (ContinuousMonoidHom.id G) f n = Hₜ(k,G,n).map f := by
   simp only [map₂, cochainsMap₂_id_left]
   rfl
 

From e6c561958108655371d1adb1d0c81350b51170e8 Mon Sep 17 00:00:00 2001
From: Richard Hill <r.m.hill@ucl.ac.uk>
Date: Thu, 9 Jul 2026 15:29:24 +0100
Subject: [PATCH 03/10] lint

---
 .../ContCohomology/Functoriality.lean         | 254 ++++++++++--------
 1 file changed, 136 insertions(+), 118 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
index fc05933d110a97..55ddcd19afd13d 100644
--- a/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
@@ -18,10 +18,10 @@ representation `X` of `G`, a topological representation `Y` of `H`, and a morphi
 
 ## Main definitions
 
-* `ContinuousCohomology.cochainsMap₂ φ f` : the cochain map
+* `ContinuousCohomology.cochainsResMap φ f` : the cochain map
   `homogeneousCochains X ⟶ homogeneousCochains Y` induced by `φ : H →ₜ* G` and
   `f : res φ X ⟶ Y`, sending an invariant function `σ : C(G, C(G, ⋯))` to `f ∘ σ ∘ φ`.
-* `ContinuousCohomology.map₂ φ f n` : the induced map `Hⁿ(G, X) ⟶ Hⁿ(H, Y)` on continuous
+* `ContinuousCohomology.ResMap φ f n` : the induced map `Hⁿ(G, X) ⟶ Hⁿ(H, Y)` on continuous
   cohomology.
 -/
 
@@ -41,12 +41,13 @@ variable {k : Type u} {G H K : Type v} [Ring k] [TopologicalSpace k]
   [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
   {X X' X'' : TopRep k G} {Y : TopRep k H} {Z : TopRep k K}
 
+/-- The morphisms between the levels of the standard resolutions of `X` and `X'` induced by a
+morphism `f : X ⟶ X'`, given by applying `coind₁Functor` repeatedly. -/
 abbrev resolutionMap (f : X ⟶ X') :
     (i : ℕ) → (resolutionX X i) ⟶ (resolutionX X' i)
   | 0 => f
   | i + 1 => ((coind₁Functor k G).map (resolutionMap f i))
 
-@[simp]
 lemma resolutionMap_zero (f : X ⟶ X') : resolutionMap f 0 = f := rfl
 
 lemma resolutionMap_succ (f : X ⟶ X') (n : ℕ) :
@@ -76,6 +77,10 @@ lemma resolutionMap_comp (f : X ⟶ X') (f' : X' ⟶ X'') (i : ℕ) :
       map_comp]
 
 variable (k G)
+/-- The shifted standard resolution `resolution'` as a functor
+`TopRep k G ⥤ CochainComplex (TopRep k G) ℕ`, acting on morphisms by `resolutionMap`.
+The shifting removes the initial term `X` from the resolution of `X`, so that the zeroth term
+is `C(G,X)`. -/
 @[simps] abbrev resolution'Functor : TopRep k G ⥤ CochainComplex (TopRep k G) ℕ where
   obj           := resolution'
   map {X Y} f   := {
@@ -85,48 +90,50 @@ variable (k G)
   map_id _      := HomologicalComplex.hom_ext _ _ <| fun _ ↦ resolutionMap_id _
   map_comp _ _  := HomologicalComplex.hom_ext _ _ <| fun _ ↦ resolutionMap_comp _ _ _
 
+/-- The complex of homogeneous cochains `homogeneousCochains X` as a functor
+`TopRep k G ⥤ CochainComplex (TopModuleCat k) ℕ`. -/
 abbrev homogeneousCochainsFunctor : TopRep k G ⥤ CochainComplex (TopModuleCat k) ℕ :=
     resolution'Functor k G ⋙ (invariantsFunctor k G).mapHomologicalComplex (.up ℕ)
 
 lemma homogeneousCochainsFunctor_obj :
     (homogeneousCochainsFunctor k G).obj = homogeneousCochains := rfl
 
+/-- Continuous cohomology `Hⁿ(G, -)` as a functor `TopRep k G ⥤ TopModuleCat k`. -/
 noncomputable abbrev _root_.continuousCohomologyFunctor (n : ℕ) : TopRep k G ⥤ TopModuleCat k :=
     homogeneousCochainsFunctor k G ⋙ HomologicalComplex.homologyFunctor _ _ n
 
-notation "Hₜ" => continuousCohomology
-notation "Hₜ(" k "," G "," n ")" => continuousCohomologyFunctor k G n
+/-- `Hₜ n X` is the `n`-th continuous cohomology of a topological representation `X`. -/
+scoped notation "Hₜ" => continuousCohomology
+/-- `HₜFunct k G n` is the functor sending a topological `G`-representation `X` over `k` to its
+`n`-th continuous cohomology `Hⁿ(G, X)`. -/
+scoped notation "HₜFunct" => continuousCohomologyFunctor
 
-lemma Functor_obj (n : ℕ) : Hₜ(k,G,n).obj = Hₜ n := rfl
+lemma continuousCohomologyFunctor_obj (n : ℕ) : (HₜFunct k G n).obj = Hₜ n := rfl
 
 variable {k G}
 variable (X) in
-/-- The morphisms between the levels of the standard resolutions of `X` and `Y` induced by a
-continuous group homomorphism `φ : H →ₜ* G` and a morphism `f : res φ X ⟶ Y`, given by
-`F ↦ f ∘ F ∘ φ`. -/
+/-- The morphisms from the standard resolution of `X` to the standard resolution
+of the restriction of `X` induced by a continuous group homomorphism `φ : H →ₜ* G`.
+This morphism is given by `F ↦ F ∘ φ`. -/
 abbrev _root_.TopRep.resolutionXRes (φ : H →ₜ* G) :
     (i : ℕ) → (res φ (resolutionX X i)) ⟶ (resolutionX (res φ.toMonoidHom X) i)
   | 0 => 𝟙 _
   | i + 1 => ofHom (coind₁ResMap φ (resolutionXRes φ i).hom)
 
-@[simp]
 lemma resolutionXRes_zero (φ : H →ₜ* G) : X.resolutionXRes φ 0 = 𝟙 _ := rfl
 
-lemma resolutionXRes_one (φ : H →ₜ* G) : X.resolutionXRes φ 1 = ofHom (coind₁ResMap φ .id) := rfl
-
 lemma resolutionXRes_succ (φ : H →ₜ* G) (i : ℕ) :
     resolutionXRes X φ (i + 1) = ofHom (coind₁ResMap φ (resolutionXRes _ φ i).hom) := rfl
 
 @[simp]
 lemma resolutionXRes_id (X : TopRep k G) (i : ℕ) :
-    resolutionXRes X (ContinuousMonoidHom.id G) i = 𝟙 (resolutionX X i) := by
+    resolutionXRes X (.id G) i = 𝟙 (resolutionX X i) := by
   induction i with
   | zero => rfl
   | succ i ih =>
     rw [resolutionXRes_succ, ih]
     ext; rfl
 
-
 lemma resolutionXRes_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (i : ℕ) :
     resolutionXRes X (φ.comp ψ) i =
       (resFunctor ψ.toMonoidHom).map (resolutionXRes X φ i) ≫ resolutionXRes _ ψ i := by
@@ -136,7 +143,7 @@ lemma resolutionXRes_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (i : ℕ) :
     rw [resolutionXRes_succ, resolutionXRes_succ, resolutionXRes_succ, ih]
     ext; rfl
 
-/-- The maps `resolutionMap₂ φ f` commute with the differentials of the resolutions. -/
+/-- The maps `resolutionResMap φ f` commute with the differentials of the resolutions. -/
 lemma resolutionXRes_comp_d (φ : H →ₜ* G) (i : ℕ) :
     resolutionXRes X φ i ≫ d _ i =
       (resFunctor (φ : H →* G)).map (d X i) ≫ resolutionXRes X φ (i + 1) := by
@@ -162,6 +169,8 @@ lemma resolutionXRes_naturality (φ : H →ₜ* G) (f : X ⟶ X') (i : ℕ) :
     ext F x
     exact congr($(ih).hom (F (φ x)))
 
+/-- The cochain map from the restriction along `φ : H →ₜ* G` of the shifted standard resolution
+of `X` to the shifted standard resolution of `res φ X`, with levels `resolutionXRes X φ`. -/
 abbrev resolution'Res (φ : H →ₜ* G) :
     ((resFunctor φ.toMonoidHom).mapHomologicalComplex (.up ℕ)).obj (resolution' X)
     ⟶ resolution' (res φ.toMonoidHom X) where
@@ -172,6 +181,7 @@ abbrev resolution'Res (φ : H →ₜ* G) :
       CochainComplex.of_d, resolution'd_eq]
     exact resolutionXRes_comp_d φ _
 
+/-- The cochain maps `resolution'Res φ` as a natural transformation. -/
 def resolution'ResNatTrans (φ : H →ₜ* G) :
     resolution'Functor k G ⋙ (resFunctor ↑φ).mapHomologicalComplex (.up ℕ)
     ⟶ (resFunctor φ) ⋙ resolution'Functor k H where
@@ -180,21 +190,25 @@ def resolution'ResNatTrans (φ : H →ₜ* G) :
     ext n : 1
     exact resolutionXRes_naturality φ f (n + 1)
 
-def _root_.TopRep.homogeneousCochainsXRes (φ : H →ₜ* G) (X : TopRep k G) (n : ℕ) :
+/-- The restriction map between the `n`-th levels of the homogeneous cochain complexes of `X`
+and `res φ X`, sending an invariant function `σ` to `σ ∘ φ`. -/
+def homogeneousCochainsXRes (φ : H →ₜ* G) (X : TopRep k G) (n : ℕ) :
     X.homogeneousCochains.X n ⟶ (X.res φ.toMonoidHom).homogeneousCochains.X n :=
-  (X.resolutionX _).invariantsRes φ.toMonoidHom ≫ ((invariantsFunctor (k := k) (G := H)).map
-  (resolutionXRes X φ _))
+  (X.resolutionX _).invariantsRes φ.toMonoidHom
+  ≫ (invariantsFunctor k H).map (resolutionXRes X φ _)
 
-lemma _root_.TopRep.homogeneousCochainsXRes_zero (φ : H →ₜ* G) (X : TopRep k G) :
-    X.homogeneousCochainsXRes φ 0 =
+lemma homogeneousCochainsXRes_zero (φ : H →ₜ* G) (X : TopRep k G) :
+    homogeneousCochainsXRes φ X 0 =
     X.coind₁.invariantsRes φ ≫ (invariantsFunctor k H).map (ofHom (coind₁ResMap φ .id)) := rfl
 
-lemma _root_.TopRep.homogeneousCochainsXRes_succ (φ : H →ₜ* G) (X : TopRep k G) (n : ℕ) :
-    X.homogeneousCochainsXRes φ (n + 1) =
+lemma homogeneousCochainsXRes_succ (φ : H →ₜ* G) (X : TopRep k G) (n : ℕ) :
+    homogeneousCochainsXRes φ X (n + 1) =
     (X.resolution'X n).coind₁.invariantsRes φ ≫ (invariantsFunctor k H).map
     (ofHom (coind₁ResMap φ (X.resolutionXRes φ (n + 1)).hom)) := rfl
 
 variable (k) in
+/-- The natural transformation on homogeneous cochain complexes induced by restriction along a
+continuous group homomorphism `φ : H →ₜ* G`, with levels `homogeneousCochainsXRes φ`. -/
 def homogeneousCochainsResNatTrans (φ : H →ₜ* G) : homogeneousCochainsFunctor k G
     ⟶ (resFunctor φ.toMonoidHom) ⋙ homogeneousCochainsFunctor k H :=
   (𝟙 (resolution'Functor k G)
@@ -208,8 +222,10 @@ lemma homogeneousCochainsResNatTrans_app_f (φ : H →ₜ* G) (X : TopRep k G) (
     ((homogeneousCochainsResNatTrans k φ).app X).f n = homogeneousCochainsXRes φ X n := rfl
 
 variable (k) in
+/-- The restriction natural transformation `Hⁿ(G, -) ⟶ resFunctor φ ⋙ Hⁿ(H, -)` on continuous
+cohomology induced by a continuous group homomorphism `φ : H →ₜ* G`. -/
 noncomputable abbrev resNatTrans (φ : H →ₜ* G) (n : ℕ) :
-    Hₜ(k,G,n) ⟶ resFunctor φ.toMonoidHom ⋙ Hₜ(k,H,n) :=
+    HₜFunct k G n ⟶ resFunctor φ.toMonoidHom ⋙ HₜFunct k H n :=
   homogeneousCochainsResNatTrans k φ ◫ 𝟙 _
 
 lemma resNatTrans_app (φ : H →ₜ* G) (n : ℕ) (X : TopRep k G) :
@@ -217,58 +233,56 @@ lemma resNatTrans_app (φ : H →ₜ* G) (n : ℕ) (X : TopRep k G) :
       HomologicalComplex.homologyMap ((homogeneousCochainsResNatTrans k φ).app X) n := by
   simp only [resNatTrans, NatTrans.hcomp_id_app, HomologicalComplex.homologyFunctor_map]
 
-
-
 set_option allowUnsafeReducibility true in
 attribute [local reducible] CategoryTheory.Functor.mapHomologicalComplex
 
 /-- The morphisms between the levels of the standard resolutions of `X` and `Y` induced by a
 continuous group homomorphism `φ : H →ₜ* G` and a morphism `f : res φ X ⟶ Y`, given by
 `F ↦ f ∘ F ∘ φ`. -/
-def resolutionMap₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
+def resolutionResMap (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
     (i : ℕ) → res φ (resolutionX X i) ⟶ resolutionX Y i
   | 0 => f
-  | i + 1 => ofHom (coind₁ResMap φ (resolutionMap₂ φ f i).hom)
+  | i + 1 => ofHom (coind₁ResMap φ (resolutionResMap φ f i).hom)
 
 @[simp]
-lemma resolutionMap₂_zero (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
-    resolutionMap₂ φ f 0 = f := rfl
+lemma resolutionResMap_zero (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
+    resolutionResMap φ f 0 = f := rfl
 
-lemma resolutionMap₂_succ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
-    resolutionMap₂ φ f (i + 1) = ofHom (coind₁ResMap φ (resolutionMap₂ φ f i).hom) := rfl
+lemma resolutionResMap_succ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
+    resolutionResMap φ f (i + 1) = ofHom (coind₁ResMap φ (resolutionResMap φ f i).hom) := rfl
 
 @[simp]
-lemma resolutionMap₂_id (X : TopRep k G) (i : ℕ) :
-    resolutionMap₂ (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (resolutionX X i) := by
+lemma resolutionResMap_id (X : TopRep k G) (i : ℕ) :
+    resolutionResMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (resolutionX X i) := by
   induction i with
   | zero => rfl
   | succ i ih =>
-    rw [resolutionMap₂_succ, ih]
+    rw [resolutionResMap_succ, ih]
     ext F x
     rfl
 
-lemma resolutionMap₂_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z)
+lemma resolutionResMap_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z)
     (i : ℕ) :
-    resolutionMap₂ (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) i =
-      (resFunctor (ψ : K →* H)).map (resolutionMap₂ φ f i) ≫ resolutionMap₂ ψ g i := by
+    resolutionResMap (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) i =
+      (resFunctor (ψ : K →* H)).map (resolutionResMap φ f i) ≫ resolutionResMap ψ g i := by
   induction i with
   | zero => rfl
   | succ i ih =>
-    rw [resolutionMap₂_succ, resolutionMap₂_succ, resolutionMap₂_succ, ih]
+    rw [resolutionResMap_succ, resolutionResMap_succ, resolutionResMap_succ, ih]
     ext F x
     rfl
 
 
-/-- The maps `resolutionMap₂ φ f` commute with the differentials of the resolutions. -/
-lemma resolutionMap₂_comp_d (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
-    resolutionMap₂ φ f i ≫ d Y i =
-      (resFunctor (φ : H →* G)).map (d X i) ≫ resolutionMap₂ φ f (i + 1) := by
+/-- The maps `resolutionResMap φ f` commute with the differentials of the resolutions. -/
+lemma resolutionResMap_comp_d (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
+    resolutionResMap φ f i ≫ d Y i =
+      (resFunctor (φ : H →* G)).map (d X i) ≫ resolutionResMap φ f (i + 1) := by
   induction i with
   | zero => rfl
   | succ i ih =>
     ext : 1
     replace ih := congr($(ih).hom)
-    simp only [TopRep.hom_comp, resolutionMap₂_succ, TopRep.hom_ofHom, hom_d_succ,
+    simp only [TopRep.hom_comp, resolutionResMap_succ, TopRep.hom_ofHom, hom_d_succ,
       ContIntertwiningMap.restrict_sub, ContIntertwiningMap.sub_comp,
       ContIntertwiningMap.comp_sub, coind₁Map_comp_coind₁ResMap,
       coind₁ResMap_comp_coind₁Map_restrict] at ih ⊢
@@ -278,163 +292,167 @@ lemma resolutionMap₂_comp_d (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ)
 group homomorphism `φ : H →ₜ* G` and a morphism of topological `H`-representations
 `f : res φ X ⟶ Y`, sending an invariant function `σ : C(G, C(G, ⋯))` to `f ∘ σ ∘ φ`. -/
 @[simps! -isSimp f f_hom]
-def cochainsMap₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
+def cochainsResMap (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
     homogeneousCochains X ⟶ homogeneousCochains Y where
-  f i := invariantsResMap φ (resolutionMap₂ φ f (i + 1))
+  f i := invariantsResMap φ (resolutionResMap φ f (i + 1))
   comm' i j (hij : _ = _) := by
     subst hij
     rw [homogeneousCochains.d_eq, homogeneousCochains.d_eq, ← invariantsResMap_comp,
-      resolutionMap₂_comp_d, invariantsResMap_map_comp]
+      resolutionResMap_comp_d, invariantsResMap_map_comp]
 
 @[simp]
-lemma cochainsMap₂_id (X : TopRep k G) :
-    cochainsMap₂ (ContinuousMonoidHom.id G) (𝟙 X) = 𝟙 (homogeneousCochains X) := by
+lemma cochainsResMap_id (X : TopRep k G) :
+    cochainsResMap (ContinuousMonoidHom.id G) (𝟙 X) = 𝟙 (homogeneousCochains X) := by
   ext i : 1
-  rw [cochainsMap₂_f, resolutionMap₂_id]
+  rw [cochainsResMap_f, resolutionResMap_id]
   ext v
   rfl
 
 @[reassoc]
-lemma cochainsMap₂_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z) :
-    cochainsMap₂ (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) =
-      cochainsMap₂ φ f ≫ cochainsMap₂ ψ g := by
+lemma cochainsResMap_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z) :
+    cochainsResMap (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) =
+      cochainsResMap φ f ≫ cochainsResMap ψ g := by
   ext i v x
-  exact congr($(resolutionMap₂_comp φ ψ f g (i + 1)).hom v.1 x)
+  exact congr($(resolutionResMap_comp φ ψ f g (i + 1)).hom v.1 x)
 
 /-- The map `Zⁿ(G, X) ⟶ Zⁿ(H, Y)` on cocycles induced by a continuous group homomorphism
 `φ : H →ₜ* G` and a morphism of topological `H`-representations `f : res φ X ⟶ Y`. -/
-noncomputable abbrev cocyclesMap₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+noncomputable abbrev cocyclesResMap (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
     cocycles X n ⟶ cocycles Y n :=
-  HomologicalComplex.cyclesMap (cochainsMap₂ φ f) n
+  HomologicalComplex.cyclesMap (cochainsResMap φ f) n
 
 @[simp]
-lemma cocyclesMap₂_id (X : TopRep k G) (n : ℕ) :
-    cocyclesMap₂ (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 _ := by
-  simp [cocyclesMap₂]
+lemma cocyclesResMap_id (X : TopRep k G) (n : ℕ) :
+    cocyclesResMap (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 _ := by
+  simp [cocyclesResMap]
 
 @[reassoc]
-lemma cocyclesMap₂_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z)
+lemma cocyclesResMap_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z)
     (n : ℕ) :
-    cocyclesMap₂ (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) n =
-      cocyclesMap₂ φ f n ≫ cocyclesMap₂ ψ g n := by
-  simp [cocyclesMap₂, ← HomologicalComplex.cyclesMap_comp, ← cochainsMap₂_comp]
+    cocyclesResMap (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) n =
+      cocyclesResMap φ f n ≫ cocyclesResMap ψ g n := by
+  simp [cocyclesResMap, ← HomologicalComplex.cyclesMap_comp, ← cochainsResMap_comp]
 
 /-- The map `Hⁿ(G, X) ⟶ Hⁿ(H, Y)` on continuous cohomology induced by a continuous group
 homomorphism `φ : H →ₜ* G` and a morphism of topological `H`-representations
-`f : res φ X ⟶ Y`. -/
-noncomputable abbrev map₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+`f : res φ X ⟶ Y`.
+The name refers to the fact that this map is the composition of the restriction map
+`resNatTrans k φ` and `(HₜFunct k G n).map f`. -/
+-- TODO : bring the names of the analogous maps for `groupCohomology` in line with this.
+noncomputable abbrev resMap (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
     continuousCohomology n X ⟶ continuousCohomology n Y :=
-  HomologicalComplex.homologyMap (cochainsMap₂ φ f) n
+  HomologicalComplex.homologyMap (cochainsResMap φ f) n
 
 @[reassoc]
-theorem π_map₂ (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
-    π X n ≫ map₂ φ f n = cocyclesMap₂ φ f n ≫ π Y n := by
-  simp [map₂, cocyclesMap₂]
+theorem π_resMap (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+    π X n ≫ resMap φ f n = cocyclesResMap φ f n ≫ π Y n := by
+  simp [resMap, cocyclesResMap]
 
 @[simp]
-lemma map₂_id (X : TopRep k G) (n : ℕ) :
-    map₂ (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 _ := by
-  simp [map₂]
+lemma resMap_id (X : TopRep k G) (n : ℕ) :
+    resMap (ContinuousMonoidHom.id G) (𝟙 X) n = 𝟙 _ := by
+  simp [resMap]
 
 @[reassoc]
-lemma map₂_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z) (n : ℕ) :
-    map₂ (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) n =
-      map₂ φ f n ≫ map₂ ψ g n := by
-  simp [map₂, ← HomologicalComplex.homologyMap_comp, ← cochainsMap₂_comp]
+lemma resMap_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z) (n : ℕ) :
+    resMap (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) n =
+      resMap φ f n ≫ resMap ψ g n := by
+  simp [resMap, ← HomologicalComplex.homologyMap_comp, ← cochainsResMap_comp]
 
 /-!
 ### Relation to the functorial constructions
 
-The maps `resolutionMap₂`, `cochainsMap₂` and `map₂` combine restriction along `φ : H →ₜ* G` with
-functoriality in the coefficient representation. The following lemmas express them in terms of
+The maps `resolutionResMap`, `cochainsResMap` and `ResMap` combine restriction along `φ : H →ₜ* G`
+with functoriality in the coefficient representation. The following lemmas express them in terms of
 the two constructions they combine: `resolutionXRes`, `homogeneousCochainsResNatTrans` and
 `resNatTrans` (pure restriction), and `resolutionMap` and the functors
-`homogeneousCochainsFunctor` and `Functor` (pure coefficient maps).
+`homogeneousCochainsFunctor` and `continuousCohomologyFunctor` (pure coefficient maps).
 -/
 
-/-- `resolutionMap₂ φ f` is the restriction map `resolutionXRes X φ` followed by the functorial
+/-- `resolutionResMap φ f` is the restriction map `resolutionXRes X φ` followed by the functorial
 map `resolutionMap f`. -/
 @[reassoc]
-lemma resolutionMap₂_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
-    resolutionMap₂ φ f i = resolutionXRes X φ i ≫ resolutionMap f i := by
+lemma resolutionResMap_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
+    resolutionResMap φ f i = resolutionXRes X φ i ≫ resolutionMap f i := by
   induction i with
   | zero => rfl
   | succ i ih =>
-    rw [resolutionMap₂_succ, resolutionXRes_succ, resolutionMap_succ, ih]
+    rw [resolutionResMap_succ, resolutionXRes_succ, resolutionMap_succ, ih]
     ext F x
     rfl
 
-/-- `resolutionXRes` is the special case of `resolutionMap₂` where the coefficient map is the
+/-- `resolutionXRes` is the special case of `resolutionResMap` where the coefficient map is the
 identity. -/
-lemma resolutionMap₂_id_right (φ : H →ₜ* G) (i : ℕ) :
-    resolutionMap₂ φ (𝟙 (res φ.toMonoidHom X)) i = resolutionXRes X φ i := by
+lemma resolutionResMap_id_snd (φ : H →ₜ* G) (i : ℕ) :
+    resolutionResMap φ (𝟙 (res φ.toMonoidHom X)) i = resolutionXRes X φ i := by
   induction i with
   | zero => rfl
-  | succ i ih => rw [resolutionMap₂_succ, resolutionXRes_succ, ih]
+  | succ i ih => rw [resolutionResMap_succ, resolutionXRes_succ, ih]
 
-/-- `resolutionMap` is the special case of `resolutionMap₂` along the identity of `G`. -/
-lemma resolutionMap₂_id_left (f : X ⟶ X') (i : ℕ) :
-    resolutionMap₂ (ContinuousMonoidHom.id G) f i = resolutionMap f i := by
+/-- `resolutionMap` is the special case of `resolutionResMap` along the identity of `G`. -/
+lemma resolutionResMap_id_fst (f : X ⟶ X') (i : ℕ) :
+    resolutionResMap (ContinuousMonoidHom.id G) f i = resolutionMap f i := by
   induction i with
   | zero => rfl
   | succ i ih =>
-    rw [resolutionMap₂_succ, resolutionMap_succ, ih]
+    rw [resolutionResMap_succ, resolutionMap_succ, ih]
     ext F x
     rfl
 
-/-- `cochainsMap₂ φ f` is the component of the restriction natural transformation on homogeneous
+/-- `cochainsResMap φ f` is the component of the restriction natural transformation on homogeneous
 cochains followed by the functorial map on homogeneous cochains. -/
 @[reassoc]
-lemma cochainsMap₂_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
-    cochainsMap₂ φ f = (homogeneousCochainsResNatTrans k φ).app X ≫
+lemma cochainsResMap_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
+    cochainsResMap φ f = (homogeneousCochainsResNatTrans k φ).app X ≫
       (homogeneousCochainsFunctor k H).map f := by
   ext i v x
-  exact congr($(resolutionMap₂_eq φ f (i + 1)).hom v.1 x)
+  exact congr($(resolutionResMap_eq φ f (i + 1)).hom v.1 x)
 
-/-- The levelwise form of `cochainsMap₂_eq`: the restriction part expressed via
+/-- The levelwise form of `cochainsResMap_eq`: the restriction part expressed via
 `homogeneousCochainsXRes` and the coefficient part via `resolutionMap`. -/
 @[reassoc]
-lemma cochainsMap₂_f_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
-    (cochainsMap₂ φ f).f n = homogeneousCochainsXRes φ X n ≫
+lemma cochainsResMap_f_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+    (cochainsResMap φ f).f n = homogeneousCochainsXRes φ X n ≫
       (invariantsFunctor k H).map (resolutionMap f (n + 1)) := by
-  rw [cochainsMap₂_eq]
+  rw [cochainsResMap_eq]
   rfl
 
 /-- The component of the restriction natural transformation on homogeneous cochains is the
-special case of `cochainsMap₂` where the coefficient map is the identity. -/
-lemma cochainsMap₂_id_right (φ : H →ₜ* G) :
-    cochainsMap₂ φ (𝟙 (res φ.toMonoidHom X)) = (homogeneousCochainsResNatTrans k φ).app X := by
+special case of `cochainsResMap` where the coefficient map is the identity. -/
+lemma cochainsResMap_id_right (φ : H →ₜ* G) :
+    cochainsResMap φ (𝟙 (res φ.toMonoidHom X)) = (homogeneousCochainsResNatTrans k φ).app X := by
   ext i v x
-  exact congr($(resolutionMap₂_id_right φ (i + 1)).hom v.1 x)
+  exact congr($(resolutionResMap_id_snd φ (i + 1)).hom v.1 x)
 
-/-- The functorial map on homogeneous cochains is the special case of `cochainsMap₂` along the
+/-- The functorial map on homogeneous cochains is the special case of `cochainsResMap` along the
 identity of `G`. -/
-lemma cochainsMap₂_id_left (f : X ⟶ X') :
-    cochainsMap₂ (ContinuousMonoidHom.id G) f = (homogeneousCochainsFunctor k G).map f := by
+lemma cochainsResMap_id_left (f : X ⟶ X') :
+    cochainsResMap (ContinuousMonoidHom.id G) f = (homogeneousCochainsFunctor k G).map f := by
   ext i v x
-  exact congr($(resolutionMap₂_id_left f (i + 1)).hom v.1 x)
+  exact congr($(resolutionResMap_id_fst f (i + 1)).hom v.1 x)
 
-/-- `map₂ φ f n` is the component of the restriction natural transformation `resNatTrans`
+/-- `ResMap φ f n` is the component of the restriction natural transformation `resNatTrans`
 followed by the functorial map on continuous cohomology. -/
 @[reassoc]
-lemma map₂_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
-    map₂ φ f n = (resNatTrans k φ n).app X ≫ Hₜ(k,H,n).map f := by
+lemma ResMap_eq (φ : H →ₜ* G) (f : res φ X ⟶ Y) (n : ℕ) :
+    resMap φ f n = (resNatTrans k φ n).app X ≫ (HₜFunct k H n).map f := by
   rw [resNatTrans_app]
-  exact (congrArg (HomologicalComplex.homologyMap · n) (cochainsMap₂_eq φ f)).trans
+  exact (congrArg (HomologicalComplex.homologyMap · n) (cochainsResMap_eq φ f)).trans
     (HomologicalComplex.homologyMap_comp _ _ _)
 
-/-- The component of `resNatTrans` is the special case of `map₂` where the coefficient map is
+/-- The component of `resNatTrans` is the special case of `ResMap` where the coefficient map is
 the identity. -/
-lemma map₂_id_right (φ : H →ₜ* G) (n : ℕ) :
-    map₂ φ (𝟙 (res φ.toMonoidHom X)) n = (resNatTrans k φ n).app X := by
+lemma ResMap_id_right (φ : H →ₜ* G) (n : ℕ) :
+    resMap φ (𝟙 (res φ.toMonoidHom X)) n = (resNatTrans k φ n).app X := by
   rw [resNatTrans_app]
-  exact congrArg (HomologicalComplex.homologyMap · n) (cochainsMap₂_id_right φ)
+  exact congrArg (HomologicalComplex.homologyMap · n) (cochainsResMap_id_right φ)
 
-/-- The functorial map on continuous cohomology is the special case of `map₂` along the
+/-- The functorial map on continuous cohomology is the special case of `ResMap` along the
 identity of `G`. -/
-lemma map₂_id_left (f : X ⟶ X') (n : ℕ) :
-    map₂ (ContinuousMonoidHom.id G) f n = Hₜ(k,G,n).map f := by
-  simp only [map₂, cochainsMap₂_id_left]
+lemma ResMap_id_left (f : X ⟶ X') (n : ℕ) :
+    resMap (ContinuousMonoidHom.id G) f n = (HₜFunct k G n).map f := by
+  simp only [resMap, cochainsResMap_id_left]
   rfl
 
 end ContinuousCohomology
+

From 699fc19bf89fee2c4b982f955f0ecaccf45a16c0 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Thu, 9 Jul 2026 14:45:45 +0000
Subject: [PATCH 04/10] [pre-commit.ci lite] apply automatic fixes

---
 .../Homological/ContCohomology/Functoriality.lean                | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
index 55ddcd19afd13d..e9546ddd4c8c62 100644
--- a/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean
@@ -455,4 +455,3 @@ lemma ResMap_id_left (f : X ⟶ X') (n : ℕ) :
   rfl
 
 end ContinuousCohomology
-

From cf4d7206262e33af96572e8758e053bf7763fb8a Mon Sep 17 00:00:00 2001
From: Richard Hill <r.m.hill@ucl.ac.uk>
Date: Thu, 9 Jul 2026 16:33:01 +0100
Subject: [PATCH 05/10] initial commit

---
 .../Homological/ContCohomology/Inflation.lean | 167 ++++++++++++++++++
 Mathlib/Topology/Algebra/Group/Quotient.lean  |  15 ++
 2 files changed, 182 insertions(+)
 create mode 100644 Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean

diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
new file mode 100644
index 00000000000000..d1a4d6c8a99523
--- /dev/null
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
@@ -0,0 +1,167 @@
+/-
+Copyright (c) 2026 Richard Hill. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Hill
+-/
+import Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
+import Mathlib.Topology.Algebra.Group.Quotient
+
+/-!
+# Inflation maps in continuous cohomology
+
+Let `N` be a normal subgroup of a topological group `G`. For a topological representation `π`
+of `G`, the `N`-invariant vectors of `π` form a representation of the quotient group `G ⧸ N`;
+this construction is functorial in `π`. The inflation map `Hⁿ(G ⧸ N, π^N) ⟶ Hⁿ(G, π)` on
+continuous cohomology is obtained by restricting along the quotient map `G → G ⧸ N` and then
+composing with the map induced by the inclusion `π^N → π`.
+
+## Main definitions
+
+* `ContRepresentation.relInvariants N`: the `R`-submodule of `N`-invariant vectors of a
+  continuous representation.
+* `TopRep.relInvariantsFunctor R N`: the functor `TopRep R G ⥤ TopRep R (G ⧸ N)` sending a
+  topological representation of `G` to the induced representation of `G ⧸ N` on its
+  `N`-invariants.
+* `ContinuousCohomology.inflNatTrans R N n`: the inflation maps in degree `n`, as a natural
+  transformation `relInvariantsFunctor R N ⋙ HₜFunct R (G ⧸ N) n ⟶ HₜFunct R G n`.
+-/
+
+universe u₁ u₂ u₃
+open CategoryTheory
+  TopRep
+  ContRepresentation
+
+variable {R : Type u₁} [Ring R]
+variable {G H : Type u₂} [Group G] [Group H]
+
+namespace ContRepresentation
+
+variable {V W : Type u₃} [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V]
+    [Module R V] (ρ : ContRepresentation R G V)
+    [AddCommGroup W] [TopologicalSpace W] [IsTopologicalAddGroup W] [Module R W]
+    (ρ' : ContRepresentation R G W) (N : Subgroup G)
+
+/--
+For `ρ : ContRepresentation R G V` and a subgroup `N` of `G`,
+`ρ.relInvariants N` is the `R`-submodule of `V` consisting of the `N`-invariant elements.
+-/
+def relInvariants : Submodule R V where
+  carrier := {v : V | ∀ n ∈ N, ρ n v = v}
+  add_mem' h₁ h₂ _ h  := by rw [map_add, h₁, h₂] <;> exact h
+  zero_mem' _ _       := map_zero _
+  smul_mem' _ _ h _ _ := by rwa [map_smul, h]
+
+variable [hN : N.Normal]
+lemma rho_mem_relInvariants {v : V} (hv : v ∈ ρ.relInvariants N) (g : G) :
+    ρ g v ∈ ρ.relInvariants N := by
+  intro n hn
+  rw [← mul_apply_eq_comp, ← map_mul, show n * g = g * (g⁻¹ * n * g) by simp [mul_assoc],
+    map_mul, mul_apply_eq_comp, hv _ (hN.conj_mem' n hn g)]
+
+/-- For a normal subgroup `N` of `G`, `ρ.relInvariantsRho N` is the representation of `G` on
+the `N`-invariants `ρ.relInvariants N` induced by `ρ`. -/
+@[simps] def relInvariantsRho : ContRepresentation R G (ρ.relInvariants N) := ⟨{
+  toFun g       := (ρ g).restrict (fun _ hv ↦ ρ.rho_mem_relInvariants N hv g)
+  map_one'      := by ext; simp
+  map_mul' _ _  := by ext; simp
+}⟩
+
+/-- A continuous intertwining map `f : ρ →ⁱL ρ'` restricts to a continuous intertwining map
+`ρ.relInvariantsRho N →ⁱL ρ'.relInvariantsRho N` on `N`-invariants. -/
+def relInvariantsIntertwining (f : ρ →ⁱL ρ') :
+    ρ.relInvariantsRho N →ⁱL ρ'.relInvariantsRho N where
+  toContinuousLinearMap := f.toContinuousLinearMap.restrict (by
+    intro v hv n hn
+    have := (f.isIntertwining n v).symm
+    rwa [hv n hn] at this)
+  isIntertwining' g := by
+    ext v
+    simp only [ContinuousLinearMap.coe_comp, Function.comp_apply,
+      ContinuousLinearMap.coe_restrict_apply]
+    exact f.isIntertwining g v
+
+lemma le_relInvariantsRho_ker : N ≤ (ρ.relInvariantsRho N).toMonoidHom.ker := by
+  intro n hn
+  rw [MonoidHom.mem_ker]
+  ext ⟨_,hv⟩
+  apply hv _ hn
+
+/-- The representation of `G ⧸ N` on the `N`-invariants `ρ.relInvariants N`, obtained by
+factoring `ρ.relInvariantsRho N` through the quotient map `G → G ⧸ N`. -/
+def relInvariantsInfl : ContRepresentation R (G ⧸ N) (ρ.relInvariants N) :=
+  ⟨QuotientGroup.lift N (ρ.relInvariantsRho N) (ρ.le_relInvariantsRho_ker N)⟩
+
+/-- The continuous intertwining map `ρ.relInvariantsInfl N →ⁱL ρ'.relInvariantsInfl N` of
+`G ⧸ N`-representations induced by a continuous intertwining map `f : ρ →ⁱL ρ'`. -/
+def relInvariantsIntertwining' (f : ρ →ⁱL ρ') :
+    ρ.relInvariantsInfl N →ⁱL ρ'.relInvariantsInfl N where
+  toContinuousLinearMap := (relInvariantsIntertwining ρ ρ' N f).toContinuousLinearMap
+  isIntertwining' g := by
+    obtain ⟨g',rfl⟩ := g.exists_rep
+    apply (relInvariantsIntertwining ρ ρ' N f).isIntertwining'
+
+end ContRepresentation
+
+variable [TopologicalSpace R] (N : Subgroup G) [N.Normal] (R)
+
+namespace TopRep
+
+/-- The functor `TopRep R G ⥤ TopRep R (G ⧸ N)` sending a topological representation of `G` to
+the induced representation of `G ⧸ N` on its `N`-invariants. -/
+def relInvariantsFunctor : TopRep R G ⥤ TopRep R (G ⧸ N) where
+  obj rep       := TopRep.of (rep.ρ.relInvariantsInfl N)
+  map f         := TopRep.ofHom (relInvariantsIntertwining' _ _ N f.hom)
+
+/-- The natural transformation whose component at a topological representation `π` of `G` is the
+inclusion of the `N`-invariants of `π`, regarded as a `G`-representation by restriction along the
+quotient map `G → G ⧸ N`. -/
+@[simps] def inflι : (relInvariantsFunctor R N ⋙ resFunctor (QuotientGroup.mk' N)) ⟶ 𝟭 (TopRep R G)
+    where
+  app _ := TopRep.ofHom {
+    toFun := Subtype.val
+    map_add' _ _ := rfl
+    map_smul' _ _ := rfl
+    isIntertwining' _ := rfl
+  }
+  naturality _ _ _ := rfl
+
+end TopRep
+
+variable [TopologicalSpace G] [IsTopologicalGroup G]
+
+noncomputable section
+namespace ContinuousCohomology
+
+/-- The inflation map from the `n`-th continuous cohomology of the `G ⧸ N`-representation on the
+`N`-invariants of `π` to the `n`-th continuous cohomology of `π`. -/
+abbrev inflApp (n : ℕ) (π : TopRep R G) :
+    (relInvariantsFunctor R N ⋙ HₜFunct R (G ⧸ N) n).obj π ⟶ (HₜFunct R G n).obj ((𝟭 _).obj π) :=
+  (resNatTrans R (QuotientTopGroup.mk N) n).app ((relInvariantsFunctor R N).obj π)
+  ≫ (HₜFunct R G n).map ((inflι R N).app π)
+
+/-- The components `inflApp N n` are natural in the representation: they intertwine the
+functorial maps on continuous cohomology. -/
+lemma inflApp_naturality (n : ℕ) {π₁ π₂ : TopRep R G} (f : π₁ ⟶ π₂) :
+    (relInvariantsFunctor R N ⋙ HₜFunct R (G ⧸ N) n).map f ≫ inflApp R N n π₂ =
+      inflApp R N n π₁ ≫ (HₜFunct R G n).map f := by
+  have h := (HₜFunct R G n).congr_map ((inflι R N).naturality f)
+  rw [Functor.map_comp, Functor.map_comp] at h
+  refine ((resNatTrans R (QuotientTopGroup.mk N) n).naturality_assoc
+    ((relInvariantsFunctor R N).map f) _).trans ?_
+  rw [Category.assoc]
+  exact whisker_eq _ h
+
+/-- The inflation maps `inflApp N n` as a natural transformation
+`relInvariantsFunctor N ⋙ HₜFunct R (G ⧸ N) n ⟶ HₜFunct R G n`. -/
+noncomputable def inflNatTrans (n : ℕ) :
+    relInvariantsFunctor R N ⋙ HₜFunct R (G ⧸ N) n ⟶ HₜFunct R G n where
+  app            := inflApp R N n
+  naturality _ _ f := by
+    /-
+    Note that the following proof is a lot quicker than `exact inflApp_naturality N n f`.
+    -/
+    have := inflApp_naturality R N n f
+    simpa only [Functor.id_obj] using this
+
+end ContinuousCohomology
+end
diff --git a/Mathlib/Topology/Algebra/Group/Quotient.lean b/Mathlib/Topology/Algebra/Group/Quotient.lean
index 218ecfba0e2974..a1b3996394676c 100644
--- a/Mathlib/Topology/Algebra/Group/Quotient.lean
+++ b/Mathlib/Topology/Algebra/Group/Quotient.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.GroupTheory.GroupAction.Quotient
 public import Mathlib.GroupTheory.QuotientGroup.Defs
+public import Mathlib.Topology.Algebra.ContinuousMonoidHom
 public import Mathlib.Topology.Algebra.Group.Pointwise
 public import Mathlib.Topology.Maps.OpenQuotient
 
@@ -15,6 +16,9 @@ public import Mathlib.Topology.Maps.OpenQuotient
 
 In this file we define topology on `G ⧸ N`, where `N` is a subgroup of `G`,
 and prove basic properties of this topology.
+
+When `N` is normal, we also bundle the quotient map as a continuous monoid homomorphism
+`QuotientTopGroup.mk`.
 -/
 
 public section
@@ -44,6 +48,17 @@ theorem isQuotientMap_mk (N : Subgroup G) : IsQuotientMap (mk : G → G ⧸ N) :
 theorem continuous_mk {N : Subgroup G} : Continuous (mk : G → G ⧸ N) :=
   continuous_quot_mk
 
+/-- The quotient map `G → G ⧸ N` as a continuous monoid homomorphism. -/
+@[expose, to_additive QuotientTopAddGroup.mk
+/-- The quotient map `G → G ⧸ N` as a continuous additive monoid homomorphism. -/]
+def _root_.QuotientTopGroup.mk (N : Subgroup G) [N.Normal] : G →ₜ* G ⧸ N where
+  toMonoidHom := mk' N
+  continuous_toFun := continuous_mk
+
+@[to_additive (attr := simp) QuotientTopAddGroup.coe_mk]
+lemma _root_.QuotientTopGroup.coe_mk (N : Subgroup G) [N.Normal] :
+    ↑(QuotientTopGroup.mk N) = mk' N := rfl
+
 section ContinuousMul
 
 variable [SeparatelyContinuousMul G] {N : Subgroup G}

From f559304a7da148221624cd7ceccfe90e471ec9b2 Mon Sep 17 00:00:00 2001
From: Richard Hill <r.m.hill@ucl.ac.uk>
Date: Thu, 9 Jul 2026 17:03:43 +0100
Subject: [PATCH 06/10] switch between abbrevs and defs

---
 .../Homological/ContCohomology/Inflation.lean | 34 +++++++++----------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
index d1a4d6c8a99523..cb3da33f3912cb 100644
--- a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
@@ -108,21 +108,27 @@ namespace TopRep
 
 /-- The functor `TopRep R G ⥤ TopRep R (G ⧸ N)` sending a topological representation of `G` to
 the induced representation of `G ⧸ N` on its `N`-invariants. -/
-def relInvariantsFunctor : TopRep R G ⥤ TopRep R (G ⧸ N) where
+abbrev relInvariantsFunctor : TopRep R G ⥤ TopRep R (G ⧸ N) where
   obj rep       := TopRep.of (rep.ρ.relInvariantsInfl N)
   map f         := TopRep.ofHom (relInvariantsIntertwining' _ _ N f.hom)
 
-/-- The natural transformation whose component at a topological representation `π` of `G` is the
-inclusion of the `N`-invariants of `π`, regarded as a `G`-representation by restriction along the
-quotient map `G → G ⧸ N`. -/
-@[simps] def inflι : (relInvariantsFunctor R N ⋙ resFunctor (QuotientGroup.mk' N)) ⟶ 𝟭 (TopRep R G)
-    where
-  app _ := TopRep.ofHom {
+variable {R} in
+def inflιapp (π : TopRep R G) :
+    (res (QuotientGroup.mk' N)) ((relInvariantsFunctor R N).obj π) ⟶ π :=
+  TopRep.ofHom {
     toFun := Subtype.val
     map_add' _ _ := rfl
     map_smul' _ _ := rfl
     isIntertwining' _ := rfl
   }
+
+
+/-- The natural transformation whose component at a topological representation `π` of `G` is the
+inclusion of the `N`-invariants of `π`, regarded as a `G`-representation by restriction along the
+quotient map `G → G ⧸ N`. -/
+abbrev inflι :
+    (relInvariantsFunctor R N ⋙ resFunctor (QuotientGroup.mk' N)) ⟶ 𝟭 (TopRep R G) where
+  app := inflιapp N
   naturality _ _ _ := rfl
 
 end TopRep
@@ -134,8 +140,7 @@ namespace ContinuousCohomology
 
 /-- The inflation map from the `n`-th continuous cohomology of the `G ⧸ N`-representation on the
 `N`-invariants of `π` to the `n`-th continuous cohomology of `π`. -/
-abbrev inflApp (n : ℕ) (π : TopRep R G) :
-    (relInvariantsFunctor R N ⋙ HₜFunct R (G ⧸ N) n).obj π ⟶ (HₜFunct R G n).obj ((𝟭 _).obj π) :=
+def inflApp (n : ℕ) (π : TopRep R G) : Hₜ n ((relInvariantsFunctor R N).obj π) ⟶ Hₜ n π :=
   (resNatTrans R (QuotientTopGroup.mk N) n).app ((relInvariantsFunctor R N).obj π)
   ≫ (HₜFunct R G n).map ((inflι R N).app π)
 
@@ -148,20 +153,15 @@ lemma inflApp_naturality (n : ℕ) {π₁ π₂ : TopRep R G} (f : π₁ ⟶ π
   rw [Functor.map_comp, Functor.map_comp] at h
   refine ((resNatTrans R (QuotientTopGroup.mk N) n).naturality_assoc
     ((relInvariantsFunctor R N).map f) _).trans ?_
-  rw [Category.assoc]
+  erw [Category.assoc]
   exact whisker_eq _ h
 
 /-- The inflation maps `inflApp N n` as a natural transformation
 `relInvariantsFunctor N ⋙ HₜFunct R (G ⧸ N) n ⟶ HₜFunct R G n`. -/
-noncomputable def inflNatTrans (n : ℕ) :
+noncomputable abbrev inflNatTrans (n : ℕ) :
     relInvariantsFunctor R N ⋙ HₜFunct R (G ⧸ N) n ⟶ HₜFunct R G n where
   app            := inflApp R N n
-  naturality _ _ f := by
-    /-
-    Note that the following proof is a lot quicker than `exact inflApp_naturality N n f`.
-    -/
-    have := inflApp_naturality R N n f
-    simpa only [Functor.id_obj] using this
+  naturality _ _ f := inflApp_naturality R N n f
 
 end ContinuousCohomology
 end

From 239cfe65bbe8ab55b41937a7d7a239ed1de7fcbf Mon Sep 17 00:00:00 2001
From: Richard Hill <r.m.hill@ucl.ac.uk>
Date: Thu, 9 Jul 2026 17:34:06 +0100
Subject: [PATCH 07/10] sort out a few things

---
 .../Homological/ContCohomology/Inflation.lean | 31 ++++++++++++++-----
 1 file changed, 24 insertions(+), 7 deletions(-)

diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
index cb3da33f3912cb..5e27e78c1f3831 100644
--- a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
@@ -113,6 +113,8 @@ abbrev relInvariantsFunctor : TopRep R G ⥤ TopRep R (G ⧸ N) where
   map f         := TopRep.ofHom (relInvariantsIntertwining' _ _ N f.hom)
 
 variable {R} in
+/-- The inclusion into `π` of the `N`-invariants of `π`, regarded as a `G`-representation by
+restriction along the quotient map `G → G ⧸ N`. This is the component at `π` of `inflι`. -/
 def inflιapp (π : TopRep R G) :
     (res (QuotientGroup.mk' N)) ((relInvariantsFunctor R N).obj π) ⟶ π :=
   TopRep.ofHom {
@@ -122,6 +124,10 @@ def inflιapp (π : TopRep R G) :
     isIntertwining' _ := rfl
   }
 
+variable {R N} in
+@[simp] lemma inflιapp_apply {π : TopRep R G}
+    (v : (res (QuotientGroup.mk' N)) ((relInvariantsFunctor R N).obj π))
+    : (inflιapp N π).hom v = ↑v := rfl
 
 /-- The natural transformation whose component at a topological representation `π` of `G` is the
 inclusion of the `N`-invariants of `π`, regarded as a `G`-representation by restriction along the
@@ -144,17 +150,27 @@ def inflApp (n : ℕ) (π : TopRep R G) : Hₜ n ((relInvariantsFunctor R N).obj
   (resNatTrans R (QuotientTopGroup.mk N) n).app ((relInvariantsFunctor R N).obj π)
   ≫ (HₜFunct R G n).map ((inflι R N).app π)
 
+/-- Abstract form of `inflApp_naturality`: given `α : K ⟶ L ⋙ H` and `ι : Φ ⋙ L ⟶ 𝟭 A`, the
+maps `α.app (Φ.obj π) ≫ H.map (ι.app π)` are natural in `π`. Stating this for opaque functors
+keeps the elaboration of the concrete instance below cheap. -/
+private lemma inflApp_naturality_aux {A B M : Type*} [Category A] [Category B] [Category M]
+    (Φ : A ⥤ B) (K : B ⥤ M) (L : B ⥤ A) (H : A ⥤ M)
+    (α : K ⟶ L ⋙ H) (ι : Φ ⋙ L ⟶ 𝟭 A) {π₁ π₂ : A} (f : π₁ ⟶ π₂) :
+    (Φ ⋙ K).map f ≫ (α.app (Φ.obj π₂) ≫ H.map (ι.app π₂)) =
+      (α.app (Φ.obj π₁) ≫ H.map (ι.app π₁)) ≫ H.map f := by
+  have h := (Functor.whiskerLeft Φ α ≫ Functor.whiskerRight ι H).naturality f
+  simp only [NatTrans.comp_app, Functor.whiskerLeft_app, Functor.whiskerRight_app,
+    Functor.comp_map, Functor.id_map, Category.assoc] at h ⊢
+  exact h
+
 /-- The components `inflApp N n` are natural in the representation: they intertwine the
 functorial maps on continuous cohomology. -/
 lemma inflApp_naturality (n : ℕ) {π₁ π₂ : TopRep R G} (f : π₁ ⟶ π₂) :
     (relInvariantsFunctor R N ⋙ HₜFunct R (G ⧸ N) n).map f ≫ inflApp R N n π₂ =
-      inflApp R N n π₁ ≫ (HₜFunct R G n).map f := by
-  have h := (HₜFunct R G n).congr_map ((inflι R N).naturality f)
-  rw [Functor.map_comp, Functor.map_comp] at h
-  refine ((resNatTrans R (QuotientTopGroup.mk N) n).naturality_assoc
-    ((relInvariantsFunctor R N).map f) _).trans ?_
-  erw [Category.assoc]
-  exact whisker_eq _ h
+      inflApp R N n π₁ ≫ (HₜFunct R G n).map f :=
+  inflApp_naturality_aux (relInvariantsFunctor R N) (HₜFunct R (G ⧸ N) n)
+    (resFunctor (QuotientGroup.mk' N)) (HₜFunct R G n)
+    (resNatTrans R (QuotientTopGroup.mk N) n) (inflι R N) f
 
 /-- The inflation maps `inflApp N n` as a natural transformation
 `relInvariantsFunctor N ⋙ HₜFunct R (G ⧸ N) n ⟶ HₜFunct R G n`. -/
@@ -165,3 +181,4 @@ noncomputable abbrev inflNatTrans (n : ℕ) :
 
 end ContinuousCohomology
 end
+

From 9d3fd507c5c231d1af3a1b03d75b83a64ef21044 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Thu, 9 Jul 2026 16:43:24 +0000
Subject: [PATCH 08/10] [pre-commit.ci lite] apply automatic fixes

---
 .../Homological/ContCohomology/Inflation.lean                    | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
index 5e27e78c1f3831..fcecf3d7387166 100644
--- a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
@@ -181,4 +181,3 @@ noncomputable abbrev inflNatTrans (n : ℕ) :
 
 end ContinuousCohomology
 end
-

From 867d4e10f6d6649bb641e1b68b3f825ec446f2a3 Mon Sep 17 00:00:00 2001
From: Richard Hill <r.m.hill@ucl.ac.uk>
Date: Sat, 11 Jul 2026 09:55:40 +0100
Subject: [PATCH 09/10] fix import

---
 Mathlib.lean                                           |  1 +
 .../Homological/ContCohomology/Inflation.lean          | 10 ++++++++--
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index bf4256c6cb96b2..e1e54a345c18ea 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6392,6 +6392,7 @@ public import Mathlib.RepresentationTheory.FinGroupCharZero
 public import Mathlib.RepresentationTheory.FiniteIndex
 public import Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
 public import Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
+public import Mathlib.RepresentationTheory.Homological.ContCohomology.Inflation
 public import Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree
 public import Mathlib.RepresentationTheory.Homological.FiniteCyclic
 public import Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
index fcecf3d7387166..1b8d297df6fcd3 100644
--- a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
@@ -3,8 +3,10 @@ Copyright (c) 2026 Richard Hill. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Richard Hill
 -/
-import Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
-import Mathlib.Topology.Algebra.Group.Quotient
+module
+
+public import Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
+public import Mathlib.Topology.Algebra.Group.Quotient
 
 /-!
 # Inflation maps in continuous cohomology
@@ -26,6 +28,8 @@ composing with the map induced by the inclusion `π^N → π`.
   transformation `relInvariantsFunctor R N ⋙ HₜFunct R (G ⧸ N) n ⟶ HₜFunct R G n`.
 -/
 
+@[expose] public section
+
 universe u₁ u₂ u₃
 open CategoryTheory
   TopRep
@@ -181,3 +185,5 @@ noncomputable abbrev inflNatTrans (n : ℕ) :
 
 end ContinuousCohomology
 end
+end
+

From 888020e604d520fb38dadf3d6bcc6c029784732a Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Sat, 11 Jul 2026 08:56:26 +0000
Subject: [PATCH 10/10] [pre-commit.ci lite] apply automatic fixes

---
 .../Homological/ContCohomology/Inflation.lean                    | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
index 1b8d297df6fcd3..e40efa21869591 100644
--- a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
@@ -186,4 +186,3 @@ noncomputable abbrev inflNatTrans (n : ℕ) :
 end ContinuousCohomology
 end
 end
-