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

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

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

instance Subrepresentation.instPartialOrder {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} : PartialOrder (Subrepresentation ρ)

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.

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 ρ)

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 ρ)

@[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 ρ) : ↑(ρ₁ ⊔ ρ₂) = ↑ρ₁ + ↑ρ₂

@[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 ρ) : ↑(ρ₁ ⊓ ρ₂) = ↑ρ₁ ∩ ↑ρ₂

@[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

@[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

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 ρ)

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 ρ)

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.

@[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 ∈ σ

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.

@[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 ∈ σ

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.

@[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

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 ρ.

@[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

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.

@[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

@[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

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 ρ.

@[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'

@[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