Cellular algebras

This file defines cellular algebras, in the style of Graham and Lehrer. The definition is not exactly the same as in their paper, but it is close enough for our purposes. We also define cell modules and the resultant representation theory.

Preliminary and helper definitions

To speak naturally about cellular algebras it will be useful to have some shorthands for tableaux sets and spans. Here, as in the definition that follows, $\Lambda$ is some type of "weights" and there is map that takes a weight to a set of "tableaux" for that weight.

def double_tableaux_in {Λ : Type} (S : Set Λ) (tableau : Λ → Type) : Set ((μ : Λ) × tableau μ × tableau μ)

The set of all triples ${}^\mu_{s_1, s_2}$ where $\mu$ is a weight in some set and $s_1, s_2$ are tableaux of shape $\mu$.

We express it here as the preimage of the set $S$ under the map from all triples ${}^\mu_{s_1, s_2}$ to their weight $\mu$.

Equations

• double_tableaux_in S tableau = Sigma.fst ⁻¹' S

theorem double_tableaux_in_mono {Λ : Type} {S₁ S₂ : Set Λ} {tableau : Λ → Type} (h : S₁ ⊆ S₂) : double_tableaux_in S₁ tableau ⊆ double_tableaux_in S₂ tableau

Increasing the set of weights increases the set of all double-tableaux.

def all_tableaux_range {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] {Λ : Type} (S : Set Λ) {tableau : Λ → Type} (c : Module.Basis ((μ : Λ) × tableau μ × tableau μ) k A) : Set A

Equations

• all_tableaux_range A S c = ⇑c '' double_tableaux_in S tableau

def tableau_linear_span {k : Type} [Field k] {A : Type} [Ring A] [Algebra k A] {Λ : Type} (S : Set Λ) {tableau : Λ → Type} (c : Module.Basis ((μ : Λ) × tableau μ × tableau μ) k A) : Submodule k A

The k-linear span of a subset of tableaux.

When this is a subset of weights closed under the partial order, we will show taht this is a two-sided ideal of the cellular algebra. However, we need a definition now so that we can talk about the multiplication rule for the basis elements.

Equations

• (c over S) = Submodule.span k (all_tableaux_range A S c)

def term_Over_ : Lean.TrailingParserDescr

Equations

• term_Over_ = Lean.ParserDescr.trailingNode `term_Over_ 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "over") (Lean.ParserDescr.cat `term 0))

def antiinvolution {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] (f : A →ₗ[k] A) : Prop

An anti-involution is a linear involution that reverses the order of multiplication.

Equations

• antiinvolution A f = ∀ (a b : A), f (a * b) = f b * f a

Main definition

class CellularAlgebra (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] : Type 1

A definition of a cellular algebra, in the style of Graham and Lehrer.

In this definition, instead of asking for a linear form $r$ over all of $A$, we just ask for an arbitrary function defined on the basis elements. This is extended to all of $A$ by linearity in CellularAlgebra.r.

Similarly, the multiplication condition is most often written as a condition on $a \cdot c^\mu_{s, t}$, but we ask for a condition on $c^ν_{s', t'} \cdot c^\mu_{s, t}$ for simplicity, and then extend it to all of $A$ in CellularAlgebra.multiplication_rule.

• Λ : Type
• Λ_order : PartialOrder (Λ k A)
• Λ_fintype : Fintype (Λ k A)
• tableau : Λ k A → Type
• fintype_tableau (μ : Λ k A) : Fintype (tableau μ)
• decidable_eq_tableau (μ : Λ k A) : DecidableEq (tableau μ)
• inhabited_tableau (μ : Λ k A) : Inhabited (tableau μ)
• c : Module.Basis ((μ : Λ k A) × tableau μ × tableau μ) k A
• ι_antiinvolution : antiinvolution A ((c.constr k) fun (x : (μ : Λ k A) × tableau μ × tableau μ) => match x with | ⟨μ, (s, t)⟩ => c ⟨μ, (t, s)⟩)
• r_basis : (ν : Λ k A) × tableau ν × tableau ν → (μ : Λ k A) → tableau μ → tableau μ → k
• multiplication_rule_basis (a : (μ : Λ k A) × tableau μ × tableau μ) (μ : Λ k A) (s t : tableau μ) : c a * c ⟨μ, (s, t)⟩ ≡ ∑ u : tableau μ, r_basis a μ s u • c ⟨μ, (u, t)⟩ [SMOD c over{ν : Λ k A | ν < μ}]

Instances and restatements

For convenience, we restate some of the data of a cellular algebra as instances, so that we can use them without having to refer to the cellular namespace.

instance instFintypeΛ {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] : Fintype (CellularAlgebra.Λ k A)

Equations

• instFintypeΛ A = CellularAlgebra.Λ_fintype

instance instFintypeTableau {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : CellularAlgebra.Λ k A) : Fintype (CellularAlgebra.tableau μ)

Equations

• instFintypeTableau A μ = CellularAlgebra.fintype_tableau μ

instance instDecidableEqTableau {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : CellularAlgebra.Λ k A) : DecidableEq (CellularAlgebra.tableau μ)

Equations

• instDecidableEqTableau A μ = CellularAlgebra.decidable_eq_tableau μ

instance instPartialOrderΛ {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] : PartialOrder (CellularAlgebra.Λ k A)

Equations

• instPartialOrderΛ A = CellularAlgebra.Λ_order

instance instLEΛ {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] : LE (CellularAlgebra.Λ k A)

Equations

• instLEΛ A = CellularAlgebra.Λ_order.toLE

instance instLTΛ {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] : LT (CellularAlgebra.Λ k A)

Equations

• instLTΛ A = CellularAlgebra.Λ_order.toLT

instance instInhabitedTableau {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : CellularAlgebra.Λ k A) : Inhabited (CellularAlgebra.tableau μ)

Equations

• instInhabitedTableau A μ = CellularAlgebra.inhabited_tableau μ

instance instFintypeSigmaΛProdTableau {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] : Fintype ((μ : CellularAlgebra.Λ k A) × CellularAlgebra.tableau μ × CellularAlgebra.tableau μ)

Equations

• instFintypeSigmaΛProdTableau A = inferInstanceAs (Fintype ((μ : CellularAlgebra.Λ k A) × CellularAlgebra.tableau μ × CellularAlgebra.tableau μ))

def CellularAlgebra.tableau_span {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (S : Set (Λ k A)) : Submodule k A

The subspace of $A$ spanned by the basis elements corresponding to tableaux of weights in a set $S$.

Equations

• CellularAlgebra.tableau_span A S = (CellularAlgebra.c over S)

Unfolding some linear maps

Some of the conditions on cellular algebras in the definition are written in terms of the basis elements but have obvious extensions to the entire algebra.

noncomputable def CellularAlgebra.r {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) : tableau μ → tableau μ → A →ₗ[k] k

The multiplication map r_basis extended to all of A by linearity.

Equations

• CellularAlgebra.r A μ s t = (CellularAlgebra.c.constr k) fun (b : (μ : CellularAlgebra.Λ k A) × CellularAlgebra.tableau μ × CellularAlgebra.tableau μ) => CellularAlgebra.r_basis b μ s t

theorem CellularAlgebra.multiplication_rule {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (a : A) (μ : Λ k A) (s t : tableau μ) : a * c ⟨μ, (s, t)⟩ ≡ ∑ u : tableau μ, (r A μ s u) a • c ⟨μ, (u, t)⟩ [SMOD tableau_span A {ν : Λ k A | ν < μ}]

The key requirement for cellular algebras.

This is the extension of CellularAlgebra.multiplication_rule_basis to all of A by linearity.

def CellularAlgebra.tableau_span_mono {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (S₁ S₂ : Set (Λ k A)) (h : S₁ ⊆ S₂) : tableau_span A S₁ ≤ tableau_span A S₂

Increasing the set of weights increases the span.

Equations

• ⋯ = ⋯

def CellularAlgebra.tableau_span_mono' {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (S₁ S₂ : Set (Λ k A)) (h : S₁ ⊂ S₂) : tableau_span A S₁ < tableau_span A S₂

The span of a strictly smaller set of weights is strictly smaller.

Equations

• ⋯ = ⋯

theorem CellularAlgebra.c_injective {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} {s₁ t₁ s₂ t₂ : tableau μ} (h : c ⟨μ, (s₁, t₁)⟩ = c ⟨μ, (s₂, t₂)⟩) : s₁ = s₂ ∧ t₁ = t₂

theorem CellularAlgebra.r_of_id {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} {s u : tableau μ} : (r A μ s u) 1 = if s = u then 1 else 0

theorem CellularAlgebra.r_of_zero {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} {s u : tableau μ} : (r A μ s u) 0 = 0

theorem CellularAlgebra.action_doesnt_increase_μ {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (a : A) (μ : Λ k A) (s t : tableau μ) : a * c ⟨μ, (s, t)⟩ ∈ tableau_span A {ν : Λ k A | ν ≤ μ}

def CellularAlgebra.cellular_ideal {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) : Submodule A A

Equations

• (A[≤μ]) = { carrier := ↑(CellularAlgebra.tableau_span A {ν : CellularAlgebra.Λ k A | ν ≤ μ}), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def CellularAlgebra.«term_[≤_]» : Lean.TrailingParserDescr

Equations

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

def CellularAlgebra.subcelluar_ideal {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) : Submodule A A

Equations

• (A[<μ]) = { carrier := ↑(CellularAlgebra.tableau_span A {ν : CellularAlgebra.Λ k A | ν < μ}), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

def CellularAlgebra.«term_[<_]» : Lean.TrailingParserDescr

Equations

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

The involution

noncomputable def CellularAlgebra.ι {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] : A →ₗ[k] A

Equations

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

@[simp]

theorem CellularAlgebra.ι_on_basis {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) (s t : tableau μ) : (ι A) (c ⟨μ, (s, t)⟩) = c ⟨μ, (t, s)⟩

theorem CellularAlgebra.ι_involution {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] : Function.Involutive ⇑(ι A)

Cellular algebras are equipped with an involution, which is the linear map that swaps the two tableaux in the basis elements.

theorem CellularAlgebra.ι_antiinvolution' {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (a b : A) : (ι A) (a * b) = (ι A) b * (ι A) a

@[simp]

theorem CellularAlgebra.ι_on_basis_product {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) (s t : tableau μ) (ν : Λ k A) (u v : tableau ν) : (ι A) (c ⟨μ, (s, t)⟩ * c ⟨ν, (u, v)⟩) = c ⟨ν, (v, u)⟩ * c ⟨μ, (t, s)⟩

theorem CellularAlgebra.subcellular_preserved_by_ι {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} : tableau_span A {ν : Λ k A | ν < μ} ≤ Submodule.comap (ι A) (tableau_span A {ν : Λ k A | ν < μ})

The basis c modulo cellular ideals

The key fact about the cellular basis, is that it respects the ordering of the cellular weights. That is, each cellular ideal $A^{≤\mu}$, taken modulo the smaller ideal $A^{<\mu}$, has a basis given by the elements $c^\mu_{s, t}$ for $s, t$ tableaux of shape $\mu$.

theorem CellularAlgebra.left_basis_mod_lesser_linear_indep {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} {t : tableau μ} : LinearIndependent k ((⇑A[<μ].mkQ ∘ ⇑c) ∘ fun (x : tableau μ) => ⟨μ, (x, t)⟩)

The set of basis vectors $\{c^\mu_{s,t} : s ∈ M(μ)\}$ is linearly independent modulo $A^{<\mu}$.

theorem CellularAlgebra.left_basis_sum_mod_lesser {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} {t : tableau μ} {f₁ f₂ : tableau μ → k} : ∑ u : tableau μ, f₁ u • c ⟨μ, (u, t)⟩ ≡ ∑ u : tableau μ, f₂ u • c ⟨μ, (u, t)⟩ [SMOD A[<μ]] → f₁ = f₂

If $\sum_{s} f₁(s) c^\mu_{s,t} ≡ \sum_{s} f₂(s) c^\mu_{s,t}$ modulo $A^{<\mu}$, then $f₁ = f₂$.

theorem CellularAlgebra.right_basis_mod_lesser_linear_indep {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} {s : tableau μ} : LinearIndependent k ((⇑A[<μ].mkQ ∘ ⇑c) ∘ fun (x : tableau μ) => ⟨μ, (s, x)⟩)

The set of basis vectors $\{c^\mu_{s,t} : t ∈ M(μ)\}$ is linearly independent modulo $A^{<\mu}$.

theorem CellularAlgebra.right_basis_sum_mod_lesser {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} {s : tableau μ} {f₁ f₂ : tableau μ → k} : ∑ u : tableau μ, f₁ u • c ⟨μ, (s, u)⟩ ≡ ∑ u : tableau μ, f₂ u • c ⟨μ, (s, u)⟩ [SMOD A[<μ]] → f₁ = f₂

If $\sum_{t} f₁(t) c^\mu_{s,t} ≡ \sum_{t} f₂(t) c^\mu_{s,t}$ modulo $A^{<\mu}$, then $f₁ = f₂$.

theorem CellularAlgebra.basis_mod_lesser_linear_indep {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} : LinearIndependent k ((⇑A[<μ].mkQ ∘ ⇑c) ∘ fun (x : tableau μ × tableau μ) => ⟨μ, x⟩)

The set of basis vectors $\{c^\mu_{s,t} : s, t ∈ M(μ)\}$ is linearly independent modulo $A^{<\mu}$.

theorem CellularAlgebra.basis_sum_mod_lesser {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} {f₁ f₂ : tableau μ → tableau μ → k} : ∑ s : tableau μ, ∑ t : tableau μ, f₁ s t • c ⟨μ, (s, t)⟩ ≡ ∑ s : tableau μ, ∑ t : tableau μ, f₂ s t • c ⟨μ, (s, t)⟩ [SMOD A[<μ]] → f₁ = f₂

If $\sum_{s, t} f₁(s, t) c^\mu_{s,t} ≡ \sum_{s, t} f₂(s, t) c^\mu_{s,t}$ modulo $A^{<\mu}$, then $f₁ = f₂$.

theorem CellularAlgebra.basis_cross_sum {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} {s t : tableau μ} (f g : tableau μ → k) : ∑ u : tableau μ, f u • c ⟨μ, (s, u)⟩ ≡ ∑ v : tableau μ, g v • c ⟨μ, (v, t)⟩ [SMOD A[<μ]] → f = ⇑(Finsupp.single t (g s))

If $\um_{u} f(u) c^\mu_{s,u} = \sum_{v} g(v) c^\mu_{v,t}$ modulo $A^{<\mu}$, then $f(u) = \begin{cases} g(s)& u=t\\ 0\text{else}\end{cases}$.

The r map

theorem CellularAlgebra.r_on_basis {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) (s t u v w : tableau μ) : (r A μ u w) (c ⟨μ, (s, t)⟩) = (Finsupp.single s ((r A μ t v) (c ⟨μ, (v, u)⟩))) w

theorem CellularAlgebra.r_on_basis_zero {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) (s t u v w : tableau μ) (h₁ : s ≠ w) : (r A μ u w) (c ⟨μ, (s, t)⟩) = 0

theorem CellularAlgebra.r_on_basis_symmetry {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) (s t u v : tableau μ) : (r A μ u s) (c ⟨μ, (s, t)⟩) = (r A μ t v) (c ⟨μ, (v, u)⟩)

theorem CellularAlgebra.r_of_mul {k : Type} [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (a₁ a₂ : A) (μ : Λ k A) (s t u : tableau μ) : (r A μ s u) (a₁ * a₂) = ∑ x : tableau μ, (r A μ s x) a₂ * (r A μ x u) a₁

Cell modules

def CellularAlgebra.cell_module (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) : Type

A cell module can be thought of as being build on the basis of tableaux

Equations

• CellularAlgebra.cell_module k A μ = (CellularAlgebra.tableau μ →₀ k)

noncomputable instance CellularAlgebra.instAddCommGroupCell_module (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} : AddCommGroup (cell_module k A μ)

Equations

• CellularAlgebra.instAddCommGroupCell_module k A = inferInstanceAs (AddCommGroup (CellularAlgebra.tableau μ →₀ k))

noncomputable instance CellularAlgebra.instModuleCell_module (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} : Module k (cell_module k A μ)

Equations

• CellularAlgebra.instModuleCell_module k A = inferInstanceAs (Module k (CellularAlgebra.tableau μ →₀ k))

noncomputable def CellularAlgebra.cell_module_basis (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) : Module.Basis (tableau μ) k (cell_module k A μ)

Equations

• CellularAlgebra.cell_module_basis k A μ = { repr := LinearEquiv.refl k (CellularAlgebra.tableau μ →₀ k) }

noncomputable instance CellularAlgebra.cellular_action (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} : SMul A (cell_module k A μ)

Equations

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

def CellularAlgebra.cellular_action_is (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} (a : A) (x : cell_module k A μ) : a • x = (((cell_module_basis k A μ).constr k) fun (s : tableau μ) => ∑ u : tableau μ, (r A μ s u) a • (cell_module_basis k A μ) u) x

Equations

• ⋯ = ⋯

noncomputable instance CellularAlgebra.cell_module_module (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) : Module A (cell_module k A μ)

Equations

• CellularAlgebra.cell_module_module k A μ = { toSMul := CellularAlgebra.cellular_action k A, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def CellularAlgebra.cell_module_form (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} : cell_module k A μ →ₗ[k] cell_module k A μ →ₗ[k] k

Equations

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

def CellularAlgebra.cell_module_form_contravariant (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) (a : A) (x y : cell_module k A μ) : ((cell_module_form k A) (a • x)) y = ((cell_module_form k A) x) ((ι A) a • y)

Equations

• ⋯ = ⋯

def CellularAlgebra.cell_module_radical (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) : Submodule A (cell_module k A μ)

Equations

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

def CellularAlgebra.simple_module (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) : Type

Equations

• CellularAlgebra.simple_module k A μ = (CellularAlgebra.cell_module k A μ ⧸ CellularAlgebra.cell_module_radical k A μ)

instance CellularAlgebra.instAddCommGroupSimple_module (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} : AddCommGroup (simple_module k A μ)

Equations

• CellularAlgebra.instAddCommGroupSimple_module k A = sorry

instance CellularAlgebra.instModuleSimple_module (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] {μ : Λ k A} : Module A (simple_module k A μ)

Equations

• CellularAlgebra.instModuleSimple_module k A = sorry

theorem CellularAlgebra.simple_module_simple (k : Type) [Field k] (A : Type) [Ring A] [Algebra k A] [cellular : CellularAlgebra k A] (μ : Λ k A) : IsSimpleModule A (simple_module k A μ)