Graded linear quivers

A graded R-linear quiver on a type of objects Obj assigns to each pair of objects X Y and each degree i : β an R-module Hom R X Y i of morphisms of degree i. It is the underlying data of an A∞-category, before any compositions are chosen.

Main definitions

• AInfinityTheory.GradedLinearQuiver β R Obj: a graded R-linear quiver.
• AInfinityTheory.GradedLinearQuiver.ComposableHomType: the hom space containing the i-th morphism of a composable string of objects.
• AInfinityTheory.GradedLinearQuiver.homCongr: transport between graded hom spaces along equalities of the source, target and degree.

Notation

• X →ᵍ[R] Y: the graded family GradedLinearQuiver.Hom R X Y : β → Type* of morphisms from X to Y, so that (X →ᵍ[R] Y) i is the R-module of morphisms of degree i. The variant X →ᵍ[R, β] Y names the grading type explicitly. Both are scoped to AInfinityTheory.GradedLinearQuiver.

class AInfinityTheory.GradedLinearQuiver (β : Type v) (R : Type u) [CommRing R] (Obj : Type w) : Type (max (max (max u v) w) (w' + 1))

A graded R-linear quiver: for objects X Y and a degree i, the morphisms of degree i from X to Y form an R-module Hom R X Y i.

• Hom : Obj → Obj → β → Type w'

  The morphisms of degree i from X to Y. The ring R is an explicit argument so that the notation X →ᵍ[R] Y can display it.

• homGroup (X Y : Obj) (i : β) : AddCommGroup (Hom R X Y i)

  Each graded piece of a hom space is an abelian group.

• homModule (X Y : Obj) (i : β) : Module R (Hom R X Y i)

  Each graded piece of a hom space is an R-module.

def AInfinityTheory.GradedLinearQuiver.«term_→ᵍ[_]_» : Lean.TrailingParserDescr

X →ᵍ[R] Y is the graded family of R-modules of morphisms from X to Y in a graded R-linear quiver, so (X →ᵍ[R] Y) i is the module Hom^i(X, Y) of degree-i morphisms.

Equations

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

def AInfinityTheory.GradedLinearQuiver.«term_→ᵍ[_,_]_» : Lean.TrailingParserDescr

X →ᵍ[R, β] Y is X →ᵍ[R] Y with the grading type β given explicitly, for use when β cannot be inferred from a degree or the expected type.

Equations

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

@[reducible, inline]

abbrev AInfinityTheory.GradedLinearQuiver.ComposableHomType {β : Type v} (R : Type u) [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] {n : ℕ} (obj : Fin (n + 1) → Obj) (i : Fin n) (b : β) : Type w'

The hom space containing the i-th morphism of a composable string of objects, in degree b.

Equations

• AInfinityTheory.GradedLinearQuiver.ComposableHomType R obj i b = AInfinityTheory.GradedLinearQuiver.Hom R (obj i.castSucc) (obj i.succ) b

def AInfinityTheory.GradedLinearQuiver.homCongr {β : Type v} (R : Type u) [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] {X X' Y Y' : Obj} {i i' : β} (hX : X = X') (hY : Y = Y') (hi : i = i') : Hom R X Y i ≃ₗ[R] Hom R X' Y' i'

Transport between graded hom spaces along equalities of the source, target and degree. This is the three-index form of LinearEquiv.cast.

Equations

• AInfinityTheory.GradedLinearQuiver.homCongr R hX hY hi = hX ▸ hY ▸ hi ▸ LinearEquiv.refl R (AInfinityTheory.GradedLinearQuiver.Hom R X Y i)

@[simp]

theorem AInfinityTheory.GradedLinearQuiver.homCongr_refl {β : Type v} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] (X Y : Obj) (i : β) : homCongr R ⋯ ⋯ ⋯ = LinearEquiv.refl R (Hom R X Y i)

Transport along reflexivity is the identity.

@[simp]

theorem AInfinityTheory.GradedLinearQuiver.homCongr_symm {β : Type v} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] {X X' Y Y' : Obj} {i i' : β} (hX : X = X') (hY : Y = Y') (hi : i = i') : (homCongr R hX hY hi).symm = homCongr R ⋯ ⋯ ⋯

The inverse of a transport is the transport along the reversed equalities.

@[simp]

theorem AInfinityTheory.GradedLinearQuiver.homCongr_trans {β : Type v} {R : Type u} [CommRing R] {Obj : Type w} [GradedLinearQuiver β R Obj] {X X' X'' Y Y' Y'' : Obj} {i i' i'' : β} (hX : X = X') (hY : Y = Y') (hi : i = i') (hX' : X' = X'') (hY' : Y' = Y'') (hi' : i' = i'') : homCongr R hX hY hi ≪≫ₗ homCongr R hX' hY' hi' = homCongr R ⋯ ⋯ ⋯

Transporting twice is transporting along the composite equalities.