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/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..e9546ddd4c8c62 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.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.
 -/
 
 @[expose] public section
 
-universe u v
+universe u v w
 
-open CategoryTheory
+open CategoryTheory CategoryTheory.Functor
 
 namespace ContinuousCohomology
 
@@ -39,7 +39,199 @@ 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}
+
+/-- 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))
+
+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)
+/-- 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   := {
+    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 _ _ _
+
+/-- 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
+
+/-- `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 continuousCohomologyFunctor_obj (n : ℕ) : (HₜFunct k G n).obj = Hₜ n := rfl
+
+variable {k G}
+variable (X) in
+/-- 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)
+
+lemma resolutionXRes_zero (φ : H →ₜ* G) : X.resolutionXRes φ 0 = 𝟙 _ := 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 (.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 `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
+  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)))
+
+/-- 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
+  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 φ _
+
+/-- 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
+  app X := resolution'Res φ
+  naturality X Y f := by
+    ext n : 1
+    exact resolutionXRes_naturality φ f (n + 1)
+
+/-- 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 H).map (resolutionXRes X φ _)
+
+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 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)
+    ◫ ((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
+/-- 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ₜFunct k G n ⟶ resFunctor φ.toMonoidHom ⋙ HₜFunct 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 +239,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 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 ⊢
@@ -99,67 +292,166 @@ 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 `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 `continuousCohomologyFunctor` (pure coefficient maps).
+-/
+
+/-- `resolutionResMap φ f` is the restriction map `resolutionXRes X φ` followed by the functorial
+map `resolutionMap f`. -/
+@[reassoc]
+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 [resolutionResMap_succ, resolutionXRes_succ, resolutionMap_succ, ih]
+    ext F x
+    rfl
+
+/-- `resolutionXRes` is the special case of `resolutionResMap` where the coefficient map is the
+identity. -/
+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 [resolutionResMap_succ, resolutionXRes_succ, ih]
+
+/-- `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 [resolutionResMap_succ, resolutionMap_succ, ih]
+    ext F x
+    rfl
+
+/-- `cochainsResMap φ f` is the component of the restriction natural transformation on homogeneous
+cochains followed by the functorial map on homogeneous cochains. -/
+@[reassoc]
+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($(resolutionResMap_eq φ f (i + 1)).hom v.1 x)
+
+/-- The levelwise form of `cochainsResMap_eq`: the restriction part expressed via
+`homogeneousCochainsXRes` and the coefficient part via `resolutionMap`. -/
+@[reassoc]
+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 [cochainsResMap_eq]
+  rfl
+
+/-- The component of the restriction natural transformation on homogeneous cochains is the
+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($(resolutionResMap_id_snd φ (i + 1)).hom v.1 x)
+
+/-- The functorial map on homogeneous cochains is the special case of `cochainsResMap` along the
+identity of `G`. -/
+lemma cochainsResMap_id_left (f : X ⟶ X') :
+    cochainsResMap (ContinuousMonoidHom.id G) f = (homogeneousCochainsFunctor k G).map f := by
+  ext i v x
+  exact congr($(resolutionResMap_id_fst f (i + 1)).hom v.1 x)
+
+/-- `ResMap φ f n` is the component of the restriction natural transformation `resNatTrans`
+followed by the functorial map on continuous cohomology. -/
+@[reassoc]
+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) (cochainsResMap_eq φ f)).trans
+    (HomologicalComplex.homologyMap_comp _ _ _)
+
+/-- The component of `resNatTrans` is the special case of `ResMap` where the coefficient map is
+the identity. -/
+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) (cochainsResMap_id_right φ)
+
+/-- The functorial map on continuous cohomology is the special case of `ResMap` along the
+identity of `G`. -/
+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
diff --git a/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
new file mode 100644
index 00000000000000..e40efa21869591
--- /dev/null
+++ b/Mathlib/RepresentationTheory/Homological/ContCohomology/Inflation.lean
@@ -0,0 +1,188 @@
+/-
+Copyright (c) 2026 Richard Hill. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Hill
+-/
+module
+
+public import Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
+public 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`.
+-/
+
+@[expose] public section
+
+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. -/
+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)
+
+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 {
+    toFun := Subtype.val
+    map_add' _ _ := rfl
+    map_smul' _ _ := rfl
+    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
+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
+
+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 `π`. -/
+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 π)
+
+/-- 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 :=
+  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`. -/
+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 := inflApp_naturality R N n f
+
+end ContinuousCohomology
+end
+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}