The invariants of a normal subgroup as a representation of the quotient

For a continuous representation π of a group G on V and a normal subgroup S ≤ G, the invariants of the restricted representation π|_S form a G-stable submodule of V, and the action of G on it factors through G ⧸ S. This file builds that G ⧸ S-representation, both in the unbundled language and in the category TopRep, together with the inclusion of the invariants back into the ambient object.

It also provides the elementary continuous linear equivalence between an additive subgroup of a topological additive group and the invariants of a continuous representation when their underlying elements agree. This coefficient-level identification is independent of the quotient-representation construction.

These are the continuous counterparts of Mathlib's Representation.toInvariants, Representation.quotientToInvariants, Representation.quotientToInvariants_lift and Rep.quotientToInvariantsFunctor. They are the coefficient half of inflation: the compatible pair inducing Hⁿ(G ⧸ S, Xˢ) ⟶ Hⁿ(G, X) on continuous cohomology consists of the quotient homomorphism G → G ⧸ S together with the inclusion Xˢ ↪ X.

Main definitions

• AddSubgroup.continuousLinearEquivInvariants: an additive subgroup is continuously linearly equivalent to a representation's invariants when membership agrees.
• ContRepresentation.toInvariants: the representation of G on the invariants of π|_S.
• ContRepresentation.quotientToInvariants: the representation of G ⧸ S on the invariants of π|_S.
• TopRep.quotientToInvariants: the same construction in the category TopRep.
• TopRep.quotientToInvariantsι: the inclusion of the invariants into the ambient object, as a morphism of G-objects.
• TopRep.quotientToInvariantsFunctor: the functor X ↦ Xˢ.

Main results

• ContRepresentation.apply_mem_invariants_restrict: the invariants of π|_S are a G-stable submodule when S is normal.
• ContRepresentation.invariants_restrict_bot, ContRepresentation.invariants_restrict_top: the two degenerate subgroups.
• TopRep.quotientToInvariantsMap_comp_quotientToInvariantsι: naturality of the inclusion of the invariants.
• TopRep.isIso_invariantsResMap_quotientToInvariantsι: taking quotient invariants and then invariants under the quotient recovers the original invariants.

These declarations live in the root AddSubgroup, ContRepresentation and TopRep namespaces, rather than under TauCeti, so that dot notation on the Mathlib types they extend elaborates.

def AddSubgroup.continuousLinearEquivInvariants {G : Type u_1} {M : Type u_2} [Monoid G] [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (S : AddSubgroup M) (pi : ContRepresentation ℤ G M) (h : ∀ (m : M), m ∈ pi.invariants ↔ m ∈ S) : ↥S ≃L[ℤ] ↥pi.invariants

An additive subgroup of a topological additive group is continuously linearly equivalent to the invariants of a continuous representation when they have the same underlying elements.

Equations

• S.continuousLinearEquivInvariants pi h = ContinuousLinearEquiv.ofEq (AddSubgroup.toIntSubmodule S) pi.invariants ⋯

@[simp]

theorem AddSubgroup.continuousLinearEquivInvariants_val {G : Type u_1} {M : Type u_2} [Monoid G] [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (S : AddSubgroup M) (pi : ContRepresentation ℤ G M) (h : ∀ (m : M), m ∈ pi.invariants ↔ m ∈ S) (m : ↥S) : ↑((S.continuousLinearEquivInvariants pi h) m) = ↑m

@[simp]

theorem AddSubgroup.continuousLinearEquivInvariants_symm_val {G : Type u_1} {M : Type u_2} [Monoid G] [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (S : AddSubgroup M) (pi : ContRepresentation ℤ G M) (h : ∀ (m : M), m ∈ pi.invariants ↔ m ∈ S) (m : ↥pi.invariants) : ↑((S.continuousLinearEquivInvariants pi h).symm m) = ↑m

theorem ContRepresentation.mem_invariants_restrict {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] {π : ContRepresentation R G V} {S : Subgroup G} {v : V} : v ∈ (π.restrict S.subtype).invariants ↔ ∀ s ∈ S, (π s) v = v

Membership in the invariants of π|_S, in terms of elements of G lying in S.

@[simp]

theorem ContRepresentation.invariants_restrict_bot {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) : (π.restrict ⊥.subtype).invariants = ⊤

The trivial subgroup fixes everything.

@[simp]

theorem ContRepresentation.invariants_restrict_top {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) : (π.restrict ⊤.subtype).invariants = π.invariants

The invariants of the whole group are the invariants of π.

theorem ContRepresentation.apply_mem_invariants_restrict {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (S : Subgroup G) [S.Normal] (g : G) (v : V) (hv : v ∈ (π.restrict S.subtype).invariants) : (π g) v ∈ (π.restrict S.subtype).invariants

For a normal subgroup S, the invariants of π|_S are a G-stable submodule: this is the statement that makes toInvariants below a representation of G and not merely of S.

@[reducible, inline]

abbrev ContRepresentation.toInvariants {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (S : Subgroup G) [S.Normal] : ContRepresentation R G ↥(π.restrict S.subtype).invariants

The representation of G on the invariants of π|_S, for a normal subgroup S ≤ G; the continuous counterpart of Representation.toInvariants.

Equations

• π.toInvariants S = π.subrepresentation (π.restrict S.subtype).invariants ⋯

theorem ContRepresentation.coe_toInvariants_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (S : Subgroup G) [S.Normal] (g : G) (v : ↥(π.restrict S.subtype).invariants) : ↑(((π.toInvariants S) g) v) = (π g) ↑v

The action on the invariants of π|_S is the ambient action, read on the underlying vectors.

theorem ContRepresentation.toInvariants_apply_of_mem {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (S : Subgroup G) [S.Normal] {s : G} (hs : s ∈ S) : (π.toInvariants S) s = 1

S acts trivially on the invariants of π|_S, which is what lets the G-action descend to G ⧸ S.

def ContRepresentation.quotientToInvariants {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (S : Subgroup G) [S.Normal] : ContRepresentation R (G ⧸ S) ↥(π.restrict S.subtype).invariants

The representation of G ⧸ S on the invariants of π|_S, for a normal subgroup S ≤ G; the continuous counterpart of Representation.quotientToInvariants.

Equations

• π.quotientToInvariants S = { toMonoidHom := QuotientGroup.lift S (π.toInvariants S).toMonoidHom ⋯ }

@[simp]

theorem ContRepresentation.quotientToInvariants_mk {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (S : Subgroup G) [S.Normal] (g : G) : (π.quotientToInvariants S) ↑g = (π.toInvariants S) g

theorem ContRepresentation.coe_quotientToInvariants_mk_apply {R : Type u_1} {G : Type u_2} {V : Type u_3} [Ring R] [Group G] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module R V] (π : ContRepresentation R G V) (S : Subgroup G) [S.Normal] (g : G) (v : ↥(π.restrict S.subtype).invariants) : ↑(((π.quotientToInvariants S) ↑g) v) = (π g) ↑v

The G ⧸ S-action on the invariants of π|_S, read on the underlying vectors.

@[reducible, inline]

abbrev TopRep.quotientToInvariants {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (X : TopRep R G) (S : Subgroup G) [S.Normal] : TopRep R (G ⧸ S)

The G ⧸ S-object on the S-invariants of a topological representation, for a normal subgroup S ≤ G. This is the coefficient half of inflation.

Equations

• X.quotientToInvariants S = TopRep.of (X.ρ.quotientToInvariants S)

def TopRep.quotientToInvariantsι {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (X : TopRep R G) (S : Subgroup G) [S.Normal] : res (QuotientGroup.mk' S) (X.quotientToInvariants S) ⟶ X

The inclusion Xˢ ↪ X of the S-invariants into the ambient object, as a morphism of G-objects, where Xˢ is a G-object by restriction along G → G ⧸ S. Together with the quotient homomorphism it is the compatible pair defining inflation; it is the continuous counterpart of Representation.quotientToInvariants_lift.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopRep.quotientToInvariantsι_apply {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (X : TopRep R G) (S : Subgroup G) [S.Normal] (v : ↥(X.ρ.restrict S.subtype).invariants) : (CategoryTheory.ConcreteCategory.hom (X.quotientToInvariantsι S)) v = ↑v

The inclusion of the S-invariants into the ambient object sends an invariant vector to itself.

def TopRep.quotientToInvariantsMap {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] {X Y : TopRep R G} (f : X ⟶ Y) (S : Subgroup G) [S.Normal] : X.quotientToInvariants S ⟶ Y.quotientToInvariants S

A morphism f : X ⟶ Y of topological G-representations restricts to the S-invariants.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopRep.coe_quotientToInvariantsMap_apply {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (S : Subgroup G) [S.Normal] {X Y : TopRep R G} (f : X ⟶ Y) (v : ↥(X.ρ.restrict S.subtype).invariants) : ↑((CategoryTheory.ConcreteCategory.hom (quotientToInvariantsMap f S)) v) = (Hom.hom f) ↑v

The restriction of a morphism f : X ⟶ Y to the S-invariants sends an invariant vector v to f v.

@[simp]

theorem TopRep.quotientToInvariantsMap_id {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (X : TopRep R G) (S : Subgroup G) [S.Normal] : quotientToInvariantsMap (CategoryTheory.CategoryStruct.id X) S = CategoryTheory.CategoryStruct.id (X.quotientToInvariants S)

@[simp]

theorem TopRep.quotientToInvariantsMap_comp {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (S : Subgroup G) [S.Normal] {X Y Z : TopRep R G} (f : X ⟶ Y) (g : Y ⟶ Z) : quotientToInvariantsMap (CategoryTheory.CategoryStruct.comp f g) S = CategoryTheory.CategoryStruct.comp (quotientToInvariantsMap f S) (quotientToInvariantsMap g S)

@[simp]

theorem TopRep.quotientToInvariantsMap_comp_quotientToInvariantsι {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (S : Subgroup G) [S.Normal] {X Y : TopRep R G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (ofHom (ContIntertwiningMap.restrict (QuotientGroup.mk' S) (Hom.hom (quotientToInvariantsMap f S)))) (Y.quotientToInvariantsι S) = CategoryTheory.CategoryStruct.comp (X.quotientToInvariantsι S) f

The inclusion of the invariants is natural: restricting f : X ⟶ Y to the S-invariants and then including into Y is including into X and then applying f. This is the square that makes the compatible pair defining inflation natural in the coefficients.

@[simp]

theorem TopRep.quotientToInvariantsMap_comp_quotientToInvariantsι_assoc {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (S : Subgroup G) [S.Normal] {X Y : TopRep R G} (f : X ⟶ Y) {Z : TopRep R G} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (ofHom (ContIntertwiningMap.restrict (QuotientGroup.mk' S) (Hom.hom (quotientToInvariantsMap f S)))) (CategoryTheory.CategoryStruct.comp (Y.quotientToInvariantsι S) h) = CategoryTheory.CategoryStruct.comp (X.quotientToInvariantsι S) (CategoryTheory.CategoryStruct.comp f h)

The inclusion of the invariants is natural: restricting f : X ⟶ Y to the S-invariants and then including into Y is including into X and then applying f. This is the square that makes the compatible pair defining inflation natural in the coefficients.

theorem TopRep.isIso_invariantsResMap_quotientToInvariantsι {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (X : TopRep R G) (S : Subgroup G) [S.Normal] : CategoryTheory.IsIso (invariantsResMap (QuotientGroup.mk' S) (X.quotientToInvariantsι S))

(X^S)^{G/S} is canonically isomorphic to X^G. The map induced on invariants by the inclusion X^S ⟶ X is an isomorphism, with inverse preserving the underlying vector.

noncomputable def TopRep.quotientToInvariantsFunctor (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u_2) [Group G] (S : Subgroup G) [S.Normal] : CategoryTheory.Functor (TopRep R G) (TopRep R (G ⧸ S))

The functor sending a topological G-representation X to the G ⧸ S-representation on Xˢ; the continuous counterpart of Rep.quotientToInvariantsFunctor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopRep.quotientToInvariantsFunctor_obj_ρ (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u_2) [Group G] (S : Subgroup G) [S.Normal] (X : TopRep R G) : ((quotientToInvariantsFunctor R G S).obj X).ρ = X.ρ.quotientToInvariants S

@[simp]

theorem TopRep.quotientToInvariantsFunctor_obj_V (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u_2) [Group G] (S : Subgroup G) [S.Normal] (X : TopRep R G) : ↑((quotientToInvariantsFunctor R G S).obj X) = ↥(X.ρ.restrict S.subtype).invariants

@[simp]

theorem TopRep.quotientToInvariantsFunctor_obj_hV3 (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u_2) [Group G] (S : Subgroup G) [S.Normal] (X : TopRep R G) : ((quotientToInvariantsFunctor R G S).obj X).hV3 = instTopologicalSpaceSubtype

@[simp]

theorem TopRep.quotientToInvariantsFunctor_map (R : Type u_1) [Ring R] [TopologicalSpace R] (G : Type u_2) [Group G] (S : Subgroup G) [S.Normal] {X✝ Y✝ : TopRep R G} (f : X✝ ⟶ Y✝) : (quotientToInvariantsFunctor R G S).map f = quotientToInvariantsMap f S