structure AInfinityTheory.KLRWCategory (n : ℕ) (R : Type u) : Type

• positioning : Fin (n + 1)

@[implicit_reducible]

instance AInfinityTheory.instTexifyKLRWCategory {R : Type u} {n : ℕ} : Texify (KLRWCategory n R)

Equations

• AInfinityTheory.instTexifyKLRWCategory = { texify := fun (x : AInfinityTheory.KLRWCategory n R) => toString "T_{" ++ toString x.positioning ++ toString "}", requiresParentheses := false }

def AInfinityTheory.compShift {n : ℕ} {R : Type u} (X Y Z : KLRWCategory n R) : ℕ

Equations

• AInfinityTheory.compShift X Y Z = max ↑X.positioning ↑Y.positioning + max ↑Y.positioning ↑Z.positioning - max ↑X.positioning ↑Z.positioning - ↑Y.positioning

theorem AInfinityTheory.compShift_self_left {n : ℕ} {R : Type u} (X Y : KLRWCategory n R) : compShift X X Y = 0

theorem AInfinityTheory.compShift_self_right {n : ℕ} {R : Type u} (X Y : KLRWCategory n R) : compShift X Y Y = 0

theorem AInfinityTheory.compShift_assoc {n : ℕ} {R : Type u} (W X Y Z : KLRWCategory n R) : compShift W X Y + compShift W Y Z = compShift X Y Z + compShift W X Z

@[reducible, inline]

abbrev AInfinityTheory.StrandSpace (R : Type u) [CommRing R] : Type u

The free module generated by the strands with fixed channels. This is an abbrev because we want it to inherit the Module typeclass instance from DFinsupp.

Uses DFinsupp because Finsupp is not currently computable. See https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Finsupp.20noncomputability

Equations

• AInfinityTheory.StrandSpace R = Π₀ (x : ℕ), R

@[implicit_reducible]

instance AInfinityTheory.instTexifyStrandSpaceOfToString {R : Type u} [CommRing R] [DecidableEq R] [ToString R] : Texify (StrandSpace R)

Equations

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

def AInfinityTheory.instTexifyStrandSpaceOfToString.termString {R : Type u} [CommRing R] [DecidableEq R] [ToString R] (x : ℕ → R) (i : ℕ) : String

Equations

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

@[reducible, inline]

abbrev AInfinityTheory.StrandSpace.dots (R : Type u) [CommRing R] (n : ℕ) : StrandSpace R

Equations

• AInfinityTheory.StrandSpace.dots R n = fun₀ | n => 1

@[implicit_reducible]

instance AInfinityTheory.instCategoryKLRWCategory {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} : CategoryTheory.Category.{u, 0} (KLRWCategory n R)

Equations

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

@[implicit_reducible]

instance AInfinityTheory.instPreadditiveKLRWCategory {R : Type u} [CommRing R] [DecidableEq R] {n : ℕ} : CategoryTheory.Preadditive (KLRWCategory n R)

Equations

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

@[implicit_reducible]

instance AInfinityTheory.instTexifyHomKLRWCategoryOfToString (R : Type u_1) [CommRing R] [DecidableEq R] [ToString R] (n : ℕ) (S T : KLRWCategory n R) : Texify (S ⟶ T)

Equations

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

theorem AInfinityTheory.KLRWCategory.not_isZero (R : Type u_1) [CommRing R] [DecidableEq R] (n : ℕ) (A : KLRWCategory n R) : ¬CategoryTheory.Limits.IsZero A

The KLRW Category lacks zero objects

@[implicit_reducible]

instance AInfinityTheory.instDecidablePredKLRWCategoryIsZero (R : Type u_1) [CommRing R] [DecidableEq R] (n : ℕ) : DecidablePred CategoryTheory.Limits.IsZero

Equations

• AInfinityTheory.instDecidablePredKLRWCategoryIsZero R n A = isFalse ⋯

@[reducible, inline]

abbrev AInfinityTheory.AddKLRWCategory (n : ℕ) (R : Type u) [CommRing R] [DecidableEq R] : Type

Equations

• AInfinityTheory.AddKLRWCategory n R = CMat_ (AInfinityTheory.KLRWCategory n R)

@[reducible, inline]

abbrev AInfinityTheory.KLRWComplexCategory (n : ℕ) (R : Type u) [CommRing R] [DecidableEq R] : Type u

Equations

• AInfinityTheory.KLRWComplexCategory n R = BoundedCochainComplex (AInfinityTheory.AddKLRWCategory n R)