Bases of zigzag component algebras

Each connected-component factor has a vertex--arrow--volume basis. On a component with an edge this is the basis of the relation quotient. On a singleton component the vertex and volume vectors are the unit and infinitesimal generator of the dual numbers. In particular the index type is uniform across both cases, and the volume vector at an isolated vertex is not zero.

The construction uses Mathlib's two-coordinate basis and transport of bases along linear equivalences. See Huerfano--Khovanov, A category for the adjoint representation, Section 3, for the singleton convention.

noncomputable def TauCeti.zigzagComponentBasis (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) : Module.Basis (ZigzagBasisIndex C.toSimpleGraph) k ↑(zigzagComponentAlgebra k G C)

The vertex--arrow--volume basis of one connected-component factor. Singleton factors use 1 and DualNumber.eps for the vertex and volume, respectively.

@[simp]

theorem TauCeti.zigzagComponentAlgebraEquivNonisolated_zigzagComponentBasis (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Nontrivial ↥C] (hns : ∀ (i : ↥C), ∃ (j : ↥C), C.toSimpleGraph.Adj i j) (b : ZigzagBasisIndex C.toSimpleGraph) : (zigzagComponentAlgebraEquivNonisolated k G C) ((zigzagComponentBasis k G C) b) = (zigzagBasis k C.toSimpleGraph hns) b

On a component with an edge the component basis maps to the relation-quotient basis.

@[simp]

theorem TauCeti.zigzagComponentBasis_repr_nonisolated (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Nontrivial ↥C] (hns : ∀ (i : ↥C), ∃ (j : ↥C), C.toSimpleGraph.Adj i j) (x : ↑(zigzagComponentAlgebra k G C)) (b : ZigzagBasisIndex C.toSimpleGraph) : ((zigzagComponentBasis k G C).repr x) b = ((zigzagBasis k C.toSimpleGraph hns).repr ((zigzagComponentAlgebraEquivNonisolated k G C) x)) b

Coordinates on a component with an edge are the relation-quotient coordinates.

@[simp]

theorem TauCeti.zigzagComponentAlgebraEquivULiftDualNumber_zigzagComponentBasis_inl (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Subsingleton ↥C] (i : ↥C) : (zigzagComponentAlgebraEquivULiftDualNumber k G C) ((zigzagComponentBasis k G C) (Sum.inl i)) = 1

On a singleton component the vertex basis vector maps to the dual-number unit.

@[simp]

theorem TauCeti.zigzagComponentAlgebraEquivULiftDualNumber_zigzagComponentBasis_inr_inr (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Subsingleton ↥C] (i : ↥C) : (zigzagComponentAlgebraEquivULiftDualNumber k G C) ((zigzagComponentBasis k G C) (Sum.inr (Sum.inr i))) = { down := DualNumber.eps }

On a singleton component the volume basis vector maps to the infinitesimal generator.

@[simp]

theorem TauCeti.zigzagComponentBasis_repr_inl_of_subsingleton (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Subsingleton ↥C] (x : ↑(zigzagComponentAlgebra k G C)) (i : ↥C) : ((zigzagComponentBasis k G C).repr x) (Sum.inl i) = TrivSqZeroExt.fst ((zigzagComponentAlgebraEquivULiftDualNumber k G C) x).down

The vertex coordinate on a singleton factor is its scalar coefficient.

@[simp]

theorem TauCeti.zigzagComponentBasis_repr_inr_inr_of_subsingleton (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Subsingleton ↥C] (x : ↑(zigzagComponentAlgebra k G C)) (i : ↥C) : ((zigzagComponentBasis k G C).repr x) (Sum.inr (Sum.inr i)) = TrivSqZeroExt.snd ((zigzagComponentAlgebraEquivULiftDualNumber k G C) x).down

The volume coordinate on a singleton factor is its infinitesimal coefficient.