Iterated restriction of topological representations

This file supplements Mathlib's restriction TopRep.res φ of a topological representation along a monoid homomorphism φ with its behaviour under composition: restricting along φ and then along ψ is restricting along φ.comp ψ, restricting along the identity does nothing, and so restricting along a group isomorphism and then along its inverse gives the representation back.

Main results

• TopRep.res_res: Res_ψ (Res_φ X) = Res_{φ ∘ ψ} X.
• TopRep.res_id: Res_id X = X.
• TopRep.res_symm_res: Res_{e⁻¹} (Res_e X) = X for e : H ≃* G.

@[simp]

theorem TopRep.res_res {k : Type u_1} {G : Type u_2} {H : Type u_3} {K : Type u_4} [Ring k] [TopologicalSpace k] [Group G] [Group H] [Monoid K] (φ : H →* G) (ψ : K →* H) (X : TopRep k G) : res ψ (res φ X) = res (φ.comp ψ) X

Restricting along φ and then along ψ is restricting along the composite φ.comp ψ.

@[simp]

theorem TopRep.res_id {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] (X : TopRep k G) : res (MonoidHom.id G) X = X

Restricting along the identity gives back the representation.

theorem TopRep.res_symm_res {k : Type u_1} {G : Type u_2} {H : Type u_3} [Ring k] [TopologicalSpace k] [Group G] [Group H] (e : H ≃* G) (X : TopRep k G) : res e.symm.toMonoidHom (res e.toMonoidHom X) = X

Restricting along e : H ≃* G and then along e⁻¹ gives back the representation.