Zhou's construction of the two groups in §2. The concrete tensor kernel, retraction, acting group, and semidirect-product boundary follow the paper. This file contains no declaration block recorded as a code transfer; its public code dependencies are attributed in their defining modules.

@[reducible, inline]

abbrev Connes.Construction.k : Type

Characteristic-two scalar field. Paper: §2.

Equations

• Connes.Construction.k = ZMod 2

@[reducible, inline]

abbrev Connes.Construction.R : Type

Polynomial coefficient ring. Paper: §2.

Equations

• Connes.Construction.R = Polynomial Connes.Construction.k

@[reducible, inline]

abbrev Connes.Construction.A : Type

Polynomial module for the construction. Paper: §2.

Equations

• Connes.Construction.A = (Fin 3 → Connes.Construction.R)

@[reducible, inline]

abbrev Connes.Construction.H : Type

Acting-group carrier. Paper: §2.

Equations

• Connes.Construction.H = (Connes.SpecialLinear.SL3 × ↥Connes.Sp4.Group)

noncomputable def Connes.Construction.actingGroup : CountableDiscreteGroup

Countable discrete wrapper for the acting group. Paper: §2.

Equations

• Connes.Construction.actingGroup = { Carrier := Connes.Construction.H, group := inferInstance, countable := Connes.Construction.actingGroup._proof_1 }

instance Connes.Construction.PaperKernel.tensorCountable {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] [Countable M] [Countable N] : Countable (TensorProduct k M N)

Countability of tensor products with countable factors. Paper: §2.

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.TensorAA : Type

Tensor square used by the paper's symmetric kernel. Paper: §2.

Equations

• Connes.Construction.PaperKernel.TensorAA = TensorProduct Connes.Construction.k Connes.Construction.A Connes.Construction.A

instance Connes.Construction.PaperKernel.tensorAACountable : Countable TensorAA

Countability of the tensor square. Paper: §2.

noncomputable def Connes.Construction.PaperKernel.flip : TensorAA ≃ₗ[k] TensorAA

Flip on the tensor square. Paper: §2.

Equations

• Connes.Construction.PaperKernel.flip = TensorProduct.comm Connes.Construction.k Connes.Construction.A Connes.Construction.A

def Connes.Construction.PaperKernel.C : Submodule k TensorAA

Flip-fixed symmetric tensor module. Paper: §2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Connes.Construction.PaperKernel.diagonal (a : A) : ↥C

Diagonal element of the paper's symmetric tensor module. Paper: §2.

Equations

• Connes.Construction.PaperKernel.diagonal a = ⟨a ⊗ₜ[Connes.Construction.k] a, ⋯⟩

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.PaperV : Type

Matrix-indexed finite symplectic module. Paper: §2.

Equations

• Connes.Construction.PaperKernel.PaperV = Connes.OpenAIPort.ModTwoSpace

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.VStar : Type

Dual of the finite symplectic module. Paper: §2.

Equations

• Connes.Construction.PaperKernel.VStar = (Connes.Construction.PaperKernel.PaperV →ₗ[Connes.Construction.k] Connes.Construction.k)

instance Connes.Construction.PaperKernel.vStarCountable : Countable VStar

Countability of the finite dual module. Paper: §2.

noncomputable def Connes.Construction.PaperKernel.hadamard (p q : R) : R

Coefficientwise product on the polynomial module. Paper: §2.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Connes.Construction.PaperKernel.coeff_hadamard (p q : R) (n : ℕ) : Polynomial.coeff (hadamard p q) n = Polynomial.coeff p n * Polynomial.coeff q n

Coefficient formula for the polynomial module product. Paper: §2.

theorem Connes.Construction.PaperKernel.hadamard_add_left (p q r : R) : hadamard (p + q) r = hadamard p r + hadamard q r

Additivity of the first coefficientwise product input. Paper: §2.

theorem Connes.Construction.PaperKernel.hadamard_add_right (p q r : R) : hadamard p (q + r) = hadamard p q + hadamard p r

Additivity of the second coefficientwise product input. Paper: §2.

theorem Connes.Construction.PaperKernel.hadamard_smul_left (c : k) (p q : R) : hadamard (c • p) q = c • hadamard p q

Scalar compatibility of the first coefficientwise product input. Paper: §2.

theorem Connes.Construction.PaperKernel.hadamard_smul_right (c : k) (p q : R) : hadamard p (c • q) = c • hadamard p q

Scalar compatibility of the second coefficientwise product input. Paper: §2.

theorem Connes.Construction.PaperKernel.hadamard_square (p : R) : hadamard p p = p

Squaring for the coefficientwise product over the Boolean field. Paper: §2.

noncomputable def Connes.Construction.PaperKernel.coordHadamard (a b : A) : A

Coordinatewise coefficientwise product on the polynomial module. Paper: §2.

Equations

• Connes.Construction.PaperKernel.coordHadamard a b i = Connes.Construction.PaperKernel.hadamard (a i) (b i)

noncomputable def Connes.Construction.PaperKernel.coordHadamardLinear : A →ₗ[k] A →ₗ[k] A

Bilinear map used to construct the paper retraction. Paper: §2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Connes.Construction.PaperKernel.deltaTensor : TensorAA →ₗ[k] A

Linear map on the tensor square underlying the paper retraction. Paper: §2.

Equations

• Connes.Construction.PaperKernel.deltaTensor = TensorProduct.lift Connes.Construction.PaperKernel.coordHadamardLinear

noncomputable def Connes.Construction.PaperKernel.delta : ↥C →ₗ[k] A

Equivariant-retraction candidate on the flip-fixed tensor module. Paper: §2.

Equations

• Connes.Construction.PaperKernel.delta = Connes.Construction.PaperKernel.deltaTensor.domRestrict Connes.Construction.PaperKernel.C

theorem Connes.Construction.PaperKernel.delta_diagonal (a : A) : delta (diagonal a) = a

The retraction returns the original vector on diagonal tensors. Paper: §2.

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.AVStar : Type

First summand of the paper's abelian kernel. Paper: §2.

Equations

• Connes.Construction.PaperKernel.AVStar = TensorProduct Connes.Construction.k Connes.Construction.A Connes.Construction.PaperKernel.VStar

instance Connes.Construction.PaperKernel.avStarCountable : Countable AVStar

Countability of the tensor-dual summand. Paper: §2.

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.D : Type

Binary product presentation of the paper's direct-sum kernel. Paper: §2.

Equations

• Connes.Construction.PaperKernel.D = (Connes.Construction.PaperKernel.AVStar × ↥Connes.Construction.PaperKernel.C)

instance Connes.Construction.PaperKernel.dCountable : Countable D

Countability of the paper-shaped kernel. Paper: §2.

instance Connes.Construction.PaperKernel.paperGammaKernelCountable : Countable (Multiplicative D)

Countability of the multiplicative paper-shaped kernel. Paper: §2.

@[reducible, inline]

abbrev Connes.Construction.PaperKernel.paperGammaCarrier (action : H →* MulAut (Multiplicative D)) : Type

Carrier of the paper-shaped semidirect group associated to a kernel action. Paper: §2.

Equations

• Connes.Construction.PaperKernel.paperGammaCarrier action = (Multiplicative Connes.Construction.PaperKernel.D ⋊[action] Connes.Construction.H)

@[reducible, inline]

noncomputable abbrev Connes.Construction.PaperKernel.paperGammaOf (action : H →* MulAut (Multiplicative D)) : CountableDiscreteGroup

Paper-shaped semidirect group associated to a kernel action. Paper: §2.

Equations

• Connes.Construction.PaperKernel.paperGammaOf action = { Carrier := Connes.Construction.PaperKernel.paperGammaCarrier action, group := inferInstance, countable := ⋯ }