Graded linear quivers induced along a map of objects

For a graded linear quiver C and a map F : D → C, the induced quiver InducedQuiver C F has an object X for each object X.obj of D, and as morphisms X ⟶ Y the graded hom module of C from F X.obj to F Y.obj. It is the graded-quiver analogue of Mathlib's CategoryTheory.InducedCategory, with the objects of D wrapped in a structure. The full subquiver TauCeti.GradedLinearQuiver.FullSubquiver P on the objects satisfying a predicate P is the induced quiver along Subtype.val. An A∞ structure on C induces one on the induced quiver (TauCeti.AInfinityCategory.induced), operating on a composable string as C does on its image.

The quiver, its total-module constructions, and their Koszul-twist compatibility work over any ring. The higher A∞ structure uses commutative scalars.

The total module of morphisms of the induced quiver maps to that of C (TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap), sending a morphism X ⟶ Y to the same morphism F X.obj ⟶ F Y.obj. The map preserves degrees and is injective on each hom module. When F is injective, the map is injective and detects degrees. When F is not injective, the map need not be injective, since distinct pairs of objects can have the same image and hence the same hom module of C; and a string of morphisms that is not composable in the induced quiver can become composable in C.

Main definitions

• TauCeti.GradedLinearQuiver.InducedQuiver: the objects of D, with the graded hom modules of C between their images under F.
• TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap: the map of total modules of morphisms.

Main results

• TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_homInclusion: the map sends a morphism of the induced quiver to the same morphism of C.
• TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_mem_totalGrading_piece: the map preserves degrees.
• TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_injective and TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_mem_totalGrading_piece_iff: along an injective map of objects, the map is injective and detects degrees.
• TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_surjective: along a surjective map of objects, the map is surjective.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 7, for A∞ categories and functors.

structure TauCeti.GradedLinearQuiver.InducedQuiver {D : Type u'} (C : Type u) (F : D → C) : Type u'

The objects of the quiver induced along F : D → C: one object for each object of D. When C is a graded linear quiver, so is InducedQuiver C F, with the hom module of C from F X.obj to F Y.obj as its hom module from X to Y.

• obj : D

  The underlying object of D.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.ext_iff {D : Type u'} {C : Type u} {F : D → C} {x y : InducedQuiver C F} : x = y ↔ x.obj = y.obj

theorem TauCeti.GradedLinearQuiver.InducedQuiver.ext {D : Type u'} {C : Type u} {F : D → C} {x y : InducedQuiver C F} (obj : x.obj = y.obj) : x = y

@[instance_reducible]

instance TauCeti.GradedLinearQuiver.InducedQuiver.inst {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} : GradedLinearQuiver R (InducedQuiver C F)

The induced quiver of a graded linear quiver is a graded linear quiver, with the graded hom modules of C between the images of the objects.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.homModule_eq {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} (X Y : InducedQuiver C F) : homModule X Y = homModule (F X.obj) (F Y.obj)

The hom module between two objects of an induced quiver is the hom module of C between their images.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.grading_eq {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} (X Y : InducedQuiver C F) : grading X Y = grading (F X.obj) (F Y.obj)

The grading of the hom module between two objects of an induced quiver is the grading in C between their images.

noncomputable def TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap {D : Type u'} {C : Type u} (R : Type w) [Ring R] [GradedLinearQuiver R C] (F : D → C) : TotalHom R (InducedQuiver C F) →ₗ[R] TotalHom R C

The map of total modules of morphisms of the induced quiver to that of C: on the hom module of X and Y it is the inclusion of the hom module of F X.obj and F Y.obj.

@[simp]

theorem TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_homInclusion {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} (X Y : InducedQuiver C F) (f : ↑(homModule X Y)) : (totalHomMap R F) ((homInclusion X Y) f) = (homInclusion (F X.obj) (F Y.obj)) f

The map of total modules sends a morphism X ⟶ Y of the induced quiver to the same morphism F X.obj ⟶ F Y.obj of C.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_mem_totalGrading_piece {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} {n : ℤ} {x : TotalHom R (InducedQuiver C F)} (hx : x ∈ (totalGrading R (InducedQuiver C F)).piece ℤ n) : (totalHomMap R F) x ∈ (totalGrading R C).piece ℤ n

The map of total modules of an induced quiver preserves degrees.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.isHomogeneous_totalHomMap {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} : LinearMap.IsHomogeneous (totalHomMap R F) ((totalGrading R (InducedQuiver C F)).piece ℤ) ((totalGrading R C).piece ℤ) 0

The map of total modules of an induced quiver is homogeneous of degree zero.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.homProjection_totalHomMap_of_not {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} {X Y : C} (h : ¬(X ∈ Set.range F ∧ Y ∈ Set.range F)) (x : TotalHom R (InducedQuiver C F)) : (homProjection X Y) ((totalHomMap R F) x) = 0

The component of the image of an element between two objects of C not both in the image of F vanishes.

@[simp]

theorem TauCeti.GradedLinearQuiver.InducedQuiver.homProjection_totalHomMap {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} (hF : Function.Injective F) (X Y : InducedQuiver C F) (x : TotalHom R (InducedQuiver C F)) : (homProjection (F X.obj) (F Y.obj)) ((totalHomMap R F) x) = (homProjection X Y) x

Along an injective map of objects, the component between the images of two objects of the image of an element in the total module of C is its component in the induced quiver.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_injective {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} (hF : Function.Injective F) : Function.Injective ⇑(totalHomMap R F)

Along an injective map of objects, the map of total modules of morphisms is injective.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_mem_totalGrading_piece_iff {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} (hF : Function.Injective F) (n : ℤ) (x : TotalHom R (InducedQuiver C F)) : (totalHomMap R F) x ∈ (totalGrading R C).piece ℤ n ↔ x ∈ (totalGrading R (InducedQuiver C F)).piece ℤ n

Along an injective map of objects, the map of total modules of morphisms detects degrees.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.totalHomMap_surjective {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} (hF : Function.Surjective F) : Function.Surjective ⇑(totalHomMap R F)

Along a surjective map of objects, the map of total modules of morphisms is surjective: a morphism F X ⟶ F Y of C is the image of the same morphism ⟨X⟩ ⟶ ⟨Y⟩ of the induced quiver.

theorem TauCeti.GradedLinearQuiver.InducedQuiver.koszulTwist_totalHomMap {D : Type u'} {C : Type u} {R : Type w} [Ring R] [GradedLinearQuiver R C] {F : D → C} (q : ℤ) (x : TotalHom R (InducedQuiver C F)) : ((totalGrading R C).koszulTwist q) ((totalHomMap R F) x) = (totalHomMap R F) (((totalGrading R (InducedQuiver C F)).koszulTwist q) x)

The map of total modules of an induced quiver commutes with the Koszul twists.