Subrepresentations

This file defines subrepresentations of a group representation.

structure Subrepresentation {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] (ρ : Representation A G W) : Type u_3

A subrepresentation of G of the A-module W is a submodule of W which is stable under the G-action.

• toSubmodule : Submodule A W

  A subrepresentation is a submodule.

• apply_mem_toSubmodule (g : G) ⦃v : W⦄ : v ∈ self.toSubmodule → (ρ g) v ∈ self.toSubmodule

theorem Subrepresentation.toSubmodule_injective {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} : Function.Injective toSubmodule

instance Subrepresentation.instSetLike {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} : SetLike (Subrepresentation ρ) W

Equations

• Subrepresentation.instSetLike = { coe := fun (ρ' : Subrepresentation ρ) => ↑ρ'.toSubmodule, coe_injective' := ⋯ }

def Subrepresentation.toRepresentation {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ' : Subrepresentation ρ) : Representation A G ↥ρ'.toSubmodule

A subrepresentation is a representation.

Equations

• ρ'.toRepresentation = { toFun := fun (g : G) => (ρ g).restrict ⋯, map_one' := ⋯, map_mul' := ⋯ }

instance Subrepresentation.instMax {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} : Max (Subrepresentation ρ)

Equations

• Subrepresentation.instMax = { max := fun (ρ₁ ρ₂ : Subrepresentation ρ) => { toSubmodule := ρ₁.toSubmodule ⊔ ρ₂.toSubmodule, apply_mem_toSubmodule := ⋯ } }

instance Subrepresentation.instMin {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} : Min (Subrepresentation ρ)

Equations

• Subrepresentation.instMin = { min := fun (ρ₁ ρ₂ : Subrepresentation ρ) => { toSubmodule := ρ₁.toSubmodule ⊓ ρ₂.toSubmodule, apply_mem_toSubmodule := ⋯ } }

@[simp]

theorem Subrepresentation.coe_sup {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ₁ ρ₂ : Subrepresentation ρ) : ↑(ρ₁ ⊔ ρ₂) = ↑ρ₁ + ↑ρ₂

@[simp]

theorem Subrepresentation.coe_inf {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ₁ ρ₂ : Subrepresentation ρ) : ↑(ρ₁ ⊓ ρ₂) = ↑ρ₁ ∩ ↑ρ₂

@[simp]

theorem Subrepresentation.toSubmodule_sup {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ₁ ρ₂ : Subrepresentation ρ) : (ρ₁ ⊔ ρ₂).toSubmodule = ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

@[simp]

theorem Subrepresentation.toSubmodule_inf {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (ρ₁ ρ₂ : Subrepresentation ρ) : (ρ₁ ⊓ ρ₂).toSubmodule = ρ₁.toSubmodule ⊓ ρ₂.toSubmodule

instance Subrepresentation.instLattice {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} : Lattice (Subrepresentation ρ)

Equations

• Subrepresentation.instLattice = Function.Injective.lattice Subrepresentation.toSubmodule ⋯ ⋯ ⋯

instance Subrepresentation.instBoundedOrder {A : Type u_1} [CommRing A] {G : Type u_2} [Group G] {W : Type u_3} [AddCommMonoid W] [Module A W] {ρ : Representation A G W} : BoundedOrder (Subrepresentation ρ)

Equations

• Subrepresentation.instBoundedOrder = { top := { toSubmodule := ⊤, apply_mem_toSubmodule := ⋯ }, le_top := ⋯, bot := { toSubmodule := ⊥, apply_mem_toSubmodule := ⋯ }, bot_le := ⋯ }