Subrepresentations and quotients in TopRep k G

An invariant submodule of a continuous representation inherits its topology and action, and the quotient by an invariant submodule carries the quotient topology and descended action. The inclusion and projection have the expected universal factorization properties.

@[reducible, inline]

abbrev TopRep.subrepresentation {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) : TopRep R G

Restrict a continuous representation to an invariant submodule, with the induced topology.

@[simp]

theorem TopRep.subrepresentation_ρ_apply {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (g : G) (x : ↑(X.subrepresentation W hW)) : ((X.subrepresentation W hW).ρ g) x = ⟨(X.ρ g) ↑x, ⋯⟩

The action on a subrepresentation is the ambient action with its membership proof.

noncomputable def TopRep.subrepresentationι {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) : X.subrepresentation W hW ⟶ X

The inclusion of an invariant subrepresentation into its ambient representation.

@[simp]

theorem TopRep.subrepresentationι_apply {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (x : ↑(X.subrepresentation W hW)) : (Hom.hom (X.subrepresentationι W hW)) x = ↑x

The inclusion of a subrepresentation is the subtype map.

theorem TopRep.subrepresentationι_injective {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) : Function.Injective ⇑(Hom.hom (X.subrepresentationι W hW))

The inclusion of a subrepresentation is injective.

def TopRep.subrepresentationLift {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : Y ⟶ X) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ W) : Y ⟶ X.subrepresentation W hW

Factor a morphism into an invariant subrepresentation when its image is contained there.

@[simp]

theorem TopRep.subrepresentationLift_apply {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : Y ⟶ X) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ W) (y : ↑Y) : (Hom.hom (subrepresentationLift X W hW f hf)) y = ⟨(Hom.hom f) y, ⋯⟩

The subrepresentation factorization evaluates by the original morphism.

@[simp]

theorem TopRep.subrepresentationLift_comp_ι {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : Y ⟶ X) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ W) : CategoryTheory.CategoryStruct.comp (subrepresentationLift X W hW f hf) (X.subrepresentationι W hW) = f

Composing the subrepresentation factorization with the inclusion recovers the morphism.

@[simp]

theorem TopRep.subrepresentationLift_comp_ι_assoc {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : Y ⟶ X) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ W) {Z : TopRep R G} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (subrepresentationLift X W hW f hf) (CategoryTheory.CategoryStruct.comp (X.subrepresentationι W hW) h) = CategoryTheory.CategoryStruct.comp f h

Composing the subrepresentation factorization with the inclusion recovers the morphism.

theorem TopRep.subrepresentationLift_unique {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : Y ⟶ X) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ W) (g : Y ⟶ X.subrepresentation W hW) (hg : CategoryTheory.CategoryStruct.comp g (X.subrepresentationι W hW) = f) : g = subrepresentationLift X W hW f hf

A morphism into a subrepresentation is determined by its composite with the inclusion.

@[reducible, inline]

abbrev TopRep.quotient {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) : TopRep R G

Descend a continuous representation to the quotient by an invariant submodule.

@[simp]

theorem TopRep.quotient_ρ {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) : (X.quotient W hW).ρ = X.ρ.quotient W hW

The operators of a quotient representation are the descended operators.

def TopRep.quotientπ {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) : X ⟶ X.quotient W hW

The projection from a representation to its quotient by an invariant submodule.

@[simp]

theorem TopRep.quotientπ_apply {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (x : ↑X) : (Hom.hom (X.quotientπ W hW)) x = Submodule.Quotient.mk x

The quotient projection sends a vector to its class.

theorem TopRep.quotientπ_surjective {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) : Function.Surjective ⇑(Hom.hom (X.quotientπ W hW))

The quotient projection is surjective.

def TopRep.quotientDesc {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : X ⟶ Y) (hf : ∀ x ∈ W, (Hom.hom f) x = 0) : X.quotient W hW ⟶ Y

Factor a morphism through a quotient when it vanishes on the invariant submodule.

@[simp]

theorem TopRep.quotientDesc_mk {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : X ⟶ Y) (hf : ∀ x ∈ W, (Hom.hom f) x = 0) (x : ↑X) : (Hom.hom (quotientDesc X W hW f hf)) (Submodule.Quotient.mk x) = (Hom.hom f) x

The quotient factorization evaluated on a class is the original morphism on a representative.

@[simp]

theorem TopRep.quotientπ_comp_quotientDesc {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : X ⟶ Y) (hf : ∀ x ∈ W, (Hom.hom f) x = 0) : CategoryTheory.CategoryStruct.comp (X.quotientπ W hW) (quotientDesc X W hW f hf) = f

Composing the quotient projection with the quotient factorization recovers the morphism.

@[simp]

theorem TopRep.quotientπ_comp_quotientDesc_assoc {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : X ⟶ Y) (hf : ∀ x ∈ W, (Hom.hom f) x = 0) {Z : TopRep R G} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.quotientπ W hW) (CategoryTheory.CategoryStruct.comp (quotientDesc X W hW f hf) h) = CategoryTheory.CategoryStruct.comp f h

Composing the quotient projection with the quotient factorization recovers the morphism.

theorem TopRep.quotientDesc_unique {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] {Y : TopRep R G} (X : TopRep R G) (W : Submodule R ↑X) (hW : ∀ (g : G), ∀ x ∈ W, (X.ρ g) x ∈ W) (f : X ⟶ Y) (hf : ∀ x ∈ W, (Hom.hom f) x = 0) (g : X.quotient W hW ⟶ Y) (hg : CategoryTheory.CategoryStruct.comp (X.quotientπ W hW) g = f) : g = quotientDesc X W hW f hf

A morphism out of a quotient is determined by its composite with the projection.