The paper action instances component of the Connes rigidity formalization.

theorem Connes.Construction.PaperKernel.transvection_action_apply_target {i j : Fin 3} (hij : i ≠ j) (a : SpecialLinear.R) (x : A) : (sl3AAction (Matrix.SpecialLinearGroup.transvection hij a)) x i = x i + a * x j

Target-coordinate formula for an elementary SL₃ transvection. Paper: §2.

theorem Connes.Construction.PaperKernel.transvection_action_apply_of_ne_target {i j r : Fin 3} (hij : i ≠ j) (hri : r ≠ i) (a : SpecialLinear.R) (x : A) : (sl3AAction (Matrix.SpecialLinearGroup.transvection hij a)) x r = x r

Off-target coordinates are fixed by an elementary SL₃ transvection. Paper: §2.

noncomputable def Connes.Construction.PaperKernel.avStarAction (l : SpecialLinear.SL3) (q : ↥Q) : AVStar ≃ₗ[k] AVStar

The linear action on the first summand of the paper kernel. Paper: §2.

Equations

• Connes.Construction.PaperKernel.avStarAction l q = TensorProduct.congr (Connes.Construction.PaperKernel.sl3AAction l) (Connes.Construction.PaperKernel.qVStarActionHom q)

noncomputable def Connes.Construction.PaperKernel.avStarActionHom : H →* AVStar ≃ₗ[k] AVStar

The first-summand action is a homomorphism. Paper: §2.

Equations

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

theorem Connes.Construction.PaperKernel.sl3TensorAction_mul (l m : SpecialLinear.SL3) : sl3TensorAction (l * m) = sl3TensorAction l ∘ₗ sl3TensorAction m

The SL₃ action on the fixed tensor module is invertible. Paper: §2.

theorem Connes.Construction.PaperKernel.sl3TensorAction_one : sl3TensorAction 1 = LinearMap.id

The identity law for the diagonal tensor action. Paper: §2.

theorem Connes.Construction.PaperKernel.sl3TensorAction_inv_comp (l : SpecialLinear.SL3) : sl3TensorAction l⁻¹ ∘ₗ sl3TensorAction l = LinearMap.id

The diagonal tensor action has inverse given by the inverse matrix. Paper: §2.

theorem Connes.Construction.PaperKernel.sl3TensorAction_comp_inv (l : SpecialLinear.SL3) : sl3TensorAction l ∘ₗ sl3TensorAction l⁻¹ = LinearMap.id

The inverse diagonal tensor action has the reverse composition law. Paper: §2.

theorem Connes.Construction.PaperKernel.sl3CAction_inv_comp (l : SpecialLinear.SL3) : sl3CAction l⁻¹ ∘ₗ sl3CAction l = LinearMap.id

The fixed-tensor action has inverse given by the inverse matrix. Paper: §2.

theorem Connes.Construction.PaperKernel.sl3CAction_comp_inv (l : SpecialLinear.SL3) : sl3CAction l ∘ₗ sl3CAction l⁻¹ = LinearMap.id

The reverse fixed-tensor action composition is the identity. Paper: §2.

noncomputable def Connes.Construction.PaperKernel.sl3CActionEquiv (l : SpecialLinear.SL3) : ↥C ≃ₗ[k] ↥C

The SL₃ action on the fixed tensor module is invertible. Paper: §2.

Equations

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

noncomputable def Connes.Construction.PaperKernel.sl3CActionHom : SpecialLinear.SL3 →* ↥C ≃ₗ[k] ↥C

The fixed-tensor action is a homomorphism. Paper: §2.

Equations

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

noncomputable def Connes.Construction.PaperKernel.paperThetaOneLinear (h : H) : D ≃ₗ[k] D

The first Zhou action as a linear equivalence of the kernel. Paper: §2.

Equations

• Connes.Construction.PaperKernel.paperThetaOneLinear h = (Connes.Construction.PaperKernel.avStarAction h.1 h.2).prodCongr (Connes.Construction.PaperKernel.sl3CActionEquiv h.1)

@[simp]

theorem Connes.Construction.PaperKernel.paperThetaOneLinear_apply (h : H) (d : D) : (paperThetaOneLinear h) d = ((avStarAction h.1 h.2) d.1, (sl3CAction h.1) d.2)

Pointwise form of the first Zhou action on the kernel splitting.

noncomputable def Connes.Construction.PaperKernel.additiveEquivToMulAut (e : D ≃ₗ[k] D) : MulAut (Multiplicative D)

Reinterpret a linear kernel equivalence as a multiplicative automorphism. Paper: §2.

Equations

• Connes.Construction.PaperKernel.additiveEquivToMulAut e = AddEquiv.toMultiplicative e.toAddEquiv

noncomputable def Connes.Construction.PaperKernel.paperThetaOneLinearHom : H →* D ≃ₗ[k] D

The first Zhou action as a linear homomorphism. Paper: §2.

Equations

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

noncomputable def Connes.Construction.PaperKernel.paperThetaOneHom : H →* MulAut (Multiplicative D)

The first Zhou action on the multiplicative kernel. Paper: §2.

Equations

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

theorem Connes.Construction.PaperKernel.quadraticDefectLinear_cocycle (p q : ↥Q) : OpenAIPort.quadraticDefectLinear (p * q) = (qVStarActionHom p) (OpenAIPort.quadraticDefectLinear q) + OpenAIPort.quadraticDefectLinear p

The finite quadratic-defect functional obeys the paper cocycle law. Paper: §2.

noncomputable def Connes.Construction.PaperKernel.thetaTwoTermMap (h : H) : ↥C →ₗ[k] AVStar

The correction term in the second Zhou action. Paper: §2.

Equations

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

@[simp]

theorem Connes.Construction.PaperKernel.thetaTwoTermMap_apply (h : H) (c : ↥C) : (thetaTwoTermMap h) c = delta ((sl3CAction h.1) c) ⊗ₜ[k] OpenAIPort.quadraticDefectLinear h.2

noncomputable def Connes.Construction.PaperKernel.thetaTwoLinearMap (h : H) : D →ₗ[k] D

The second Zhou action as a linear map. Paper: §2.

Equations

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

theorem Connes.Construction.PaperKernel.thetaTwoLinearMap_mul (h h' : H) : thetaTwoLinearMap (h * h') = thetaTwoLinearMap h ∘ₗ thetaTwoLinearMap h'

The second Zhou linear map composes according to the group law. Paper: §2.

theorem Connes.Construction.PaperKernel.thetaTwoLinearMap_one : thetaTwoLinearMap 1 = LinearMap.id

The identity law for the second Zhou linear map. Paper: §2.

noncomputable def Connes.Construction.PaperKernel.paperThetaTwoLinearEquiv (h : H) : D ≃ₗ[k] D

The second Zhou action as a linear equivalence. Paper: §2.

Equations

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

noncomputable def Connes.Construction.PaperKernel.paperThetaTwoLinearHom : H →* D ≃ₗ[k] D

The second Zhou action as a linear homomorphism. Paper: §2.

Equations

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

noncomputable def Connes.Construction.PaperKernel.paperThetaTwoHom : H →* MulAut (Multiplicative D)

The second Zhou action on the multiplicative kernel. Paper: §2.

Equations

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

noncomputable def Connes.Construction.PaperKernel.contractStar (ψ : VStar →ₗ[k] k) : AVStar →ₗ[k] A

Contract the finite-dual factor of A ⊗ V⋆. Paper: §2.

Equations

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

@[simp]

theorem Connes.Construction.PaperKernel.contractStar_tmul (ψ : VStar →ₗ[k] k) (a : A) (f : VStar) : (contractStar ψ) (a ⊗ₜ[k] f) = ψ f • a

noncomputable def Connes.Construction.PaperKernel.a0 : A

The constant-one polynomial used in the §4 detector and §§5–6 witnesses.

Equations

• Connes.Construction.PaperKernel.a0 x✝ = 1

theorem Connes.Construction.PaperKernel.a0_ne_zero : a0 ≠ 0

theorem Connes.Construction.PaperKernel.avStar_q_action (q : ↥Q) (f : VStar) : (avStarAction 1 q) (a0 ⊗ₜ[k] f) = a0 ⊗ₜ[k] (qVStarActionHom q) f

The finite quotient acts only on the dual tensor factor of a0 ⊗ f.

theorem Connes.Construction.PaperKernel.thetaTwoLinearMap_sl3 (s : SpecialLinear.SL3) (d : D) : (thetaTwoLinearMap (s, 1)) d = ((avStarAction s 1) d.1, (sl3CAction s) d.2)

The two Zhou actions agree on the SL₃ factor. This is part of the action construction, used independently by the §4 detector and §5 orbit arguments. Paper: §2.

@[reducible, inline]

noncomputable abbrev Connes.Construction.PaperKernel.paperGammaOne : CountableDiscreteGroup

Zhou's first concrete semidirect-product group. Paper: §2.

Equations

• Connes.Construction.PaperKernel.paperGammaOne = Connes.Construction.PaperKernel.paperGammaOf Connes.Construction.PaperKernel.paperThetaOneHom

@[reducible, inline]

noncomputable abbrev Connes.Construction.PaperKernel.paperGammaTwo : CountableDiscreteGroup

Zhou's second concrete semidirect-product group. Paper: §2.

Equations

• Connes.Construction.PaperKernel.paperGammaTwo = Connes.Construction.PaperKernel.paperGammaOf Connes.Construction.PaperKernel.paperThetaTwoHom