Gradings for A-infinity categories

This file introduces graded hom spaces, R-linear graded quivers, and the grading data needed to write down A-infinity structures.

The grading type β of an A-infinity category is an abelian group of degrees. The A-infinity axioms only ever use two pieces of additional structure on it:

• integer degree shifts ℤ →+ β, so that the n-ary operation mₙ can have degree 2 - n;
• a Koszul sign character β →+ Additive ℤˣ, so that a degree d determines a sign (-1) ^ d.

They are compatible in that the differential, of degree shift 1, is odd.

No degree is ever multiplied, so β is not required to be a ring. This is what allows bigradings such as ℤ × ℤ or ℤ × ZMod 2, where mₙ has degree (2 - n, 0) and the sign is the total parity.

A homomorphism of grading types GradingHom β β', written β →+ᵍ β', is an additive homomorphism preserving the shifts and the signs. It translates degrees when an A-infinity functor changes the grading.

class AInfinityTheory.GradingType (β : Type u_1) [AddCommGroup β] : Type u_1

A grading type is an abelian group of degrees β together with a homomorphism shift : ℤ →+ β realising integer degree shifts (the n-ary operation mₙ has degree shift (2 - n)) and a Koszul sign character sign : β →+ Additive ℤˣ, such that the differential, of degree shift 1, is odd.

• shift : ℤ →+ β

  The integer degree shifts: mₙ has degree shift (2 - n).

• sign : β →+ Additive ℤˣ

  The Koszul sign character, written additively.

• sign_shift_one : sign (shift 1) = Additive.ofMul (-1)

  The differential has odd degree.

@[simp]

theorem AInfinityTheory.sign_shift {β : Type v} [AddCommGroup β] [GradingType β] (n : ℤ) : sign (shift n) = n.negOnePow

The sign of an integer degree shift is Mathlib's Int.negOnePow.

Instances

Global instances are provided only for the two standard gradings ℤ and ZMod 2. Product gradings are constructed by the named definitions prodFst and prodTotal below and must be activated locally, since both are reasonable choices on the same product type.

@[implicit_reducible]

instance AInfinityTheory.GradingType.instInt : GradingType ℤ

The integers, graded by themselves: the shift is the identity and the sign of n is (-1) ^ n.

Equations

• AInfinityTheory.GradingType.instInt = { shift := AddMonoidHom.id ℤ, sign := (zmultiplesHom (Additive ℤˣ)) (Additive.ofMul (-1)), sign_shift_one := AInfinityTheory.GradingType.instInt._proof_1 }

@[simp]

theorem AInfinityTheory.GradingType.shift_int (n : ℤ) : shift n = n

@[implicit_reducible]

instance AInfinityTheory.GradingType.instZModOfNatNat : GradingType (ZMod 2)

The parity grading ZMod 2: the shift is reduction modulo 2 and the sign of a parity p is (-1) ^ p, using Mathlib's power operation on ℤˣ by ZMod 2.

Equations

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

@[simp]

theorem AInfinityTheory.GradingType.shift_zmod_two (n : ℤ) : shift n = ↑n

@[reducible, inline]

abbrev AInfinityTheory.GradingType.prodFst (β : Type u_1) [AddCommGroup β] (γ : Type u_2) [AddCommGroup γ] [GradingType β] : GradingType (β × γ)

The product grading on β × γ whose shifts land in the first factor and whose sign is read off the first factor alone.

Equations

• AInfinityTheory.GradingType.prodFst β γ = { shift := (AddMonoidHom.inl β γ).comp AInfinityTheory.shift, sign := AInfinityTheory.sign.comp (AddMonoidHom.fst β γ), sign_shift_one := ⋯ }

@[simp]

theorem AInfinityTheory.GradingType.prodFst_shift (β : Type u_1) [AddCommGroup β] (γ : Type u_2) [AddCommGroup γ] [GradingType β] (n : ℤ) : shift n = (shift n, 0)

@[reducible, inline]

abbrev AInfinityTheory.GradingType.prodTotal (β : Type u_1) [AddCommGroup β] (γ : Type u_2) [AddCommGroup γ] [GradingType β] [GradingType γ] : GradingType (β × γ)

The product grading on β × γ whose shifts land in the first factor and whose sign is the product of the signs of both factors (the total sign).

Equations

• AInfinityTheory.GradingType.prodTotal β γ = { shift := (AddMonoidHom.inl β γ).comp AInfinityTheory.shift, sign := AInfinityTheory.sign.coprod AInfinityTheory.sign, sign_shift_one := ⋯ }

@[simp]

theorem AInfinityTheory.GradingType.prodTotal_shift (β : Type u_1) [AddCommGroup β] (γ : Type u_2) [AddCommGroup γ] [GradingType β] [GradingType γ] (n : ℤ) : shift n = (shift n, 0)

Koszul signs in the standard gradings

@[simp]

theorem AInfinityTheory.sign_int (n : ℤ) : sign n = n.negOnePow

theorem AInfinityTheory.sign_zmod_two (p : ZMod 2) : sign p = (-1) ^ p

In the parity grading, sign is Mathlib's power operation on ℤˣ by ZMod 2.

@[simp]

theorem AInfinityTheory.sign_prodFst (β : Type u_1) [AddCommGroup β] (γ : Type u_2) [AddCommGroup γ] [GradingType β] (d : β × γ) : sign d = sign d.1

@[simp]

theorem AInfinityTheory.sign_prodTotal (β : Type u_1) [AddCommGroup β] (γ : Type u_2) [AddCommGroup γ] [GradingType β] [GradingType γ] (d : β × γ) : sign d = sign d.1 + sign d.2

Homomorphisms of grading types

structure AInfinityTheory.GradingHom (β : Type u_1) (β' : Type u_2) [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] extends β →+ β' : Type (max u_1 u_2)

A homomorphism of grading types is an additive homomorphism β →+ β' that preserves the integer degree shifts and the Koszul signs. It translates degrees in β into degrees in β' so that mₙ keeps degree shift (2 - n) and every Koszul sign is unchanged; for example, reduction ℤ → ZMod 2, or the inclusion of β into the product grading prodFst β γ.

• toFun : β → β'
• map_zero' : (↑self.toAddMonoidHom).toFun 0 = 0
• map_add' (x y : β) : (↑self.toAddMonoidHom).toFun (x + y) = (↑self.toAddMonoidHom).toFun x + (↑self.toAddMonoidHom).toFun y
• map_shift' (k : ℤ) : (↑self.toAddMonoidHom).toFun (shift k) = shift k

  The homomorphism preserves the integer degree shifts.

• map_sign' (b : β) : sign ((↑self.toAddMonoidHom).toFun b) = sign b

  The homomorphism preserves the Koszul signs.

def AInfinityTheory.«term_→+ᵍ_» : Lean.TrailingParserDescr

β →+ᵍ β' denotes the type of homomorphisms of grading types from β to β'.

Equations

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

@[implicit_reducible]

instance AInfinityTheory.GradingHom.instFunLike {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] : FunLike (β →+ᵍ β') β β'

A homomorphism of grading types is applied to degrees through its underlying function.

Equations

• AInfinityTheory.GradingHom.instFunLike = { coe := fun (f : β →+ᵍ β') => (↑f.toAddMonoidHom).toFun, coe_injective' := ⋯ }

instance AInfinityTheory.GradingHom.instAddMonoidHomClass {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] : AddMonoidHomClass (β →+ᵍ β') β β'

A homomorphism of grading types is in particular an additive homomorphism.

@[simp]

theorem AInfinityTheory.GradingHom.coe_toAddMonoidHom {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] (f : β →+ᵍ β') : ⇑f.toAddMonoidHom = ⇑f

@[simp]

theorem AInfinityTheory.GradingHom.coe_mk {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] (f : β →+ β') (h₁ : ∀ (k : ℤ), (↑f).toFun (shift k) = shift k) (h₂ : ∀ (b : β), sign ((↑f).toFun b) = sign b) : ⇑{ toAddMonoidHom := f, map_shift' := h₁, map_sign' := h₂ } = ⇑f

theorem AInfinityTheory.GradingHom.ext {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {f g : β →+ᵍ β'} (h : ∀ (b : β), f b = g b) : f = g

Two homomorphisms of grading types are equal if they agree on every degree.

theorem AInfinityTheory.GradingHom.ext_iff {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] {f g : β →+ᵍ β'} : f = g ↔ ∀ (b : β), f b = g b

@[simp]

theorem AInfinityTheory.GradingHom.map_shift {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] (f : β →+ᵍ β') (k : ℤ) : f (shift k) = shift k

A homomorphism of grading types preserves the integer degree shifts.

@[simp]

theorem AInfinityTheory.GradingHom.map_sign {β : Type u_1} {β' : Type u_2} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] (f : β →+ᵍ β') (b : β) : sign (f b) = sign b

A homomorphism of grading types preserves the Koszul signs.

def AInfinityTheory.GradingHom.id (β : Type u_1) [AddCommGroup β] [GradingType β] : β →+ᵍ β

The identity homomorphism of a grading type.

Equations

• AInfinityTheory.GradingHom.id β = { toAddMonoidHom := AddMonoidHom.id β, map_shift' := ⋯, map_sign' := ⋯ }

@[simp]

theorem AInfinityTheory.GradingHom.id_apply {β : Type u_1} [AddCommGroup β] [GradingType β] (b : β) : (id β) b = b

def AInfinityTheory.GradingHom.comp {β : Type u_1} {β' : Type u_2} {β'' : Type u_3} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] [AddCommGroup β''] [GradingType β''] (g : β' →+ᵍ β'') (f : β →+ᵍ β') : β →+ᵍ β''

The composite of two homomorphisms of grading types.

Equations

• g.comp f = { toAddMonoidHom := g.comp f.toAddMonoidHom, map_shift' := ⋯, map_sign' := ⋯ }

@[simp]

theorem AInfinityTheory.GradingHom.comp_apply {β : Type u_1} {β' : Type u_2} {β'' : Type u_3} [AddCommGroup β] [GradingType β] [AddCommGroup β'] [GradingType β'] [AddCommGroup β''] [GradingType β''] (g : β' →+ᵍ β'') (f : β →+ᵍ β') (b : β) : (g.comp f) b = g (f b)