@[reducible, inline]

abbrev AInfinityTheory.Parity : Type

Equations

• AInfinityTheory.Parity = ZMod 2

class AInfinityTheory.Grading (β : Type u) extends AddCommGroup β : Type u

• add : β → β → β
• add_assoc (a b c : β) : a + b + c = a + (b + c)
• zero : β
• zero_add (a : β) : 0 + a = a
• add_zero (a : β) : a + 0 = a
• nsmul : ℕ → β → β
• nsmul_zero (x : β) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : β) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : β → β
• sub : β → β → β
• sub_eq_add_neg (a b : β) : a - b = a + -b
• zsmul : ℤ → β → β
• zsmul_zero' (a : β) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : β) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : β) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : β) : -a + a = 0
• add_comm (a b : β) : a + b = b + a
• ofInt : ℤ →+ β
• sign : β →+ Parity
• sign_ofInt (n : ℤ) : sign (ofInt n) = ↑n

def AInfinityTheory.shift_ofInt {β : Type u_1} [Grading β] (n : ℤ) : β

Equations

• AInfinityTheory.shift_ofInt n = AInfinityTheory.Grading.ofInt n

@[reducible, inline]

abbrev AInfinityTheory.GradedRModule {β : Type v} (R : Type u) [CommRing R] : Type (max v (u + 1))

Equations

• AInfinityTheory.GradedRModule R = CategoryTheory.GradedObject β (ModuleCat R)

class AInfinityTheory.RLinearGQuiver {β : Type v} (R : Type u) [CommRing R] (Obj : Type w) : Type (max (max (u + 1) v) w)

The graded R-module of morphisms between two objects.

• Hom : Obj → Obj → GradedRModule R