Conjugation structure on a tensor species

i. Overview

Each index of a tensor carries a colour naming the representation it transforms in. A species already has the variance dual τ c, the colour an index must meet to contract. Conjugation adds a second involution, the conjugate colour bar c: the colour an index transforms in after complex conjugation. A spinor index is the textbook example: complex conjugation sends a left-handed Weyl spinor to a right-handed one, (ψ_α)* = ψ̄_α̇, so bar swaps the left- and right-handed colours while fixing a real vector colour. Variance is untouched, so bar commutes with τ. In an N=1 chiral sector bar swaps chiral and anti-chiral indices.

conjT conjugates a tensor at the basis level: star each coordinate in the species basis and place it at the conjugate colour. Reality and Hermiticity are stated through it: a tensor is real when conjugation fixes it, and a metric is Hermitian when conjugating it swaps its two indices.

Conjugation is intrinsic species data, not a detachable add-on: a ConjTensorSpecies is a TensorSpecies bundled (extends) with the conjugate-colour involution bar and the coherence the recipe needs. bar c shares basis labels with c (barIdx_eq) and the contraction coefficients survive star (conj_contrComm), which together make conjugation commute with contraction. conjT is then conj-semilinear, involutive, and commutes with contraction; the last makes reality and Hermiticity compatible with raising and lowering indices.

At the single-index level, conjEquiv : V c ≃ₛₗ V (bar c) realises this conjugation: it reads a vector's coordinates, conjugates them with ConjModule.starFinsupp, and re-seats them at the conjugate colour. It rests on the conjugate module ConjModule (Physlib.Mathematics.ConjModule), the same vectors with the scalar action twisted by conjugation (i acts as −i). Equipping the conjugate colours with such conjugate-module carriers is what makes a metric V c ⊗ V (bar c) → k genuinely bilinear and IsHermitian an honest conjugate-transpose.

ii. Key results

ConjTensorSpecies is a tensor species bundled with its conjugation.

ConjTensorSpecies.conjT is the conjugation of a tensor.

ConjTensorSpecies.conjT_conjT proves that conjugation is an involution.

ConjTensorSpecies.conjT_contrT proves that conjugation commutes with contraction.

ConjTensorSpecies.conjT_eq_permT_iff is the componentwise criterion for conjT t = permT σ h t', the workhorse for proving reality and Hermiticity conditions.

ConjTensorSpecies.conjEquiv is the single-slot conjugate-linear isomorphism V c ≃ₛₗ V (bar c).

ConjTensorSpecies.IsHermitian is the structural conjugate-transpose condition on a metric slot.

iii. Table of contents

A. The conjugation structure

B. The conjugation of vectors

C. Conjugation of tensors

D. The involution law

E. Commutation with contraction

F. Hermitian pairings

A. The conjugation structure

A ConjTensorSpecies bundles a TensorSpecies (extends) with the conjugation data. Conjugation is defined at the basis level, where it is "star the components" (§B). Four of the new fields are bookkeeping on colours and index sets, trivial to supply per instance: bar (the conjugate-colour involution), bar_involution, bar_tau (it commutes with τ), and barIdx_eq (a colour and its conjugate share basis labels). The one substantive field is conj_contrComm, that the contraction coefficients are unchanged by star; this is what makes conjugation commute with contraction (§D), and for a real (δ) contraction it is star δ = δ.

A tensor species bundled with a conjugation. Beyond the TensorSpecies it extends, it carries the conjugate-colour involution bar, the index-set identification barIdx_eq, and the contraction-coherence conj_contrComm. Also carries bar_involution and bar_tau (that bar is involutive and commutes with the variance dual).

The conjugate colour: the colour an index transforms in under complex conjugation; preserves variance (commutes with τ).

bar is an involution.

bar commutes with the variance dual τ.

Conjugation fixes the index set: the conjugate colour reuses the same basis labels. Conjugation conjugates components in an adapted basis; it never permutes labels, so the label sets of c and bar c coincide.

Conjugation is equivariant: it preserves the action of the group.

Conjugation is compatible with contraction at the basis level: star of the contraction coefficient at colour d equals the coefficient at the conjugate colour bar d, with basis labels carried over by barIdx_eq. For a real (δ) contraction this is star δ = δ.

B. The conjugation of vectors

conjEquiv is the conjugate-linear isomorphism V c ≃ₛₗ[starRingEnd k] V (bar c): read off the coordinates of a vector in the species basis, conjugate them (star), and re-seat them as the coordinates at the conjugate colour (the index sets agree by barIdx_eq). It is the single-slot shadow of conjT, packaged as a bundled equivalence so the Hermitian-metric layer can apply it to a metric slot. Semilinearity is built in via the coordinate star; invertibility is star's involutivity together with bar's.

The conjugate-linear slot isomorphism V c ≃ₛₗ[starRingEnd k] V (bar c): conjugate the coordinates in the species basis and relabel to the conjugate colour via barIdx_eq.

conjEquiv on a basis vector: b c i ↦ b (bar c) i (relabelled through barIdx_eq), since the basis coordinates of b c i are the indicator at i and star fixes 0 and 1.

C. Conjugation of tensors

We define the conjugation map conjT through its action on components, record that it conjugates components in place (componentMap_conjT), and show it is conj-semilinear and additive.

Reindex component labels of bar ∘ c back to c, slotwise via the cast barIdx_eq.

Conjugation of a tensor: conjugate the components and reindex the basis to the conjugate colours.