Unit identifications for the actual graded zigzag bimodule

The existing graded zigzag bimodule is the regular unit for balanced tensor composition. It is identified with the universe-lifted regular graded unit, the unit of the graded bimodule setting of the zigzag algebra. The resulting left and right unit isomorphisms identify the mixed terms in tensor products of braid complexes. Their pure-tensor formulas express the two restricted enveloping-algebra actions. The constructions specialize GradedModuleCat.bimoduleTensorLeftUnitor and GradedModuleCat.bimoduleTensorRightUnitor using ULift.moduleEquiv.

The unit complex of the graded bimodule setting of the zigzag algebra, the regular graded zigzag bimodule in cohomological degree zero, is zigzagBraidUnitComplex; zigzagBraidUnitComplexHomotopyEquiv identifies it with the unit complex of that setting. The hom and the inv of that equivalence are characterised by zigzagBraidUnitComplexHomotopyEquiv_hom and zigzagBraidUnitComplexHomotopyEquiv_inv.

noncomputable def TauCeti.zigzagGradedBimoduleUnitIso (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : GradedModuleCat.bimoduleUnit (zigzagAlgebraInternalGrading k G) ≅ zigzagGradedBimodule k G

The existing graded zigzag bimodule is the regular graded unit, at the lift universe w of the ground ring. This is the unit of the graded bimodule setting of the zigzag algebra, so the single isomorphism serves both the unit identifications of the braid complexes and the unit complex of that setting.

@[simp]

theorem TauCeti.zigzagGradedBimoduleUnitIso_hom_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (x : (GradedModuleCat.bimoduleUnit (zigzagAlgebraInternalGrading k G)).carrier) : (zigzagGradedBimoduleUnitIso k G).hom.hom x = x.down

@[simp]

theorem TauCeti.zigzagGradedBimoduleUnitIso_inv_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (x : (zigzagGradedBimodule k G).carrier) : (zigzagGradedBimoduleUnitIso k G).inv.hom x = { down := x }

@[reducible, inline]

noncomputable abbrev TauCeti.zigzagBraidUnitComplex (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : HomologicalComplex (GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) (ComplexShape.up ℤ)

The regular graded zigzag bimodule concentrated in cohomological degree zero: the common target of the two one-sided inverse-product equivalences of the braid family.

noncomputable def TauCeti.zigzagBraidUnitComplexHomotopyEquiv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : HomotopyEquiv (zigzagBraidUnitComplex k G) (gradedBimoduleUnitComplex k (zigzagAlgebraInternalGrading k G))

The regular graded zigzag bimodule is the unit complex of the graded bimodule setting of the zigzag algebra: the homotopy equivalence between the regular graded bimodule in cohomological degree zero and the unit complex of that setting. It is the transport of zigzagGradedBimoduleUnitIso to the single-degree complex.

@[simp]

theorem TauCeti.zigzagBraidUnitComplexHomotopyEquiv_hom (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : (zigzagBraidUnitComplexHomotopyEquiv k G).hom = (HomologicalComplex.single (GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) (ComplexShape.up ℤ) 0).map (zigzagGradedBimoduleUnitIso k G).inv

The hom of the unit-complex homotopy equivalence of the zigzag setting is the map of the single-degree complex induced by the inverse of the unit isomorphism. This is the characterisation that lets a consumer compute the hom of the unit comparison.

@[simp]

theorem TauCeti.zigzagBraidUnitComplexHomotopyEquiv_inv (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : (zigzagBraidUnitComplexHomotopyEquiv k G).inv = (HomologicalComplex.single (GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) (ComplexShape.up ℤ) 0).map (zigzagGradedBimoduleUnitIso k G).hom

The inv of the unit-complex homotopy equivalence of the zigzag setting is the map of the single-degree complex induced by the unit isomorphism. This is the characterisation that lets a consumer compute the inv of the unit comparison.

noncomputable def TauCeti.zigzagBimoduleLeftUnitor (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) : GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBimodule k G) M ≅ M

Tensoring the actual regular zigzag bimodule on the left preserves a graded bimodule.

noncomputable def TauCeti.zigzagBimoduleRightUnitor (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) : GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) M (zigzagGradedBimodule k G) ≅ M

Tensoring the actual regular zigzag bimodule on the right preserves a graded bimodule.

@[simp]

theorem TauCeti.zigzagBimoduleLeftUnitor_hom_tmul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) (z : (zigzagGradedBimodule k G).carrier) (m : M.carrier) : (zigzagBimoduleLeftUnitor k G M).hom.hom (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBimodule k G) M z m) = (Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))).symm z ⊗ₜ[k] 1 • m

@[simp]

theorem TauCeti.zigzagBimoduleRightUnitor_hom_tmul (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) (m : M.carrier) (z : (zigzagGradedBimodule k G).carrier) : (zigzagBimoduleRightUnitor k G M).hom.hom (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) M (zigzagGradedBimodule k G) m z) = 1 ⊗ₜ[k] MulOpposite.op ((Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))).symm z) • m

@[simp]

theorem TauCeti.zigzagBimoduleLeftUnitor_inv_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) (m : M.carrier) : (zigzagBimoduleLeftUnitor k G M).inv.hom m = GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBimodule k G) M ((Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))) 1) m

@[simp]

theorem TauCeti.zigzagBimoduleRightUnitor_inv_apply (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) (m : M.carrier) : (zigzagBimoduleRightUnitor k G M).inv.hom m = GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) M (zigzagGradedBimodule k G) m ((Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))) 1)

@[simp]

theorem TauCeti.zigzagBimoduleLeftUnitor_naturality (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) {N : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (CategoryTheory.CategoryStruct.id (zigzagGradedBimodule k G)) f) (zigzagBimoduleLeftUnitor k G N).hom = CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G M).hom f

The actual left unit identification commutes with graded bimodule maps.

@[simp]

theorem TauCeti.zigzagBimoduleLeftUnitor_naturality_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) {N : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (f : M ⟶ N) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (CategoryTheory.CategoryStruct.id (zigzagGradedBimodule k G)) f) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G N).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBimoduleLeftUnitor k G M).hom (CategoryTheory.CategoryStruct.comp f h)

The actual left unit identification commutes with graded bimodule maps.

@[simp]

theorem TauCeti.zigzagBimoduleRightUnitor_naturality (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) {N : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) f (CategoryTheory.CategoryStruct.id (zigzagGradedBimodule k G))) (zigzagBimoduleRightUnitor k G N).hom = CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G M).hom f

The actual right unit identification commutes with graded bimodule maps.

@[simp]

theorem TauCeti.zigzagBimoduleRightUnitor_naturality_assoc (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (M : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)) {N : GradedModuleCat ((zigzagEnvelopingGrading k G).piece ℤ)} (f : M ⟶ N) {Z : GradedModuleCat (((zigzagAlgebraInternalGrading k G).tensorProduct (zigzagAlgebraInternalGrading k G).opposite).piece ℤ)} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (GradedModuleCat.bimoduleTensorMap (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) f (CategoryTheory.CategoryStruct.id (zigzagGradedBimodule k G))) (CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G N).hom h) = CategoryTheory.CategoryStruct.comp (zigzagBimoduleRightUnitor k G M).hom (CategoryTheory.CategoryStruct.comp f h)

The actual right unit identification commutes with graded bimodule maps.

theorem TauCeti.zigzagBimoduleUnitHom_eq (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : (zigzagBimoduleLeftUnitor k G (zigzagGradedBimodule k G)).hom = (zigzagBimoduleRightUnitor k G (zigzagGradedBimodule k G)).hom

The two unit identifications agree when both factors are the regular bimodule.