feat(RepresentationTheory/Homological/ContCohomology): add inflation maps in continuous cohomology

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

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)`. -/

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