Nondegeneracy from the snake identities

A form b : V ⊗ V ⟶ 𝟙 admitting a copairing C : 𝟙 ⟶ V ⊗ V with the two snake identities has nondegenerate blocks — the hypothesis shape produced by rigidity, and the hypothesis shape consumed by exists_coordinates.

The route: writing the copairing's even element as a pair of finite sums of pure tensors (TensorProduct.exists_finset), the two snake identities evaluated on generators become four contraction identities (exists_contraction_families):

• ∀ x, Σ_{(m,n)} b(x, m) • n = x and ∀ x, Σ_{(m,n)} b(n, x) • m = x on the even block,
• the same two identities on the odd block.

Each identity forces the corresponding separation property, so the even block separates on the left and the odd block is nondegenerate (blocks_nondegenerate_of_snake), and the graded coordinate identification follows unconditionally (exists_coordinates_of_snake).

Reduced views of the remaining morphism components

def RS.formOddMap {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) : TensorProduct ℂ V.even V.odd × TensorProduct ℂ V.odd V.even →ₗ[ℂ] PUnit.{1}

The odd component of a form morphism, with its domain and codomain presented in reduced form.

Equations

• RS.formOddMap b = b.oddMap

def RS.formCoevMap {V : SuperVect} (C : SuperVect.tensorUnit.Hom (V.tensorObj V)) : ℂ →ₗ[ℂ] TensorProduct ℂ V.even V.even × TensorProduct ℂ V.odd V.odd

The even component of a copairing morphism 𝟙 ⟶ V ⊗ V, with its domain and codomain presented in reduced form.

Equations

• RS.formCoevMap C = C.evenMap

def RS.formCoevOddMap {V : SuperVect} (C : SuperVect.tensorUnit.Hom (V.tensorObj V)) : PUnit.{1} →ₗ[ℂ] TensorProduct ℂ V.even V.odd × TensorProduct ℂ V.odd V.even

The odd component of a copairing morphism, with its domain and codomain presented in reduced form.

Equations

• RS.formCoevOddMap C = C.oddMap

The contraction identities

The sum-shuffling these proofs run on -- pushing a finite sum through a bound map, splitting it across the summands of a product -- is Common/ProdSum.lean; the maps there are bound so that instance search never meets a metavariable.

theorem RS.exists_contraction_families {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (C : SuperVect.tensorUnit.Hom (V.tensorObj V)) (h1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (have this := C; this)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V V V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := b; this) V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).inv) (h2 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := C; this) V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V V V).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (have this := b; this))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv) : ∃ (S : Finset (V.even × V.even)) (T : Finset (V.odd × V.odd)), ((formCoevMap C) 1).1 = ∑ i ∈ S, i.1 ⊗ₜ[ℂ] i.2 ∧ ((formCoevMap C) 1).2 = ∑ i ∈ T, i.1 ⊗ₜ[ℂ] i.2 ∧ (∀ (x : V.even), ∑ i ∈ S, ((formEvenBlock b) x) i.1 • i.2 = x) ∧ (∀ (x : V.even), ∑ i ∈ S, ((formEvenBlock b) i.2) x • i.1 = x) ∧ (∀ (x : V.odd), ∑ i ∈ T, ((formOddBlock b) x) i.1 • i.2 = x) ∧ ∀ (x : V.odd), ∑ i ∈ T, ((formOddBlock b) i.2) x • i.1 = x

Contraction families from the snake identities (accompanying paper §5.2): the even copairing element decomposes as finite sums of pure tensors over each graded block, and the two snake identities become the four contraction identities relating those families to the blocks of the form.

Nondegeneracy of the blocks

theorem RS.blocks_nondegenerate_of_snake {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (C : SuperVect.tensorUnit.Hom (V.tensorObj V)) (h1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (have this := C; this)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V V V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := b; this) V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).inv) (h2 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := C; this) V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V V V).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (have this := b; this))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv) : (∀ (x : V.even), (∀ (y : V.even), ((formEvenBlock b) x) y = 0) → x = 0) ∧ (formOddBlock b).Nondegenerate

Nondegeneracy from the snake identities: the even block separates on the left and the odd block is nondegenerate — exactly the hypotheses of exists_coordinates.

The unconditional coordinate identification

theorem RS.exists_coordinates_of_snake {V : SuperVect} (b : (V.tensorObj V).Hom SuperVect.tensorUnit) (C : SuperVect.tensorUnit.Hom (V.tensorObj V)) (hb : b.comp (V.koszulBraiding V) = b) (h1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (have this := C; this)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V V V).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := b; this) V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).inv) (h2 : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (have this := C; this) V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator V V V).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft V (have this := b; this))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor V).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor V).inv) : ∃ (k : ℕ) (ℓ : ℕ) (eE : (Fin k → ℂ) ≃ₗ[ℂ] V.even) (eO : (Fin (2 * ℓ) → ℂ) ≃ₗ[ℂ] V.odd), (∀ (x y : Fin k → ℂ), ((formEvenBlock b) (eE x)) (eE y) = stdFormEven k x y) ∧ ∀ (x y : Fin (2 * ℓ) → ℂ), ((formOddBlock b) (eO x)) (eO y) = stdFormOdd ℓ x y

Standard coordinates from rigidity (accompanying paper §5.1): a super vector space with a supersymmetric form admitting a copairing with the snake identities carries graded coordinates taking the form's blocks to the standard forms.