Uniqueness of the copairing

The snake identities determine the copairing (accompanying paper §5.2): any copairing for the standard form equals stdCopair.

The engine is the contraction operator of a bilinear form, contractionMap B : M ⊗ N →ₗ (M →ₗ N), sending m ⊗ n to x ↦ B(x, m) • n. The contraction identities say exactly that the copairing's blocks are sent to the identity; the operator is injective for a nondegenerate form on a finite-dimensional space (dualTensorHom is bijective, and the form identifies the space with its dual), so the blocks are pinned to the standard copairing elements, which satisfy the same identities.

The contraction operator

def RS.contractionMap {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℂ M] [AddCommGroup N] [Module ℂ N] (B : LinearMap.BilinForm ℂ M) : TensorProduct ℂ M N →ₗ[ℂ] M →ₗ[ℂ] N

The left contraction operator of a bilinear form: m ⊗ n ↦ (x ↦ B(x, m) • n).

Equations

• RS.contractionMap B = dualTensorHom ℂ M N ∘ₗ TensorProduct.map (LinearMap.flip B) LinearMap.id

theorem RS.contractionMap_tmul {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℂ M] [AddCommGroup N] [Module ℂ N] (B : LinearMap.BilinForm ℂ M) (m : M) (n : N) (x : M) : ((contractionMap B) (m ⊗ₜ[ℂ] n)) x = (B x) m • n

The contraction operator on a pure tensor.

theorem RS.contractionMap_injective {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module ℂ M] [FiniteDimensional ℂ M] [AddCommGroup N] [Module ℂ N] (B : LinearMap.BilinForm ℂ M) (hB : B.Nondegenerate) : Function.Injective ⇑(contractionMap B)

The contraction operator of a nondegenerate form on a finite-dimensional space is injective: the form identifies the space with its dual, and dualTensorHom is bijective.

Nondegeneracy of the standard bilinear forms

theorem RS.stdFormEvenBilin_nondegenerate (k : ℕ) : (stdFormEvenBilin k).Nondegenerate

The standard even form is nondegenerate, so its contraction operator is injective.

theorem RS.stdFormOddBilin_nondegenerate (ℓ : ℕ) : (stdFormOddBilin ℓ).Nondegenerate

The standard odd form is nondegenerate too.

The standard copairing contracts to the identity

theorem RS.contractionMap_stdCopairEvenElem (k : ℕ) (x : Fin k → ℂ) : ((contractionMap (stdFormEvenBilin k)) (stdCopairEvenElem k)) x = x

The standard even copairing element contracts to the identity — it satisfies the even contraction identity.

theorem RS.stdFormOdd_stdF_right (ℓ : ℕ) (x : Fin (2 * ℓ) → ℂ) (m : Fin (2 * ℓ)) : stdFormOdd ℓ x (stdF ℓ m) = ↑(oddPartnerSign ℓ m) * x (oddPartner ℓ m)

The standard odd form against a basis vector on the right: b(x, f_m) = s_m · x_{p(m)}.

theorem RS.contractionMap_stdCopairOddElem (ℓ : ℕ) (x : Fin (2 * ℓ) → ℂ) : ((contractionMap (stdFormOddBilin ℓ)) (stdCopairOddElem ℓ)) x = x

And the odd element satisfies the odd one.

The standard form's blocks

theorem RS.formEvenBlock_stdForm (k ℓ : ℕ) (x y : Fin k → ℂ) : ((formEvenBlock (stdForm k ℓ)) x) y = stdFormEven k x y

The standard form's even block is the standard even form.

theorem RS.formOddBlock_stdForm (k ℓ : ℕ) (x y : Fin (2 * ℓ) → ℂ) : ((formOddBlock (stdForm k ℓ)) x) y = stdFormOdd ℓ x y

And its odd block the standard odd form.

Uniqueness

theorem RS.stdCopair_unique (k ℓ : ℕ) (C' : SuperVect.tensorUnit.Hom ((stdSuperPair k ℓ).tensorObj (stdSuperPair k ℓ))) (h1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (stdSuperPair k ℓ) (have this := C'; this)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (stdSuperPair k ℓ) (stdSuperPair k ℓ) (stdSuperPair k ℓ)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := stdForm k ℓ; this) (stdSuperPair k ℓ))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (stdSuperPair k ℓ)).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor (stdSuperPair k ℓ)).inv) (h2 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := C'; this) (stdSuperPair k ℓ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (stdSuperPair k ℓ) (stdSuperPair k ℓ) (stdSuperPair k ℓ)).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (stdSuperPair k ℓ) (have this := stdForm k ℓ; this))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (stdSuperPair k ℓ)).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor (stdSuperPair k ℓ)).inv) : C' = stdCopair k ℓ

Uniqueness of the copairing (accompanying paper §5.2): any copairing satisfying the snake identities against the standard form is the standard copairing.