Invariant vectors and maps on cosets

For a representation ρ of a group G and a vector x fixed by a subgroup H, the value ρ a x depends only on the left coset aH. This holds over any semiring.

For a representation ρ of a submonoid Δ of a group and a subgroup Γ contained in Δ, let q be a semilinear map satisfying q ∘ ρ(γ) = q for γ ∈ Γ. Then q ∘ ρ(x) depends only on the right coset Γ x. In particular, sums of these maps can be compared using coset decompositions, as in HeckeCoset.heckeSum_eq_sum_of_rightCosets.

The target of q may be a module over a different semiring: the coset argument uses only composition and the invariance of q.

theorem Representation.apply_eq_apply_of_quotientGroup_mk_eq {R : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring R] [Group G] [AddCommMonoid V] [Module R V] (ρ : Representation R G V) {H : Subgroup G} {x : V} (hx : ∀ (h : ↥H), (ρ ↑h) x = x) {a b : G} (hab : ↑a = ↑b) : (ρ a) x = (ρ b) x

The image of an H-fixed vector under ρ depends only on the left coset aH.

theorem Representation.comp_eq_of_rightCoset_eq {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ : Subgroup G} {R : Type u_2} {S : Type u_3} {V : Type u_4} {W : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module S W] {σ : R →+* S} (ρ : Representation R (↥Δ) V) (hΓ : Γ.toSubmonoid ≤ Δ) {q : V →ₛₗ[σ] W} (hq : ∀ (γ : G) (hγ : γ ∈ Γ), q ∘ₛₗ ρ ⟨γ, ⋯⟩ = q) {x y : G} (hx : x ∈ Δ) (hy : y ∈ Δ) (h : MulOpposite.op x • ↑Γ = MulOpposite.op y • ↑Γ) : q ∘ₛₗ ρ ⟨x, hx⟩ = q ∘ₛₗ ρ ⟨y, hy⟩

For a Γ-invariant semilinear map q, the map q ∘ ρ(x) depends only on the right coset Γ x.