Tensor factors of the zigzag vertex bimodule

The cyclic enveloping-algebra ideal used for zigzagBraidBimodule is Z e_i ⊗[k] e_i Z. The right ideal is represented in Zᵐᵒᵖ. We identify these presentations using spanSingletonTensorProductEquiv and LinearEquiv.ofEq, and compute the two outer actions on the tensor factors.

This carrier identification is the input for extracting the middle corner from balanced products of vertex bimodules. In particular it supplies a prerequisite for the self-tensor decomposition used in the inverse braid homotopy equivalence. The construction covers isolated vertices of the public componentwise algebra. Balanced products extract the middle corner e_i Z e_j, leaving the two outer ideal factors.

noncomputable def TauCeti.zigzagBraidBimoduleFactorsEquiv (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagGradedBraidBimodule k G i).carrier ≃ₗ[k] TensorProduct k ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i) ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)

Identify the actual graded vertex bimodule carrier with its two idempotent-ideal factors.

theorem TauCeti.coe_zigzagBraidBimoduleFactorsEquiv_symm_apply (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (t : TensorProduct k ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i) ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) : ↑((zigzagBraidBimoduleFactorsEquiv k G i).symm t) = (TensorProduct.map (↑k (Submodule.subtype ((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i))) (↑k (Submodule.subtype ((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)))) t

Including the tensor factors gives the enveloping-algebra representative of the bimodule.

@[simp]

theorem TauCeti.coe_zigzagBraidBimoduleFactorsEquiv_symm_tmul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (x : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) (y : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) : ↑((zigzagBraidBimoduleFactorsEquiv k G i).symm (x ⊗ₜ[k] y)) = ↑x ⊗ₜ[k] ↑y

The inverse identifies a pure tensor of the two ideals with the same ambient pure tensor.

@[simp]

theorem TauCeti.zigzagBraidBimoduleFactorsEquiv_symm_map_smul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (a b : ↑(zigzagAlgebra k G)) (t : TensorProduct k ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i) ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) : (zigzagBraidBimoduleFactorsEquiv k G i).symm ((TensorProduct.map ((Algebra.lsmul k k ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) a) ((Algebra.lsmul k k ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) (MulOpposite.op b))) t) = a ⊗ₜ[k] MulOpposite.op b • (zigzagBraidBimoduleFactorsEquiv k G i).symm t

The inverse factor identification carries the two outer actions to the enveloping action.

theorem TauCeti.zigzagBraidBimoduleFactorsEquiv_tmul_smul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (a b : ↑(zigzagAlgebra k G)) (u : (zigzagGradedBraidBimodule k G i).carrier) : (zigzagBraidBimoduleFactorsEquiv k G i) (a ⊗ₜ[k] MulOpposite.op b • u) = (TensorProduct.map ((Algebra.lsmul k k ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) a) ((Algebra.lsmul k k ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) (MulOpposite.op b))) ((zigzagBraidBimoduleFactorsEquiv k G i) u)

The factor identification sends the enveloping action to the two factor actions.

@[simp]

theorem TauCeti.zigzagBraidBimoduleFactorsEquiv_symm_tmul_smul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (a : ↑(zigzagAlgebra k G)) (b : (↑(zigzagAlgebra k G))ᵐᵒᵖ) (x : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) (y : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) : a ⊗ₜ[k] b • (zigzagBraidBimoduleFactorsEquiv k G i).symm (x ⊗ₜ[k] y) = (zigzagBraidBimoduleFactorsEquiv k G i).symm ((a • x) ⊗ₜ[k] (b • y))

On pure ideal tensors, the two factor actions are the enveloping-algebra action.

noncomputable def TauCeti.zigzagBraidBimoduleVertexGenerator (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagGradedBraidBimodule k G i).carrier

The generator e_i ⊗ e_i of the vertex bimodule, given by the generators of its two idempotent-ideal factors.

theorem TauCeti.zigzagBraidBimoduleVertexGenerator_def (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : zigzagBraidBimoduleVertexGenerator k G i = (zigzagBraidBimoduleFactorsEquiv k G i).symm (spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ⊗ₜ[k] spanSingletonGenerator (MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)))

The vertex generator is the inverse factor identification of the two ideal generators.

theorem TauCeti.zigzagBraidBimoduleVertexGenerator_mem (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : zigzagBraidBimoduleVertexGenerator k G i ∈ (zigzagGradedBraidBimodule k G i).grading.piece ℤ 0

The vertex generator has internal degree zero.

noncomputable def TauCeti.zigzagBraidBimoduleRightFactorsEquiv (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) : (zigzagGradedBraidBimodule k G i).carrier ≃ₗ[k] TensorProduct k ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i) ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)

Identify the vertex bimodule with its two idempotent-ideal factors in the opposite order, the right ideal first. The right action of Z is then the action of Zᵐᵒᵖ on the first factor, the form in which balanced tensor products over Z act.

@[simp]

theorem TauCeti.zigzagBraidBimoduleRightFactorsEquiv_apply (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (u : (zigzagGradedBraidBimodule k G i).carrier) : (zigzagBraidBimoduleRightFactorsEquiv k G i) u = (TensorProduct.comm k ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i) ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) ((zigzagBraidBimoduleFactorsEquiv k G i) u)

The reversed factor identification is the factor identification followed by swapping the two factors.

theorem TauCeti.zigzagBraidBimoduleRightFactorsEquiv_op_smul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (a : ↑(zigzagAlgebra k G)) (m : (zigzagGradedBraidBimodule k G i).carrier) : (zigzagBraidBimoduleRightFactorsEquiv k G i) (MulOpposite.op a • m) = MulOpposite.op a • (zigzagBraidBimoduleRightFactorsEquiv k G i) m

The reversed factor identification carries the right action of Z on the vertex bimodule to the action of Zᵐᵒᵖ on the right-ideal factor. It is stated with the restricted Zᵐᵒᵖ action, the form BalancedTensorProduct.congr expects.

noncomputable def TauCeti.zigzagBraidTensorCornerEquiv (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i j : V) : (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)).carrier ≃ₗ[k] TensorProduct k (↥(cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j))) (TensorProduct k ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i) ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) j))

Extract the middle corner from the actual balanced product of two vertex bimodules.

@[simp]

theorem TauCeti.zigzagBraidTensorCornerEquiv_tmul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i j : V) (l : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) (r : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) (l' : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) j)) (r' : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) j)) : (zigzagBraidTensorCornerEquiv k G i j) (GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] r)) ((zigzagBraidBimoduleFactorsEquiv k G j).symm (l' ⊗ₜ[k] r'))) = (spanSingletonBalancedTensorProductEquivCorner k ⋯) (BalancedTensorProduct.tmul k (↑(zigzagAlgebra k G)) r l') ⊗ₜ[k] (l ⊗ₜ[k] r')

On pure vertex factors, middle-corner extraction multiplies the two inner factors.

@[simp]

theorem TauCeti.zigzagBraidTensorCornerEquiv_symm_tmul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i j : V) (x : ↥(cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j))) (l : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) (r : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) j)) : (zigzagBraidTensorCornerEquiv k G i j).symm (x ⊗ₜ[k] (l ⊗ₜ[k] r)) = GradedModuleCat.bimoduleTensorTmul (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] spanSingletonGenerator (MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)))) ((zigzagBraidBimoduleFactorsEquiv k G j).symm (⟨↑x, ⋯⟩ ⊗ₜ[k] r))

The inverse middle-corner map inserts the right generator of the first vertex ideal.

theorem TauCeti.zigzagBraidTensorCornerEquiv_tmul_smul (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i j : V) (a : ↑(zigzagAlgebra k G)) (b : (↑(zigzagAlgebra k G))ᵐᵒᵖ) (t : (GradedModuleCat.bimoduleTensorObj (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagAlgebraInternalGrading k G) (zigzagGradedBraidBimodule k G i) (zigzagGradedBraidBimodule k G j)).carrier) : (zigzagBraidTensorCornerEquiv k G i j) (a ⊗ₜ[k] b • t) = (TensorProduct.map LinearMap.id (TensorProduct.map ((Algebra.lsmul k k ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) a) ((Algebra.lsmul k k ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) j)) b))) ((zigzagBraidTensorCornerEquiv k G i j) t)

Middle-corner extraction carries enveloping scalars to the two outer ideal factors.

@[simp]

theorem TauCeti.zigzagBraidEvaluation_factors (k : Type u_1) [CommRing k] {V : Type u_2} (G : SimpleGraph V) [Finite V] (i : V) (l : ↥((fun (i : V) => Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i}) i)) (r : ↥((fun (i : V) => Ideal.span {MulOpposite.op ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)}) i)) : (Bimodule.of (AlgHom.id k ↑(zigzagAlgebra k G))).symm ((zigzagBraidEvaluation k G i) ((zigzagBraidBimoduleFactorsEquiv k G i).symm (l ⊗ₜ[k] r))) = ↑l * MulOpposite.unop ↑r

Evaluation on the left and right vertex factors is multiplication. The function type fixes the graded source and target module structures.