A transfer principle for the Khovanov-Seidel braid relations #
The Khovanov-Seidel braid relations are relations between complexes of bimodules in a graded
bimodule setting: the two one-sided inverse products are homotopy equivalent to the unit of
the setting, the nonadjacent factors commute up to chain homotopy, and the adjacent factors
satisfy the braid relation up to chain homotopy. A graded bimodule setting is a graded algebra
A with an internal grading Ξ: its graded bimodules are the graded modules over the
enveloping grading Ξ.tensorProduct Ξ.opposite, they are combined by the balanced bimodule
tensor GradedModuleCat.bimoduleTensor Ξ Ξ Ξ, and the unit complex of the setting is
gradedBimoduleUnitComplex k Ξ, the regular graded bimodule
GradedModuleCat.bimoduleUnit Ξ placed in cohomological degree zero. The category
GradedBimoduleCat of such a setting is defined in
TauCeti.Algebra.Category.GradedModuleCat.BimoduleTensor.Basic, next to
GradedModuleCat.bimoduleTensor, and the unit complex
gradedBimoduleUnitComplex in TauCeti.Algebra.Category.GradedModuleCat.BimoduleTensor.Unit,
next to GradedModuleCat.bimoduleUnit. The pointwise homotopy-monoidal datum
GradedBimoduleMonoidalDatum of a functor on complexes of graded bimodules is defined in
TauCeti.Algebra.Category.GradedModuleCat.BimoduleTensor.Monoidal, next to
bimoduleMonoidalCategory.
KhovanovSeidelRelations records the three relations for a family C of complexes with
prescribed inverses C' in a graded bimodule setting. The unit of the relations is the unit
complex gradedBimoduleUnitComplex k Ξ of that setting, so the two inverse relations are
statements about the actual unit of the tensor.
KhovanovSeidelRelations.transfer is the transfer principle. It is stated for a functor Φ
on complexes of graded bimodules from a source graded bimodule setting to a target graded
bimodule setting, together with
- a datum
hΦ, carrying every homotopy equivalence of source complexes to a homotopy equivalence of image complexes, - a pointwise homotopy-monoidal datum
η : GradedBimoduleMonoidalDatum k Ξ₁ Ξ₂ Φ, a homotopy equivalence for every pair of source complexesXandYcomparing the target tensor product of the image complexes with the image of the source tensor product, and - a unit datum
ε, a homotopy equivalence comparing the image of the source unit complex with the target unit complex,
and transports the three relations from the source setting to the target setting, provided the
image complexes are identified with a target family by the homotopy equivalences a and a'.
The two settings need not agree: the target is a second graded algebra, and Φ need not be an
equivalence.
KhovanovSeidelRelations.transferDegreewise is the degreewise specialisation of the
principle: the transfer at the functor H.mapHomologicalComplex c of an additive functor H
of graded bimodule categories. The functors it covers include the Morita-type equivalences
realised by a single bimodule, whose action on a complex of bimodules is the degreewise action
of that equivalence.
The four field values of the transferred relations are the public declarations
transferInverseForward, transferInverseReverse, transferCommute and transferBraid,
and the four projection lemmas transfer_inverseForward, transfer_inverseReverse,
transfer_commute and transfer_braid read those values off the transferred relations; the
four projection lemmas transferDegreewise_inverseForward and its three siblings read them off
the degreewise transferred relations. The hom and the inv of each of the four transferred
equivalences are characterised by the lemmas transferInverseForward_hom and
transferInverseForward_inv and their three sibling pairs, in terms of the supplied
equivalences and the tensor maps.
Scope #
The principle is stated for a functor Φ on complexes of graded bimodules, with the datum hΦ
that it carries homotopy equivalences to homotopy equivalences. Conjugation of bimodules with a
tilting bimodule complex is a functor on complexes of bimodules and not an additive functor on
bimodules, so it is not an instance of the degreewise specialisation transferDegreewise, but
it is an instance of Φ. The monoidal and unit compatibilities η and ε are hypotheses of
the principle, supplied by each instantiation.
Naturality of the transferred relations up to chain homotopy, the derived-Koszul comparison,
spherical twists and graded-K₀ statements are out of scope.
References #
- M. Khovanov and P. Seidel, Quivers, Floer cohomology, and braid group actions, arXiv:math/0006056.
The three Khovanov-Seidel relations for a family C of complexes of graded bimodules in
the graded bimodule setting of Ξ, with prescribed inverses C': both one-sided inverse
products C i ⊗ C' i and C' i ⊗ C i are homotopy equivalent to the unit complex of the
setting, the nonadjacent factors commute up to chain homotopy, and the adjacent factors
satisfy the braid relation up to chain homotopy.
- inverseForward (i : V) : HomotopyEquiv ((C i).mapBifunctor (C' i) (GradedModuleCat.bimoduleTensor Ξ Ξ Ξ) (ComplexShape.up ℤ)) (gradedBimoduleUnitComplex k Ξ)
The forward inverse product
C i ⊗ C' iis homotopy equivalent to the unit. - inverseReverse (i : V) : HomotopyEquiv ((C' i).mapBifunctor (C i) (GradedModuleCat.bimoduleTensor Ξ Ξ Ξ) (ComplexShape.up ℤ)) (gradedBimoduleUnitComplex k Ξ)
The reverse inverse product
C' i ⊗ C iis homotopy equivalent to the unit. - commute (i j : V) (hij : i ≠ j) (hadj : ¬G.Adj i j) : HomotopyEquiv ((C i).mapBifunctor (C j) (GradedModuleCat.bimoduleTensor Ξ Ξ Ξ) (ComplexShape.up ℤ)) ((C j).mapBifunctor (C i) (GradedModuleCat.bimoduleTensor Ξ Ξ Ξ) (ComplexShape.up ℤ))
Nonadjacent factors commute up to chain homotopy.
- braid {i j : V} (h : G.Adj j i) : HomotopyEquiv (((C i).mapBifunctor (C j) (GradedModuleCat.bimoduleTensor Ξ Ξ Ξ) (ComplexShape.up ℤ)).mapBifunctor (C i) (GradedModuleCat.bimoduleTensor Ξ Ξ Ξ) (ComplexShape.up ℤ)) (((C j).mapBifunctor (C i) (GradedModuleCat.bimoduleTensor Ξ Ξ Ξ) (ComplexShape.up ℤ)).mapBifunctor (C j) (GradedModuleCat.bimoduleTensor Ξ Ξ Ξ) (ComplexShape.up ℤ))
Adjacent factors satisfy the braid relation up to chain homotopy.
Instances For
Transfer of the forward inverse relation of the source family to the target setting: the
target tensor product C i ⊗ C' i is homotopy equivalent to the target unit complex.
Instances For
Transfer of the reverse inverse relation of the source family to the target setting: the
target tensor product C' i ⊗ C i is homotopy equivalent to the target unit complex.
Instances For
Transfer of the commutation relation of the source family to the target setting: the
target tensor products C i ⊗ C j and C j ⊗ C i are homotopy equivalent for nonadjacent
vertices.
Instances For
Transfer of the braid relation of the source family to the target setting: the target
triple tensor products C i ⊗ C j ⊗ C i and C j ⊗ C i ⊗ C j are homotopy equivalent at
adjacent vertices.
Instances For
The hom of the forward inverse transfer is the composite of the tensor map induced by
the inverses of the identifications a i and a' i, the hom of the monoidal datum
η (B i) (B' i), the hom of the image hΦ (rel.inverseForward i) of the source forward
inverse relation, and the hom of the unit datum ε.
The inv of the forward inverse transfer is the composite of the inv of the unit datum
ε, the inv of the image hΦ (rel.inverseForward i) of the source forward inverse
relation, the inv of the monoidal datum η (B i) (B' i), and the tensor map induced by the
identifications a i and a' i.
The hom of the reverse inverse transfer is the composite of the tensor map induced by
the inverses of the identifications a' i and a i, the hom of the monoidal datum
η (B' i) (B i), the hom of the image hΦ (rel.inverseReverse i) of the source reverse
inverse relation, and the hom of the unit datum ε.
The inv of the reverse inverse transfer is the composite of the inv of the unit datum
ε, the inv of the image hΦ (rel.inverseReverse i) of the source reverse inverse
relation, the inv of the monoidal datum η (B' i) (B i), and the tensor map induced by the
identifications a' i and a i.
The hom of the commutation transfer is the composite of the tensor map induced by the
inverses of the identifications a i and a j, the hom of the monoidal datum
η (B i) (B j), the hom of the image hΦ (rel.commute i j hij hadj) of the source
commutation relation, the inv of the monoidal datum η (B j) (B i), and the tensor map
induced by the identifications a j and a i.
The inv of the commutation transfer is the composite of the tensor map induced by the
inverses of the identifications a j and a i, the hom of the monoidal datum
η (B j) (B i), the inv of the image hΦ (rel.commute i j hij hadj) of the source
commutation relation, the inv of the monoidal datum η (B i) (B j), and the tensor map
induced by the identifications a i and a j.
The hom of the braid transfer is the composite of the tensor map of the inverses of
the identifications a i and a j with the inverse of a i, the tensor map of the hom of
the monoidal datum η (B i) (B j) with the identity of Φ.obj (B i), the hom of the
monoidal datum η (mapBifunctor (B i) (B j) …) (B i), the hom of the image
hΦ (rel.braid h) of the source braid relation, the inv of the monoidal datum
η (mapBifunctor (B j) (B i) …) (B j), the tensor map of the inv of the monoidal datum
η (B j) (B i) with the identity of Φ.obj (B j), and the tensor map of the identifications
a j and a i with a j.
The inv of the braid transfer is the composite of the tensor map of the inverses of
the identifications a j and a i with the inverse of a j, the tensor map of the hom of
the monoidal datum η (B j) (B i) with the identity of Φ.obj (B j), the hom of the
monoidal datum η (mapBifunctor (B j) (B i) …) (B j), the inv of the image
hΦ (rel.braid h) of the source braid relation, the inv of the monoidal datum
η (mapBifunctor (B i) (B j) …) (B i), the tensor map of the inv of the monoidal datum
η (B i) (B j) with the identity of Φ.obj (B i), and the tensor map of the identifications
a i and a j with a i.
Transfer of the Khovanov-Seidel relations of a source family to a target graded bimodule
setting. Let Φ be a functor on complexes of graded bimodules from the source setting of Ξ₁
to the target setting of Ξ₂, let hΦ carry the homotopy equivalences of source complexes
to homotopy equivalences of image complexes, let η be the pointwise homotopy-monoidal datum
of Φ comparing the target tensor product of image complexes with the image of the source
tensor product, and let ε compare the image of the source unit complex with the target unit
complex. If the source family B with its inverses B' satisfies the Khovanov-Seidel
relations in the source setting, and the image complexes are identified with a target family C
with inverses C' by the homotopy equivalences a and a', then the target family satisfies
the Khovanov-Seidel relations in the target setting.
Instances For
The degreewise specialisation of the transfer principle: the transfer at the functor
H.mapHomologicalComplex c of an additive functor H of graded bimodule categories, whose
homotopy equivalences are carried along by H.mapHomotopyEquiv. It applies in particular to
the Morita-type equivalences realised by a single bimodule, whose action on a complex of
bimodules is the degreewise action of that equivalence.
Instances For
The forward inverse relation of the transferred relations is the forward inverse transfer
transferInverseForward.
The reverse inverse relation of the transferred relations is the reverse inverse transfer
transferInverseReverse.
The commutation relation of the transferred relations is the commutation transfer
transferCommute.
The braid relation of the transferred relations is the braid transfer transferBraid.
The forward inverse relation of the degreewise transferred relations is the forward inverse
transfer transferInverseForward.
The reverse inverse relation of the degreewise transferred relations is the reverse inverse
transfer transferInverseReverse.
The commutation relation of the degreewise transferred relations is the commutation
transfer transferCommute.
The braid relation of the degreewise transferred relations is the braid transfer
transferBraid.