structure BraidingFunctorData (R : Type u) [CommRing R] [CharP R 2] [DecidableEq R] (n : ℕ) : Type u

• gen₀ : AInfinityTheory.KLRWCategory n R → BoundedCochainComplex (CMat_ (AInfinityTheory.KLRWCategory n R))
• gen₁ {A B : AInfinityTheory.KLRWCategory n R} : (A ⟶ B) → (self.gen₀ A ⟶ self.gen₀ B)
• gen₂ {A B C : AInfinityTheory.KLRWCategory n R} : (A ⟶ B) → (B ⟶ C) → (self.gen₀ A ⟶ (BoundedCochainComplex.shiftFunctor (-1)).obj (self.gen₀ C))

def BraidingFunctorData.add₀ {R : Type u} [CommRing R] [CharP R 2] [DecidableEq R] {n : ℕ} (β : BraidingFunctorData R n) (A : CMat_ (AInfinityTheory.KLRWCategory n R)) : BoundedCochainComplex (CMat_ (AInfinityTheory.KLRWCategory n R))

Equations

• β.add₀ A = sorry

def BraidingFunctorData.add₁ {R : Type u} [CommRing R] [CharP R 2] [DecidableEq R] {n : ℕ} (β : BraidingFunctorData R n) {A B : CMat_ (AInfinityTheory.KLRWCategory n R)} (f : A ⟶ B) : β.add₀ A ⟶ β.add₀ B

Equations

• β.add₁ f = sorry

def BraidingFunctorData.add₂ {R : Type u} [CommRing R] [CharP R 2] [DecidableEq R] {n : ℕ} (β : BraidingFunctorData R n) {A B C : CMat_ (AInfinityTheory.KLRWCategory n R)} (f : A ⟶ B) (g : B ⟶ C) : β.add₀ A ⟶ β.add₀ C

Equations

• β.add₂ f g = sorry

def BraidingFunctorData.full₀ {R : Type u} [CommRing R] [CharP R 2] [DecidableEq R] {n : ℕ} (β : BraidingFunctorData R n) (A : BoundedCochainComplex (CMat_ (AInfinityTheory.KLRWCategory n R))) : BoundedCochainComplex (CMat_ (AInfinityTheory.KLRWCategory n R))

Equations

• β.full₀ A = sorry

def BraidingFunctorData.full₁ {R : Type u} [CommRing R] [CharP R 2] [DecidableEq R] {n : ℕ} (β : BraidingFunctorData R n) {A B : BoundedCochainComplex (CMat_ (AInfinityTheory.KLRWCategory n R))} (f : A ⟶ B) : β.full₀ A ⟶ β.full₀ B

Equations

• β.full₁ f = sorry

def BraidingFunctorData.full₂ {R : Type u} [CommRing R] [CharP R 2] [DecidableEq R] {n : ℕ} (β : BraidingFunctorData R n) {A B C : BoundedCochainComplex (CMat_ (AInfinityTheory.KLRWCategory n R))} (f : A ⟶ B) (g : B ⟶ C) : β.full₀ A ⟶ β.full₀ C

Equations

• β.full₂ f g = sorry