The square span component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.OrderedBasisIndex : Type

Ordered basis indices for the polynomial module. Paper: §2.

Equations

• Connes.Construction.PaperKernel.OrderedBasisIndex = Lex (Fin 3 × ℕ)

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.OrderedTensorIndex : Type

Ordered basis indices for the tensor square. Paper: §2.

Equations

• Connes.Construction.PaperKernel.OrderedTensorIndex = Lex (Connes.Construction.PaperKernel.OrderedBasisIndex × Connes.Construction.PaperKernel.OrderedBasisIndex)

noncomputable def Connes.Construction.PaperKernel.orderedBasis : Module.Basis OrderedBasisIndex k A

The ordered monomial basis of the polynomial module. Paper: §2.

Equations

• Connes.Construction.PaperKernel.orderedBasis = (Pi.basis fun (x : Fin 3) => Polynomial.basisMonomials Connes.Construction.k).reindex ((Equiv.sigmaEquivProd (Fin 3) ℕ).trans toLex)

noncomputable def Connes.Construction.PaperKernel.orderedTensorBasis : Module.Basis OrderedTensorIndex k TensorAA

The ordered tensor basis used for coefficient involution. Paper: §2.

Equations

• Connes.Construction.PaperKernel.orderedTensorBasis = (Connes.Construction.PaperKernel.orderedBasis.tensorProduct Connes.Construction.PaperKernel.orderedBasis).reindex toLex

def Connes.Construction.PaperKernel.swapIndex (p : OrderedTensorIndex) : OrderedTensorIndex

The index involution induced by tensor flip. Paper: §2.

Equations

• Connes.Construction.PaperKernel.swapIndex p = toLex (ofLex p).swap

theorem Connes.Construction.PaperKernel.swapIndex_involutive (p : OrderedTensorIndex) : swapIndex (swapIndex p) = p

The flip involution on ordered tensor indices is self-inverse. Paper: §2.

noncomputable def Connes.Construction.PaperKernel.coeffMap (i j : OrderedBasisIndex) : TensorAA →ₗ[k] k

Coordinate extraction in the ordered tensor basis. Paper: §2.

Equations

• Connes.Construction.PaperKernel.coeffMap i j = Finsupp.lapply (toLex (i, j)) ∘ₗ ↑Connes.Construction.PaperKernel.orderedTensorBasis.repr

theorem Connes.Construction.PaperKernel.coeffMap_flip (x : TensorAA) (i j : OrderedBasisIndex) : (coeffMap i j) ((TensorProduct.comm k A A) x) = (coeffMap j i) x

Flip exchanges the two ordered tensor coordinates. Paper: §2.

theorem Connes.Construction.PaperKernel.coeff_flip (x : TensorAA) (p : OrderedTensorIndex) : (orderedTensorBasis.repr ((TensorProduct.comm k A A) x)) p = (orderedTensorBasis.repr x) (swapIndex p)

Flip exchanges ordered tensor-basis coefficients. Paper: §2.

theorem Connes.Construction.PaperKernel.pair_mem_squareSpan (i j : OrderedBasisIndex) : orderedBasis i ⊗ₜ[k] orderedBasis j + orderedBasis j ⊗ₜ[k] orderedBasis i ∈ squareSpan

Off-diagonal basis pairs lie in the square span. Paper: §2.

theorem Connes.Construction.PaperKernel.basis_expansion (x : TensorAA) : x = ∑ p ∈ (orderedTensorBasis.repr x).support, (orderedTensorBasis.repr x) p • orderedTensorBasis p

The expansion of a tensor in the ordered tensor basis. Paper: §2.

def Connes.Construction.PaperKernel.diagonalIndex (p : OrderedTensorIndex) : Prop

The diagonal predicate on ordered tensor indices. Paper: §2.

Equations

• Connes.Construction.PaperKernel.diagonalIndex p = ((ofLex p).1 = (ofLex p).2)

def Connes.Construction.PaperKernel.offDiagonalIndex (p : OrderedTensorIndex) : Prop

The off-diagonal predicate on ordered tensor indices. Paper: §2.

Equations

• Connes.Construction.PaperKernel.offDiagonalIndex p = ((ofLex p).1 ≠ (ofLex p).2)

theorem Connes.Construction.PaperKernel.swapIndex_offDiagonal {p : OrderedTensorIndex} (hp : offDiagonalIndex p) : offDiagonalIndex (swapIndex p)

Swapping preserves the off-diagonal predicate. Paper: §2.

theorem Connes.Construction.PaperKernel.swapIndex_ne_self_of_offDiagonal {p : OrderedTensorIndex} (hp : offDiagonalIndex p) : swapIndex p ≠ p

An off-diagonal index is not fixed by swapping. Paper: §2.

theorem Connes.Construction.PaperKernel.repr_swap_eq (c : ↥C) (p : OrderedTensorIndex) : (orderedTensorBasis.repr ↑c) (swapIndex p) = (orderedTensorBasis.repr ↑c) p

Fixed tensors have swap-symmetric ordered coefficients. Paper: §2.

theorem Connes.Construction.PaperKernel.basis_mem_squareSpan_of_diagonal {p : OrderedTensorIndex} (hp : diagonalIndex p) : orderedTensorBasis p ∈ squareSpan

A diagonal tensor-basis vector lies in the square span. Paper: §2.

theorem Connes.Construction.PaperKernel.coeff_pair_mem_squareSpan (c : ↥C) (p : OrderedTensorIndex) : (orderedTensorBasis.repr ↑c) p • orderedTensorBasis p + (orderedTensorBasis.repr ↑c) (swapIndex p) • orderedTensorBasis (swapIndex p) ∈ squareSpan

Coefficient-symmetric basis pairs lie in the square span. Paper: §2.

theorem Connes.Construction.PaperKernel.repr_support_swap_mem (c : ↥C) {p : OrderedTensorIndex} (hp : p ∈ (orderedTensorBasis.repr ↑c).support) : swapIndex p ∈ (orderedTensorBasis.repr ↑c).support

Flip symmetry preserves the finite coefficient support. Paper: §2.

theorem Connes.Construction.PaperKernel.concreteSquareSpanData : SquareSpanData

The Zhou fixed tensor module is spanned by square tensors. Paper: §2.