Subrepresentations #

This file defines subrepresentations of a monoid representation.

structure Subrepresentation {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [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

Instances For

source

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

Function.Injective toSubmodule

source

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

SetLike (Subrepresentation ρ) W

Equations

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

source

def Subrepresentation.toRepresentation {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [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' := ⋯ }

Instances For

source

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

Max (Subrepresentation ρ)

Equations

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

source

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

Min (Subrepresentation ρ)

Equations

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

source

@[simp]

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

↑(ρ₁ ⊔ ρ₂) = ↑ρ₁ + ↑ρ₂

source

@[simp]

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

↑(ρ₁ ⊓ ρ₂) = ↑ρ₁ ∩ ↑ρ₂

source

@[simp]

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

(ρ₁ ⊔ ρ₂).toSubmodule = ρ₁.toSubmodule ⊔ ρ₂.toSubmodule

source

@[simp]

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

(ρ₁ ⊓ ρ₂).toSubmodule = ρ₁.toSubmodule ⊓ ρ₂.toSubmodule

source

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

Lattice (Subrepresentation ρ)

Equations

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

source

instance Subrepresentation.instBoundedOrder {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [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 := ⋯ }

source

def Subrepresentation.asSubmodule {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (σ : Subrepresentation ρ) :

Submodule (MonoidAlgebra A G) ρ.asModule

A subrepresentation of ρ can be thought of as an A[G] submodule of ρ.asModule.

Equations

σ.asSubmodule = { toAddSubmonoid := σ.toSubmodule.toAddSubmonoid, smul_mem' := ⋯ }

Instances For

source

@[simp]

theorem Subrepresentation.mem_asSubmodule_iff {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} {σ : Subrepresentation ρ} {v : W} :

v ∈ σ.asSubmodule ↔ v ∈ σ

source

def Subrepresentation.asSubmodule' {A : Type u_1} {G : Type u_2} {M : Type u_4} [CommRing A] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra A G) M] (σ : Subrepresentation (Representation.ofModule M)) :

Submodule (MonoidAlgebra A G) M

A subrepresentation of ofModule M can be thought of as an A[G] submodule of M.

Equations

σ.asSubmodule' = { toAddSubmonoid := σ.toSubmodule.toAddSubmonoid, smul_mem' := ⋯ }

Instances For

source

@[simp]

theorem Subrepresentation.mem_asSubmodule'_iff {A : Type u_1} {G : Type u_2} {M : Type u_4} [CommRing A] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra A G) M] {σ : Subrepresentation (Representation.ofModule M)} {m : M} :

m ∈ σ.asSubmodule' ↔ m ∈ σ

source

def Subrepresentation.ofSubmodule {A : Type u_1} {G : Type u_2} {M : Type u_4} [CommRing A] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra A G) M] (N : Submodule (MonoidAlgebra A G) M) :

Subrepresentation (Representation.ofModule M)

A submodule of an A[G]-module M can be thought of as a subrepresentation of ofModule M.

Equations

Subrepresentation.ofSubmodule N = { toSubmodule := { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }, apply_mem_toSubmodule := ⋯ }

Instances For

source

@[simp]

theorem Subrepresentation.mem_ofSubmodule_iff {A : Type u_1} {G : Type u_2} {M : Type u_4} [CommRing A] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra A G) M] {N : Submodule (MonoidAlgebra A G) M} {m : M} :

m ∈ ofSubmodule N ↔ m ∈ N

source

def Subrepresentation.ofSubmodule' {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (N : Submodule (MonoidAlgebra A G) ρ.asModule) :

Subrepresentation ρ

An A[G]-submodule of ρ.asModule can be thought of as a subrepresentation of ρ.

Equations

Subrepresentation.ofSubmodule' N = { toSubmodule := { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }, apply_mem_toSubmodule := ⋯ }

Instances For

source

@[simp]

theorem Subrepresentation.mem_ofSubmodule'_iff {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} {N : Submodule (MonoidAlgebra A G) ρ.asModule} {w : W} :

w ∈ ofSubmodule' N ↔ w ∈ N

source

def Subrepresentation.subrepresentationSubmoduleOrderIso {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} :

Subrepresentation ρ ≃o Submodule (MonoidAlgebra A G) ρ.asModule

An order-preserving equivalence between subrepresentations of ρ and submodules of ρ.asModule.

Equations

Subrepresentation.subrepresentationSubmoduleOrderIso = { toFun := Subrepresentation.asSubmodule, invFun := Subrepresentation.ofSubmodule', left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

Instances For

source

@[simp]

theorem Subrepresentation.subrepresentationSubmoduleOrderIso_apply {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (σ : Subrepresentation ρ) :

subrepresentationSubmoduleOrderIso σ = σ.asSubmodule

source

@[simp]

theorem Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply {A : Type u_1} {G : Type u_2} {W : Type u_3} [CommRing A] [Monoid G] [AddCommMonoid W] [Module A W] {ρ : Representation A G W} (N : Submodule (MonoidAlgebra A G) ρ.asModule) :

(RelIso.symm subrepresentationSubmoduleOrderIso) N = ofSubmodule' N

source

def Subrepresentation.submoduleSubrepresentationOrderIso {A : Type u_1} {G : Type u_2} {M : Type u_4} [CommRing A] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra A G) M] :

Submodule (MonoidAlgebra A G) M ≃o Subrepresentation (Representation.ofModule M)

An order-preserving equivalence between A[G]-submodules of an A[G]-module M and subrepresentations of ρ.

Equations

Subrepresentation.submoduleSubrepresentationOrderIso = { toFun := Subrepresentation.ofSubmodule, invFun := Subrepresentation.asSubmodule', left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

Instances For

source

@[simp]

theorem Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply {A : Type u_1} {G : Type u_2} {M : Type u_4} [CommRing A] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra A G) M] (σ : Subrepresentation (Representation.ofModule M)) :

(RelIso.symm submoduleSubrepresentationOrderIso) σ = σ.asSubmodule'

source

@[simp]

theorem Subrepresentation.submoduleSubrepresentationOrderIso_apply {A : Type u_1} {G : Type u_2} {M : Type u_4} [CommRing A] [Monoid G] [AddCommMonoid M] [Module (MonoidAlgebra A G) M] (N : Submodule (MonoidAlgebra A G) M) :

submoduleSubrepresentationOrderIso N = ofSubmodule N

Documentation

Mathlib.RepresentationTheory.Subrepresentation

Subrepresentations #