structure KLRW.SimpleDigraph (V : Type u_1) extends Digraph V : Type u_1

• Adj : V → V → Prop
• loopless (x : V) : ¬self.Adj x x

inductive KLRW.StrandColor : Type

• red : StrandColor
• black : StrandColor

@[implicit_reducible]

instance KLRW.instDecidableEqStrandColor : DecidableEq StrandColor

Equations

• KLRW.instDecidableEqStrandColor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KLRW.instFintypeStrandColor : Fintype StrandColor

Equations

• KLRW.instFintypeStrandColor = { elems := { val := ↑KLRW.StrandColor.enumList, nodup := KLRW.StrandColor.enumList_nodup }, complete := KLRW.instFintypeStrandColor._proof_1 }

structure KLRW.KLRWStructure (V : Type u_1) : Type u_1

• Γ : SimpleDigraph V
• BlackStrands : V → ℕ
• RedStrands : V → ℕ

structure KLRW.StrandData (V : Type u_1) : Type u_1

• label : V
• color : StrandColor

@[implicit_reducible]

instance KLRW.instDecidableEqStrandData {V✝ : Type u_1} [DecidableEq V✝] : DecidableEq (StrandData V✝)

Equations

• KLRW.instDecidableEqStrandData = KLRW.instDecidableEqStrandData.decEq

def KLRW.instDecidableEqStrandData.decEq {V✝ : Type u_1} [DecidableEq V✝] (x✝ x✝¹ : StrandData V✝) : Decidable (x✝ = x✝¹)

Equations

• KLRW.instDecidableEqStrandData.decEq { label := a, color := a_1 } { label := b, color := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def KLRW.numColor {V : Type u_1} [DecidableEq V] {m : ℕ} (v : Vector (StrandData V) m) (k : V) (c : StrandColor) : ℕ

Equations

• KLRW.numColor v k c = (List.filter (fun (p : KLRW.StrandData V) => p.label == k && p.color == c) v.toList).length

@[reducible, inline]

abbrev KLRW.numBlack {V : Type u_1} [DecidableEq V] {m : ℕ} (v : Vector (StrandData V) m) (k : V) : ℕ

Equations

• KLRW.numBlack v k = KLRW.numColor v k KLRW.StrandColor.black

@[reducible, inline]

abbrev KLRW.numRed {V : Type u_1} [DecidableEq V] {m : ℕ} (v : Vector (StrandData V) m) (k : V) : ℕ

Equations

• KLRW.numRed v k = KLRW.numColor v k KLRW.StrandColor.red

@[reducible, inline]

abbrev KLRW.totalStrands {V : Type u_1} [Fintype V] (parameters : KLRWStructure V) : ℕ

Equations

• KLRW.totalStrands parameters = ∑ v : V, (parameters.BlackStrands v + parameters.RedStrands v)

structure KLRW.KLRWObject {V : Type u_1} [DecidableEq V] [Fintype V] (parameters : KLRWStructure V) : Type u_1

• strandSeq : Vector (StrandData V) (totalStrands parameters)
• corr_num_black (i : V) : parameters.BlackStrands i = numBlack self.strandSeq i
• corr_num_red (i : V) : parameters.RedStrands i = numRed self.strandSeq i

@[reducible, inline]

abbrev KLRW.KLRWObject.get {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} (M : KLRWObject parameters) (i : Fin (totalStrands parameters)) : StrandData V

Equations

• M.get i = M.strandSeq.get i

inductive KLRW.StrandGenerator {V : Type u_1} [DecidableEq V] [Fintype V] (parameters : KLRWStructure V) : Type u_1

• dot {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} : KLRWObject parameters → Fin (totalStrands parameters) → StrandGenerator parameters
• cross {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} : KLRWObject parameters → Fin (totalStrands parameters - 1) → StrandGenerator parameters
• idem {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} : KLRWObject parameters → StrandGenerator parameters

def KLRW.StrandGenerator.domain {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} (gen : StrandGenerator parameters) : KLRWObject parameters

Equations

• (KLRW.StrandGenerator.dot M a).domain = M
• (KLRW.StrandGenerator.cross M a).domain = M
• (KLRW.StrandGenerator.idem M).domain = M

theorem KLRW.toList_eq_ofFn {α : Type u_2} {n : ℕ} (v : Vector α n) : v.toList = List.ofFn v.get

theorem KLRW.filter_perm_length_eq {α : Type u_2} {n : ℕ} (v : Vector α n) (e : Equiv.Perm (Fin n)) (p : α → Bool) : (List.filter p (Vector.ofFn fun (k : Fin n) => v.get (e k)).toList).length = (List.filter p v.toList).length

def KLRW.adjSwap {n : ℕ} (i : Fin (n - 1)) : Equiv.Perm (Fin n)

Equations

• KLRW.adjSwap i = Equiv.swap ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩

def KLRW.afterCross {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) : KLRWObject parameters

Equations

• KLRW.afterCross M i = { strandSeq := Vector.ofFn fun (k : Fin (KLRW.totalStrands parameters)) => M.get ((KLRW.adjSwap i) k), corr_num_black := ⋯, corr_num_red := ⋯ }

def KLRW.StrandGenerator.codomain {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} (gen : StrandGenerator parameters) : KLRWObject parameters

Equations

• (KLRW.StrandGenerator.dot M a).codomain = M
• (KLRW.StrandGenerator.cross M a).codomain = KLRW.afterCross M a
• (KLRW.StrandGenerator.idem M).codomain = M

@[reducible, inline]

abbrev KLRW.KLRWFreeAlg {V : Type u_1} [DecidableEq V] [Fintype V] (R : Type u_2) [CommRing R] (parameters : KLRWStructure V) : Type (max u_2 u_1)

Equations

• KLRW.KLRWFreeAlg R parameters = FreeAlgebra (MvPolynomial (Fin 2) R) (KLRW.StrandGenerator parameters)

@[implicit_reducible]

instance KLRW.instFintypeStrandDataOfDecidableEq (V : Type u_2) [Fintype V] [DecidableEq V] : Fintype (StrandData V)

Equations

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

@[implicit_reducible]

instance KLRW.instFintypeVectorStrandDataOfDecidableEq (V : Type u_2) [Fintype V] [DecidableEq V] (n : ℕ) : Fintype (Vector (StrandData V) n)

Equations

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

@[implicit_reducible]

noncomputable instance KLRW.instFintypeKLRWObject {V : Type u_1} [DecidableEq V] [Fintype V] (parameters : KLRWStructure V) : Fintype (KLRWObject parameters)

Equations

• KLRW.instFintypeKLRWObject parameters = Fintype.ofInjective (fun (X : KLRW.KLRWObject parameters) => X.strandSeq) ⋯

inductive KLRW.KLRWImplicitConRel {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] : KLRWFreeAlg R parameters → KLRWFreeAlg R parameters → Prop

• dot_on_red {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters)) : (M.get i).color = StrandColor.red → KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M i)) 0
• cross_two_red {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) : (M.get ⟨↑i, ⋯⟩).color = StrandColor.red → (M.get ⟨↑i + 1, ⋯⟩).color = StrandColor.red → KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) 0
• bad_comp {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (f g : StrandGenerator parameters) : f.codomain ≠ g.domain → KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) g * FreeAlgebra.ι (MvPolynomial (Fin 2) R) f) 0
• idem_left {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (g : StrandGenerator parameters) : g.domain = M → KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.idem M) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) g) (FreeAlgebra.ι (MvPolynomial (Fin 2) R) g)
• idem_right {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (g : StrandGenerator parameters) : g.codomain = M → KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) g * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.idem M)) (FreeAlgebra.ι (MvPolynomial (Fin 2) R) g)
• id_sum {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] : KLRWImplicitConRel (∑ M : KLRWObject parameters, FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.idem M)) 1
• cross_cross_comm {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i j : Fin (totalStrands parameters - 1)) : dist ↑i ↑j > 1 → KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross (afterCross M i) j) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross (afterCross M i) i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M j))
• dot_dot_comm {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i j : Fin (totalStrands parameters)) : KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M j) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M i)) (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M j))
• cross_dot_far_comm {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) (j : Fin (totalStrands parameters)) : (↑j != ↑i) = true → (↑j != ↑i + 1) = true → KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M j) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M j))
• cross_dot_diff_index_comm {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) (j : Fin (totalStrands parameters)) : (M.get ⟨↑i, ⋯⟩).label ≠ (M.get ⟨↑i + 1, ⋯⟩).label → KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M j) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M j))
• cross_dot_red_comm {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) (j : Fin (totalStrands parameters)) : (M.get ⟨↑i, ⋯⟩).color = StrandColor.red → KLRWImplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M j) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M j))

@[reducible, inline]

noncomputable abbrev KLRW.uVar {R : Type u_2} [CommRing R] : MvPolynomial (Fin 2) R

Equations

• KLRW.uVar = MvPolynomial.X 0

@[reducible, inline]

noncomputable abbrev KLRW.ℏ {R : Type u_2} [CommRing R] : MvPolynomial (Fin 2) R

Equations

• KLRW.ℏ = MvPolynomial.X 1

@[reducible, inline]

noncomputable abbrev KLRW.poly {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (p : MvPolynomial (Fin 2) R) : KLRWFreeAlg R parameters

Equations

• KLRW.poly p = (algebraMap (MvPolynomial (Fin 2) R) (KLRW.KLRWFreeAlg R parameters)) p

inductive KLRW.KLRWExplicitConRel {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] : KLRWFreeAlg R parameters → KLRWFreeAlg R parameters → Prop

• bigon {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) : (M.get ⟨↑i, ⋯⟩).label = (M.get ⟨↑i + 1, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).color = StrandColor.black → (M.get ⟨↑i + 1, ⋯⟩).color = StrandColor.black → KLRWExplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) 0
• bigon_for_j_to_i {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) : parameters.Γ.Adj (M.get ⟨↑i, ⋯⟩).label (M.get ⟨↑i + 1, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).color = StrandColor.black → (M.get ⟨↑i + 1, ⋯⟩).color = StrandColor.black → KLRWExplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) (poly uVar * (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M ⟨↑i + 1, ⋯⟩) - FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M ⟨↑i, ⋯⟩)))
• bigon_with_red_left {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) : (M.get ⟨↑i, ⋯⟩).label = (M.get ⟨↑i + 1, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).color = StrandColor.red → (M.get ⟨↑i + 1, ⋯⟩).color = StrandColor.black → KLRWExplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) (poly uVar * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M ⟨↑i + 1, ⋯⟩))
• bigon_with_red_right {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) : (M.get ⟨↑i, ⋯⟩).label = (M.get ⟨↑i + 1, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).color = StrandColor.black → (M.get ⟨↑i + 1, ⋯⟩).color = StrandColor.red → KLRWExplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) (poly uVar * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M ⟨↑i, ⋯⟩))
• braid_with_neighbor {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 2)) : parameters.Γ.Adj (M.get ⟨↑i + 1, ⋯⟩).label (M.get ⟨↑i, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).label = (M.get ⟨↑i + 2, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).color = StrandColor.black → (M.get ⟨↑i + 1, ⋯⟩).color = StrandColor.black → (M.get ⟨↑i + 2, ⋯⟩).color = StrandColor.black → KLRWExplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i + 1, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i, ⋯⟩) - FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i + 1, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i + 1, ⋯⟩)) (poly uVar * poly ℏ * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.idem M))
• braid_with_red {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 2)) : (M.get ⟨↑i + 1, ⋯⟩).label = (M.get ⟨↑i, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).label = (M.get ⟨↑i + 2, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).color = StrandColor.black → (M.get ⟨↑i + 1, ⋯⟩).color = StrandColor.red → (M.get ⟨↑i + 2, ⋯⟩).color = StrandColor.black → KLRWExplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i + 1, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i, ⋯⟩) - FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i + 1, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M ⟨↑i + 1, ⋯⟩)) (poly uVar * poly ℏ * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.idem M))
• dot_pass_cross {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) : (M.get ⟨↑i, ⋯⟩).label = (M.get ⟨↑i + 1, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).color = StrandColor.black → (M.get ⟨↑i + 1, ⋯⟩).color = StrandColor.black → KLRWExplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot (afterCross M i) ⟨↑i, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) - FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M ⟨↑i + 1, ⋯⟩)) (poly ℏ * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.idem M))
• dot_pass_cross_2 {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} {R : Type u_2} [CommRing R] (M : KLRWObject parameters) (i : Fin (totalStrands parameters - 1)) : (M.get ⟨↑i, ⋯⟩).label = (M.get ⟨↑i + 1, ⋯⟩).label → (M.get ⟨↑i, ⋯⟩).color = StrandColor.black → (M.get ⟨↑i + 1, ⋯⟩).color = StrandColor.black → KLRWExplicitConRel (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot M ⟨↑i, ⋯⟩) - FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.dot (afterCross M i) ⟨↑i + 1, ⋯⟩) * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.cross M i)) (poly ℏ * FreeAlgebra.ι (MvPolynomial (Fin 2) R) (StrandGenerator.idem M))

noncomputable def KLRW.KLRWRel {V : Type u_1} [DecidableEq V] [Fintype V] (R : Type u_3) [CommRing R] (parameters : KLRWStructure V) : RingCon (KLRWFreeAlg R parameters)

Equations

• KLRW.KLRWRel R parameters = ringConGen fun (x y : KLRW.KLRWFreeAlg R parameters) => KLRW.KLRWImplicitConRel x y ∨ KLRW.KLRWExplicitConRel x y

@[reducible, inline]

abbrev KLRW.KLRWAlg {V : Type u_1} [DecidableEq V] [Fintype V] (R : Type u_3) [CommRing R] (parameters : KLRWStructure V) : Type (max u_1 u_3)

Equations

• KLRW.KLRWAlg R parameters = (KLRW.KLRWRel R parameters).Quotient

noncomputable def KLRW.idem_morph {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} (R : Type u_3) [CommRing R] (X : KLRWObject parameters) : KLRWAlg R parameters

Equations

• KLRW.idem_morph R X = (KLRW.KLRWRel R parameters).mk' (FreeAlgebra.ι (MvPolynomial (Fin 2) R) (KLRW.StrandGenerator.idem X))

noncomputable def KLRW.KLRWHom {V : Type u_1} [DecidableEq V] [Fintype V] {parameters : KLRWStructure V} (R : Type u_3) [CommRing R] (X Y : KLRWObject parameters) : Submodule R (KLRWAlg R parameters)

Equations

• KLRW.KLRWHom R X Y = (LinearMap.mulLeft R (KLRW.idem_morph R Y) ∘ₗ LinearMap.mulRight R (KLRW.idem_morph R X)).range