Atlas.TensorCategories.code.GrothendieckRing

source

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

↑(R.N R.unit j k) = if j = k then 1 else 0

Integer-valued version of the fusion ring unit-left-multiplication axiom.

source

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

↑(R.N i R.unit k) = if i = k then 1 else 0

Integer-valued version of the fusion ring unit-right-multiplication axiom.

source

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

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

Integer-valued version of the associativity identity for fusion coefficients.

source

def FusionRing.GrRing (ι : Type u_2) [DecidableEq ι] [Fintype ι] :

Type u_2

The underlying integer-valued function space ι → ℤ of the Grothendieck ring on basis ι. Elements are interpreted as formal ℤ-linear combinations of basis vectors.

Instances For

source

def FusionRing.grMul {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (f g : GrRing ι) :

GrRing ι

Multiplication on GrRing ι defined by the fusion structure constants N i j k, implementing X_i X_j = ∑_k N_{ij}^k X_k.

Instances For

source

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

GrRing ι

The multiplicative identity of GrRing ι: the indicator function of the unit basis element.

Instances For

source

theorem FusionRing.sum_ite_const_zero {α : Type u_2} [AddCommMonoid α] {ι' : Type u_3} {p : Prop} [Decidable p] (s : Finset ι') (f : ι' → α) :

(∑ x ∈ s, if p then f x else 0) = if p then ∑ x ∈ s, f x else 0

A sum of a constant if-expression equals the same if applied to the unconditional sum.

source

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

R.grMul R.grOne f = f

Left identity for grMul: the unit element acts as the multiplicative identity.

source

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

R.grMul f R.grOne = f

Right identity for grMul: the unit element acts as the multiplicative identity.

source

theorem FusionRing.inner_sum_eq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : FusionRing ι) (a b c : GrRing ι) (l i j k : ι) :

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

Auxiliary rearrangement used in the proof of associativity: rewriting the inner sum using the integer-valued associativity identity.

source

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

R.grMul (R.grMul a b) c = R.grMul a (R.grMul b c)

Associativity of grMul on GrRing ι, coming from the associativity of fusion coefficients (Lemma 1.16.1).

source

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

(R.grMul a fun (k : ι) => b k + c k) = fun (k : ι) => R.grMul a b k + R.grMul a c k

Left distributivity of grMul over pointwise addition.

source

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

R.grMul (fun (k : ι) => a k + b k) c = fun (k : ι) => R.grMul a c k + R.grMul b c k

Right distributivity of grMul over pointwise addition.

source

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

(R.grMul a fun (x : ι) => 0) = fun (x : ι) => 0

Multiplying by the zero function on the right yields zero.

source

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

R.grMul (fun (x : ι) => 0) a = fun (x : ι) => 0

Multiplying by the zero function on the left yields zero.

source

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

Type u_1

Bundled form of the Grothendieck ring of a fusion ring R: an element is identified with its integer-valued coefficient function on the basis.

coeff : ι → ℤ

Instances For

source

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

x = y ↔ x.coeff = y.coeff

source

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

x = y

source

@[implicit_reducible]

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

Zero R.GrRingOf

Zero element of GrRingOf R.

source

@[implicit_reducible]

instance FusionRing.GrRingOf.instOne {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

One R.GrRingOf

Multiplicative identity of GrRingOf R, given by R.grOne.

source

@[implicit_reducible]

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

Add R.GrRingOf

Pointwise addition on GrRingOf R.

source

@[implicit_reducible]

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

Neg R.GrRingOf

Pointwise negation on GrRingOf R.

source

@[implicit_reducible]

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

Sub R.GrRingOf

Pointwise subtraction on GrRingOf R.

source

@[implicit_reducible]

instance FusionRing.GrRingOf.instMul {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

Mul R.GrRingOf

Fusion multiplication on GrRingOf R.

source

@[implicit_reducible]

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

SMul ℕ R.GrRingOf

Pointwise ℕ-scalar multiplication on GrRingOf R.

source

@[implicit_reducible]

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

SMul ℤ R.GrRingOf

Pointwise ℤ-scalar multiplication on GrRingOf R.

source

@[implicit_reducible]

instance FusionRing.GrRingOf.instNatCast {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

NatCast R.GrRingOf

Embedding of ℕ into GrRingOf R as multiples of the unit basis element.

source

@[implicit_reducible]

instance FusionRing.GrRingOf.instIntCast {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

IntCast R.GrRingOf

Embedding of ℤ into GrRingOf R as multiples of the unit basis element.

source

@[simp]

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

coeff 0 k = 0

The coefficient of the zero element is zero.

source

@[simp]

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

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

Coefficients distribute over addition.

source

@[simp]

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

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

Coefficients distribute over negation.

source

@[simp]

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

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

Coefficients distribute over subtraction.

source

@[implicit_reducible]

instance FusionRing.GrRingOf.instRing {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : FusionRing ι} :

Ring R.GrRingOf

The Grothendieck ring GrRingOf R of a fusion ring R is a Ring.

source

def FusionRing.basisVec {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) :

GrRing ι

The basis vector indexed by i ∈ ι, given by the indicator function of {i}.

Instances For

source

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

basisVec R.unit = R.grOne

The basis vector at the unit equals the multiplicative identity grOne.

source

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

a * b * c = a * (b * c)

Associativity of multiplication in the Grothendieck ring, packaged at the bundled level.

source

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

a * b * c = a * (b * c)

Lemma 1.16.1: The multiplication on Gr(C) defined by fusion coefficients is associative.

source

structure FusionRing.FusionRingHom {ι : Type u_2} [DecidableEq ι] [Fintype ι] {κ : Type u_3} [DecidableEq κ] [Fintype κ] (R : FusionRing ι) (S : FusionRing κ) :

Type (max u_2 u_3)

A homomorphism of fusion rings, represented combinatorially by an integer matrix M on the bases satisfying unit-preservation and a fusion-multiplication identity.

M : ι → κ → ℤ
map_unit (l : κ) : self.M R.unit l = if l = S.unit then 1 else 0
map_mul (i j : ι) (l : κ) : ∑ k : ι, ↑(R.N i j k) * self.M k l = ∑ p : κ, ∑ q : κ, self.M i p * self.M j q * ↑(S.N p q l)

Instances For

source

def FusionRing.FusionRingHom.grMap {ι : Type u_2} [DecidableEq ι] [Fintype ι] {κ : Type u_3} [DecidableEq κ] [Fintype κ] {R : FusionRing ι} {S : FusionRing κ} (φ : R.FusionRingHom S) (f : GrRing ι) :

GrRing κ

The integer-valued action of a FusionRingHom on GrRing elements: linear extension of the matrix φ.M along the basis.

Instances For

source

theorem FusionRing.FusionRingHom.grMap_one {ι : Type u_2} [DecidableEq ι] [Fintype ι] {κ : Type u_3} [DecidableEq κ] [Fintype κ] {R : FusionRing ι} {S : FusionRing κ} (φ : R.FusionRingHom S) :

φ.grMap R.grOne = S.grOne

grMap sends the multiplicative identity of GrRing R to that of GrRing S.

source

theorem FusionRing.FusionRingHom.grMap_add {ι : Type u_2} [DecidableEq ι] [Fintype ι] {κ : Type u_3} [DecidableEq κ] [Fintype κ] {R : FusionRing ι} {S : FusionRing κ} (φ : R.FusionRingHom S) (f g : GrRing ι) :

(φ.grMap fun (k : ι) => f k + g k) = fun (l : κ) => φ.grMap f l + φ.grMap g l

grMap is additive in its function argument.

source

theorem FusionRing.FusionRingHom.grMap_mul {ι : Type u_2} [DecidableEq ι] [Fintype ι] {κ : Type u_3} [DecidableEq κ] [Fintype κ] {R : FusionRing ι} {S : FusionRing κ} (φ : R.FusionRingHom S) (f g : GrRing ι) :

φ.grMap (R.grMul f g) = S.grMul (φ.grMap f) (φ.grMap g)

grMap is multiplicative with respect to the fusion product on the source and target.

source

def FusionRing.FusionRingHom.inducedRingHom {ι : Type u_2} [DecidableEq ι] [Fintype ι] {κ : Type u_3} [DecidableEq κ] [Fintype κ] {R : FusionRing ι} {S : FusionRing κ} (φ : R.FusionRingHom S) :

R.GrRingOf →+* S.GrRingOf

The ring homomorphism GrRingOf R →+* GrRingOf S induced by a FusionRingHom.

Instances For

source

def repZ2 :

FusionRing (Fin 2)

The fusion ring of representations of ℤ/2, with basis Fin 2 and product given by addition modulo 2.

Instances For

source

theorem repZ2.mul_e1_e1 :

repZ2.grMul (FusionRing.basisVec 1) (FusionRing.basisVec 1) = FusionRing.basisVec 0

In Gr(Rep(ℤ/2)), the nontrivial sign object squares to the unit.