Strict functors of A-infinity categories

A strict functor of nonunital A∞ categories consists of an object map and degree-zero linear maps on Hom modules preserving every operation on composable strings. Its higher functor components are zero. No identity-preservation condition is imposed here.

The operation equation is required only on composable strings. In particular, the object map need not be injective: two arrows that are not composable can become composable after applying it. Requiring a morphism of the total morphism algebras would incorrectly exclude such functors.

We provide extensionality, identity, composition, the degreewise operation equation, and the chain-map and binary-composition equations. Between A∞ categories whose operations of arity at least three vanish, such as those of differential graded categories, the chain-map and binary-composition equations suffice to give a strict functor (TauCeti.AInfinityStrictFunctor.ofHomDifferentialComp). Composition has no additional Koszul sign because all Hom maps have degree zero.

References

• B. Keller, Introduction to A-infinity algebras and modules, Sections 3.4 and 7.1.

structure TauCeti.AInfinityStrictFunctor {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] (𝒞 : AInfinityCategory R C) (𝒟 : AInfinityCategory R D) : Type (max (max (max u₁ u₂) v₁) v₂)

A strict functor between nonunital A∞ categories: an arbitrary object map and degree-zero linear Hom maps commuting with all operations on composable strings. There is no unit-preservation condition.

• obj : C → D

  The map on objects.

• map (X Y : C) : ↑(GradedLinearQuiver.homModule X Y) →ₗ[R] ↑(GradedLinearQuiver.homModule (self.obj X) (self.obj Y))

  The linear map on each Hom module.

• map_mem' (X Y : C) {p : ℤ} {f : ↑(GradedLinearQuiver.homModule X Y)} : f ∈ (GradedLinearQuiver.grading X Y).piece ℤ p → (self.map X Y) f ∈ (GradedLinearQuiver.grading (self.obj X) (self.obj Y)).piece ℤ p

  Each Hom map preserves degree.

• map_m' {n : ℕ} (X : Fin (n + 1) → C) (f : (i : Fin n) → ↑(GradedLinearQuiver.homModule (X i.rev.castSucc) (X i.rev.succ))) : (self.map (X 0) (X (Fin.last n))) ((GradedLinearQuiver.homProjection (X 0) (X (Fin.last n))) ((𝒞.m n) fun (i : Fin n) => (GradedLinearQuiver.homInclusion (X i.rev.castSucc) (X i.rev.succ)) (f i))) = (GradedLinearQuiver.homProjection (self.obj (X 0)) (self.obj (X (Fin.last n)))) ((𝒟.m n) fun (i : Fin n) => (GradedLinearQuiver.homInclusion (self.obj (X i.rev.castSucc)) (self.obj (X i.rev.succ))) ((self.map (X i.rev.castSucc) (X i.rev.succ)) (f i)))

  Each operation is preserved on every composable string, in Keller's input order.

theorem TauCeti.AInfinityStrictFunctor.ext {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} {F G : AInfinityStrictFunctor 𝒞 𝒟} (hobj : F.obj = G.obj) (hmap : F.map ≍ G.map) : F = G

Strict functors are determined by their object and Hom maps. The heterogeneous equality accounts only for the endpoints of the target Hom modules.

theorem TauCeti.AInfinityStrictFunctor.ext_iff {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} {F G : AInfinityStrictFunctor 𝒞 𝒟} : F = G ↔ F.obj = G.obj ∧ F.map ≍ G.map

theorem TauCeti.AInfinityStrictFunctor.ext_of_obj_eq {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} {F G : AInfinityStrictFunctor 𝒞 𝒟} (hobj : F.obj = G.obj) (hmap : ∀ (X Y : C) (f : ↑(GradedLinearQuiver.homModule X Y)), hobj ▸ (F.map X Y) f = (G.map X Y) f) : F = G

Strict functors with equal object maps are equal if their Hom maps agree pointwise, after transporting the target endpoints along the object-map equality.

theorem TauCeti.AInfinityStrictFunctor.map_mem {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (F : AInfinityStrictFunctor 𝒞 𝒟) (X Y : C) {p : ℤ} {f : ↑(GradedLinearQuiver.homModule X Y)} (hf : f ∈ (GradedLinearQuiver.grading X Y).piece ℤ p) : (F.map X Y) f ∈ (GradedLinearQuiver.grading (F.obj X) (F.obj Y)).piece ℤ p

The Hom map of a strict functor preserves degree.

@[simp]

theorem TauCeti.AInfinityStrictFunctor.map_m {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (F : AInfinityStrictFunctor 𝒞 𝒟) {n : ℕ} (X : Fin (n + 1) → C) (f : (i : Fin n) → ↑(GradedLinearQuiver.homModule (X i.rev.castSucc) (X i.rev.succ))) : (F.map (X 0) (X (Fin.last n))) ((GradedLinearQuiver.homProjection (X 0) (X (Fin.last n))) ((𝒞.m n) fun (i : Fin n) => (GradedLinearQuiver.homInclusion (X i.rev.castSucc) (X i.rev.succ)) (f i))) = (GradedLinearQuiver.homProjection (F.obj (X 0)) (F.obj (X (Fin.last n)))) ((𝒟.m n) fun (i : Fin n) => (GradedLinearQuiver.homInclusion (F.obj (X i.rev.castSucc)) (F.obj (X i.rev.succ))) ((F.map (X i.rev.castSucc) (X i.rev.succ)) (f i)))

A strict functor preserves operations on composable strings of arbitrary morphisms.

def TauCeti.AInfinityStrictFunctor.gradedMap {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (F : AInfinityStrictFunctor 𝒞 𝒟) (X Y : C) (p : ℤ) : GradedLinearQuiver.grHom R X Y p →ₗ[R] GradedLinearQuiver.grHom R (F.obj X) (F.obj Y) p

The map of a strict functor on the degree-p piece of a Hom module.

@[simp]

theorem TauCeti.AInfinityStrictFunctor.coe_gradedMap {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (F : AInfinityStrictFunctor 𝒞 𝒟) (X Y : C) (p : ℤ) (f : GradedLinearQuiver.grHom R X Y p) : ↑((F.gradedMap X Y p) f) = (F.map X Y) ↑f

@[simp]

theorem TauCeti.AInfinityStrictFunctor.map_pathOperation {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (F : AInfinityStrictFunctor 𝒞 𝒟) {n : ℕ} (X : Fin (n + 1) → C) (d : Fin n → ℤ) (f : (i : Fin n) → GradedLinearQuiver.grHom R (X i.rev.castSucc) (X i.rev.succ) (d i)) : (F.gradedMap (X 0) (X (Fin.last n)) (∑ i : Fin n, d i + (2 - ↑n))) ((𝒞.pathOperation X d) f) = (𝒟.pathOperation (F.obj ∘ X) d) fun (i : Fin n) => (F.gradedMap (X i.rev.castSucc) (X i.rev.succ) (d i)) (f i)

A strict functor preserves the degreewise operations on composable homogeneous morphisms.

@[simp]

theorem TauCeti.AInfinityStrictFunctor.map_homDifferential {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (F : AInfinityStrictFunctor 𝒞 𝒟) (X Y : C) (f : ↑(GradedLinearQuiver.homModule X Y)) : (F.map X Y) ((𝒞.homDifferential X Y) f) = (𝒟.homDifferential (F.obj X) (F.obj Y)) ((F.map X Y) f)

A strict functor commutes with the differential of every Hom module.

@[simp]

theorem TauCeti.AInfinityStrictFunctor.map_comp {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (F : AInfinityStrictFunctor 𝒞 𝒟) (X Y Z : C) (g : ↑(GradedLinearQuiver.homModule Y Z)) (f : ↑(GradedLinearQuiver.homModule X Y)) : (F.map X Z) (((𝒞.comp X Y Z) g) f) = ((𝒟.comp (F.obj X) (F.obj Y) (F.obj Z)) ((F.map Y Z) g)) ((F.map X Y) f)

A strict functor preserves the binary composition m₂(g,f).

def TauCeti.AInfinityStrictFunctor.ofHomDifferentialComp {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (h𝒞 : ∀ (n : ℕ), 3 ≤ n → 𝒞.m n = 0) (h𝒟 : ∀ (n : ℕ), 3 ≤ n → 𝒟.m n = 0) (obj : C → D) (map : (X Y : C) → ↑(GradedLinearQuiver.homModule X Y) →ₗ[R] ↑(GradedLinearQuiver.homModule (obj X) (obj Y))) (map_mem : ∀ (X Y : C) {p : ℤ} {f : ↑(GradedLinearQuiver.homModule X Y)}, f ∈ (GradedLinearQuiver.grading X Y).piece ℤ p → (map X Y) f ∈ (GradedLinearQuiver.grading (obj X) (obj Y)).piece ℤ p) (map_homDifferential : ∀ (X Y : C) (f : ↑(GradedLinearQuiver.homModule X Y)), (map X Y) ((𝒞.homDifferential X Y) f) = (𝒟.homDifferential (obj X) (obj Y)) ((map X Y) f)) (map_comp : ∀ (X Y Z : C) (g : ↑(GradedLinearQuiver.homModule Y Z)) (f : ↑(GradedLinearQuiver.homModule X Y)), (map X Z) (((𝒞.comp X Y Z) g) f) = ((𝒟.comp (obj X) (obj Y) (obj Z)) ((map Y Z) g)) ((map X Y) f)) : AInfinityStrictFunctor 𝒞 𝒟

A strict functor between A∞ categories whose operations of arity at least three vanish, from an object map and degree-preserving linear Hom maps commuting with the differential m₁ and preserving the composition m₂.

@[simp]

theorem TauCeti.AInfinityStrictFunctor.ofHomDifferentialComp_obj {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (h𝒞 : ∀ (n : ℕ), 3 ≤ n → 𝒞.m n = 0) (h𝒟 : ∀ (n : ℕ), 3 ≤ n → 𝒟.m n = 0) (obj : C → D) (map : (X Y : C) → ↑(GradedLinearQuiver.homModule X Y) →ₗ[R] ↑(GradedLinearQuiver.homModule (obj X) (obj Y))) (map_mem : ∀ (X Y : C) {p : ℤ} {f : ↑(GradedLinearQuiver.homModule X Y)}, f ∈ (GradedLinearQuiver.grading X Y).piece ℤ p → (map X Y) f ∈ (GradedLinearQuiver.grading (obj X) (obj Y)).piece ℤ p) (map_homDifferential : ∀ (X Y : C) (f : ↑(GradedLinearQuiver.homModule X Y)), (map X Y) ((𝒞.homDifferential X Y) f) = (𝒟.homDifferential (obj X) (obj Y)) ((map X Y) f)) (map_comp : ∀ (X Y Z : C) (g : ↑(GradedLinearQuiver.homModule Y Z)) (f : ↑(GradedLinearQuiver.homModule X Y)), (map X Z) (((𝒞.comp X Y Z) g) f) = ((𝒟.comp (obj X) (obj Y) (obj Z)) ((map Y Z) g)) ((map X Y) f)) (X : C) : (ofHomDifferentialComp h𝒞 h𝒟 obj map map_mem map_homDifferential map_comp).obj X = obj X

@[simp]

theorem TauCeti.AInfinityStrictFunctor.ofHomDifferentialComp_map {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (h𝒞 : ∀ (n : ℕ), 3 ≤ n → 𝒞.m n = 0) (h𝒟 : ∀ (n : ℕ), 3 ≤ n → 𝒟.m n = 0) (obj : C → D) (map : (X Y : C) → ↑(GradedLinearQuiver.homModule X Y) →ₗ[R] ↑(GradedLinearQuiver.homModule (obj X) (obj Y))) (map_mem : ∀ (X Y : C) {p : ℤ} {f : ↑(GradedLinearQuiver.homModule X Y)}, f ∈ (GradedLinearQuiver.grading X Y).piece ℤ p → (map X Y) f ∈ (GradedLinearQuiver.grading (obj X) (obj Y)).piece ℤ p) (map_homDifferential : ∀ (X Y : C) (f : ↑(GradedLinearQuiver.homModule X Y)), (map X Y) ((𝒞.homDifferential X Y) f) = (𝒟.homDifferential (obj X) (obj Y)) ((map X Y) f)) (map_comp : ∀ (X Y Z : C) (g : ↑(GradedLinearQuiver.homModule Y Z)) (f : ↑(GradedLinearQuiver.homModule X Y)), (map X Z) (((𝒞.comp X Y Z) g) f) = ((𝒟.comp (obj X) (obj Y) (obj Z)) ((map Y Z) g)) ((map X Y) f)) (X Y : C) : (ofHomDifferentialComp h𝒞 h𝒟 obj map map_mem map_homDifferential map_comp).map X Y = map X Y

def TauCeti.AInfinityStrictFunctor.id {R : Type w} [CommRing R] {C : Type u₁} [GradedLinearQuiver R C] (𝒞 : AInfinityCategory R C) : AInfinityStrictFunctor 𝒞 𝒞

The identity strict functor of a nonunital A∞ category.

@[simp]

theorem TauCeti.AInfinityStrictFunctor.id_obj {R : Type w} [CommRing R] {C : Type u₁} [GradedLinearQuiver R C] (𝒞 : AInfinityCategory R C) (X : C) : (AInfinityStrictFunctor.id 𝒞).obj X = X

@[simp]

theorem TauCeti.AInfinityStrictFunctor.id_map {R : Type w} [CommRing R] {C : Type u₁} [GradedLinearQuiver R C] (𝒞 : AInfinityCategory R C) (X Y : C) : (AInfinityStrictFunctor.id 𝒞).map X Y = LinearMap.id

def TauCeti.AInfinityStrictFunctor.comp {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} {E : Type u₃} [GradedLinearQuiver R C] [GradedLinearQuiver R D] [GradedLinearQuiver R E] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} {ℰ : AInfinityCategory R E} (G : AInfinityStrictFunctor 𝒟 ℰ) (F : AInfinityStrictFunctor 𝒞 𝒟) : AInfinityStrictFunctor 𝒞 ℰ

Composition of strict functors: apply the first Hom map, then the second.

@[simp]

theorem TauCeti.AInfinityStrictFunctor.comp_obj {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} {E : Type u₃} [GradedLinearQuiver R C] [GradedLinearQuiver R D] [GradedLinearQuiver R E] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} {ℰ : AInfinityCategory R E} (G : AInfinityStrictFunctor 𝒟 ℰ) (F : AInfinityStrictFunctor 𝒞 𝒟) (X : C) : (G.comp F).obj X = G.obj (F.obj X)

@[simp]

theorem TauCeti.AInfinityStrictFunctor.comp_map {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} {E : Type u₃} [GradedLinearQuiver R C] [GradedLinearQuiver R D] [GradedLinearQuiver R E] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} {ℰ : AInfinityCategory R E} (G : AInfinityStrictFunctor 𝒟 ℰ) (F : AInfinityStrictFunctor 𝒞 𝒟) (X Y : C) : (G.comp F).map X Y = G.map (F.obj X) (F.obj Y) ∘ₗ F.map X Y

@[simp]

theorem TauCeti.AInfinityStrictFunctor.comp_id {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (F : AInfinityStrictFunctor 𝒞 𝒟) : F.comp (AInfinityStrictFunctor.id 𝒞) = F

@[simp]

theorem TauCeti.AInfinityStrictFunctor.id_comp {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} [GradedLinearQuiver R C] [GradedLinearQuiver R D] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} (F : AInfinityStrictFunctor 𝒞 𝒟) : (AInfinityStrictFunctor.id 𝒟).comp F = F

@[simp]

theorem TauCeti.AInfinityStrictFunctor.comp_assoc {R : Type w} [CommRing R] {C : Type u₁} {D : Type u₂} {E : Type u₃} {K : Type u₄} [GradedLinearQuiver R C] [GradedLinearQuiver R D] [GradedLinearQuiver R E] [GradedLinearQuiver R K] {𝒞 : AInfinityCategory R C} {𝒟 : AInfinityCategory R D} {ℰ : AInfinityCategory R E} {𝒦 : AInfinityCategory R K} (H : AInfinityStrictFunctor ℰ 𝒦) (G : AInfinityStrictFunctor 𝒟 ℰ) (F : AInfinityStrictFunctor 𝒞 𝒟) : (H.comp G).comp F = H.comp (G.comp F)

Composition of strict functors is associative.