Atlas.TensorCategories.code.K0Bimodule

structure FusionRing.K0Group {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) :

The Grothendieck group K₀(R) of a fusion ring R, represented as integer-valued coefficient vectors indexed by the basis ι.

coeff : ι → ℤ

Instances For

source

theorem FusionRing.K0Group.ext_iff {ι : Type u_1} {inst✝ : DecidableEq ι} {inst✝¹ : Fintype ι} {R : FusionRing ι} {x y : R.K0Group} :

x = y ↔ x.coeff = y.coeff

source

theorem FusionRing.K0Group.ext {ι : Type u_1} {inst✝ : DecidableEq ι} {inst✝¹ : Fintype ι} {R : FusionRing ι} {x y : R.K0Group} (coeff : x.coeff = y.coeff) :

x = y

source

@[implicit_reducible]

instance FusionRing.K0Group.instZero {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

Zero R.K0Group

The zero element of K₀(R) is the all-zero coefficient vector.

source

@[implicit_reducible]

instance FusionRing.K0Group.instAdd {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

Add R.K0Group

Componentwise addition of elements of K₀(R).

source

@[implicit_reducible]

instance FusionRing.K0Group.instNeg {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

Neg R.K0Group

Componentwise negation on K₀(R).

source

@[implicit_reducible]

instance FusionRing.K0Group.instSub {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

Sub R.K0Group

Componentwise subtraction on K₀(R).

source

@[implicit_reducible]

instance FusionRing.K0Group.instSMulNat {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

SMul ℕ R.K0Group

Natural-number scalar multiplication on K₀(R), applied componentwise.

source

@[implicit_reducible]

instance FusionRing.K0Group.instSMulInt {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

SMul ℤ R.K0Group

Integer scalar multiplication on K₀(R), applied componentwise.

source

@[simp]

theorem FusionRing.K0Group.coeff_zero {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (k : ι) :

coeff 0 k = 0

Each coefficient of the zero element of K₀(R) is 0.

source

@[simp]

theorem FusionRing.K0Group.coeff_add {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (a b : R.K0Group) (k : ι) :

(a + b).coeff k = a.coeff k + b.coeff k

Addition on K₀(R) is computed componentwise.

source

@[simp]

theorem FusionRing.K0Group.coeff_neg {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (a : R.K0Group) (k : ι) :

(-a).coeff k = -a.coeff k

Negation on K₀(R) is componentwise.

source

@[simp]

theorem FusionRing.K0Group.coeff_sub {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (a b : R.K0Group) (k : ι) :

(a - b).coeff k = a.coeff k - b.coeff k

Subtraction on K₀(R) is computed componentwise.

source

@[implicit_reducible]

instance FusionRing.K0Group.instAddCommGroup {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

AddCommGroup R.K0Group

K₀(R) is an additive abelian group with componentwise operations.

source

def FusionRing.k0ActLeft {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (r p : ι → ℤ) :

ι → ℤ

Left action of the Grothendieck ring of R on K₀(R) in coefficient form, defined by (r ◃ p)_k = Σᵢⱼ rᵢ pⱼ N_{i* k j}.

Instances For

source

def FusionRing.k0ActRight {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (p r : ι → ℤ) :

ι → ℤ

Right action of the Grothendieck ring of R on K₀(R) in coefficient form, defined by (p ▹ r)_k = Σ_{a,j} pₐ rⱼ N_{k j* a}.

Instances For

source

theorem FusionRing.k0ActLeft_eq_grMul {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (r p : ι → ℤ) :

R.k0ActLeft r p = R.grMul r p

The left K₀-action coincides with multiplication in the Grothendieck ring Gr(R).

source

theorem FusionRing.k0ActRight_one {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (p : ι → ℤ) :

R.k0ActRight p R.grOne = p

The right action by the unit of Gr(R) is the identity.

source

theorem FusionRing.k0ActRight_add_left {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (p₁ p₂ r : ι → ℤ) :

R.k0ActRight (fun (k : ι) => p₁ k + p₂ k) r = fun (k : ι) => R.k0ActRight p₁ r k + R.k0ActRight p₂ r k

Additivity of the right action in the module argument.

source

theorem FusionRing.k0ActRight_add_right {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (p r₁ r₂ : ι → ℤ) :

(R.k0ActRight p fun (k : ι) => r₁ k + r₂ k) = fun (k : ι) => R.k0ActRight p r₁ k + R.k0ActRight p r₂ k

Additivity of the right action in the ring argument.

source

theorem FusionRing.k0ActRight_zero_left {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (r : ι → ℤ) :

R.k0ActRight (fun (x : ι) => 0) r = fun (x : ι) => 0

Right action of any ring element on the zero module element is zero.

source

theorem FusionRing.k0ActRight_zero_right {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (p : ι → ℤ) :

(R.k0ActRight p fun (x : ι) => 0) = fun (x : ι) => 0

Right action of the zero ring element on any module element is zero.

source

theorem FusionRing.star_eq_iff {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (a b : ι) :

a = R.star b ↔ b = R.star a

Symmetry of the duality involution star: a = b* iff b = a*.

source

theorem FusionRing.N_cyclic_star {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (i j k : ι) :

R.N i j (R.star k) = R.N j k (R.star i)

Cyclic symmetry of the structure constants under duality: N_{i j k*} = N_{j k i*}.

source

theorem FusionRing.N_star_triple {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (p j q : ι) :

R.N (R.star p) (R.star j) (R.star q) = R.N j p q

Star-equivariance of the structure constants: N_{p* j* q*} = N_{j p q}.

source

noncomputable def FusionRing.starEquiv {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) :

ι ≃ ι

The involutive duality on the index set viewed as a self-equivalence of ι.

Instances For

source

theorem FusionRing.sum_star_reparametrize {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (f : ι → ℤ) :

∑ m : ι, f m = ∑ q : ι, f (R.star q)

A sum over ι is invariant under reparametrization by the duality involution star.

source

theorem FusionRing.inner_sum_k0ActRight_assoc {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (a j p l : ι) :

∑ k : ι, ↑(R.N k (R.star j) a) * ↑(R.N l (R.star p) k) = ∑ q : ι, ↑(R.N j p q) * ↑(R.N l (R.star q) a)

Inner-sum identity used to prove associativity of the right K₀-action: rewrites a contraction over k in terms of a contraction over q via the cyclic identity.

source

theorem FusionRing.inner_sum_bimodule {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (a j i l : ι) :

∑ k : ι, ↑(R.N k (R.star j) a) * ↑(R.N i k l) = ∑ b : ι, ↑(R.N i a b) * ↑(R.N l (R.star j) b)

Inner-sum identity used to prove the bimodule compatibility: rewrites the contraction exchanging the roles of left and right action variables.

source

theorem FusionRing.k0ActRight_mul_assoc {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (m s r : ι → ℤ) :

R.k0ActRight (R.k0ActRight m s) r = R.k0ActRight m (R.grMul s r)

Associativity of the right K₀-action: (m ▹ s) ▹ r = m ▹ (s ⋆ r).

source

theorem FusionRing.k0_bimodule_compat {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (r m s : ι → ℤ) :

R.grMul r (R.k0ActRight m s) = R.k0ActRight (R.grMul r m) s

Bimodule compatibility: the left action by Gr(R) commutes with the right action, namely r ⋆ (m ▹ s) = (r ⋆ m) ▹ s.

source

@[implicit_reducible]

instance FusionRing.K0Group.instSMulLeft {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

SMul R.GrRingOf R.K0Group

Left action of the Grothendieck ring Gr(R) on K₀(R) via k0ActLeft.

source

@[simp]

theorem FusionRing.K0Group.smul_left_coeff {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (r : R.GrRingOf) (m : R.K0Group) (k : ι) :

(r • m).coeff k = R.k0ActLeft r.coeff m.coeff k

Coefficients of the left scalar product are computed by k0ActLeft.

source

@[implicit_reducible]

instance FusionRing.K0Group.instModule {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

Module R.GrRingOf R.K0Group

K₀(R) is a left module over the Grothendieck ring Gr(R).

source

@[implicit_reducible]

instance FusionRing.K0Group.instSMulRight {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

SMul R.GrRingOfᵐᵒᵖ R.K0Group

Right action of Gr(R)ᵐᵒᵖ on K₀(R) via k0ActRight.

source

@[simp]

theorem FusionRing.K0Group.smul_right_coeff {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} (r : R.GrRingOfᵐᵒᵖ) (m : R.K0Group) (k : ι) :

(r • m).coeff k = R.k0ActRight m.coeff (MulOpposite.unop r).coeff k

Coefficients of the right scalar product are computed by k0ActRight.

source

@[implicit_reducible]

instance FusionRing.K0Group.instModuleOp {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

Module R.GrRingOfᵐᵒᵖ R.K0Group

K₀(R) is a right module over the Grothendieck ring Gr(R), presented as a left module over Gr(R)ᵐᵒᵖ.

source

instance FusionRing.K0Group.instSMulCommClass {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

SMulCommClass R.GrRingOf R.GrRingOfᵐᵒᵖ R.K0Group

The left and right actions of the Grothendieck ring on K₀(R) commute, equipping it with a Gr(R)-bimodule structure.

source

theorem FusionRing.prop_1_47_1 {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) :

SMulCommClass R.GrRingOf R.GrRingOfᵐᵒᵖ R.K0Group

Proposition 1.47.1 (EGNO). For a fusion ring R, the Grothendieck group K₀(R) carries a canonical bimodule structure over the Grothendieck ring Gr(R).