Concrete orbit and displacement proofs for Zhou's semidirect products. The finite quotient detector is checked by kernel computation over the public finite carrier. Paper: §5.

noncomputable def Connes.PaperICC.paperVBasis : Module.Basis Construction.PaperKernel.SymplecticIndex Construction.k Construction.PaperKernel.PaperV

Coordinate basis for the finite symplectic module. Paper: §2.

Equations

• Connes.PaperICC.paperVBasis = Pi.basisFun Connes.Construction.k Connes.Construction.PaperKernel.SymplecticIndex

noncomputable def Connes.PaperICC.paperVStarBasis : Module.Basis Construction.PaperKernel.SymplecticIndex Construction.k Construction.PaperKernel.VStar

Dual coordinate basis for the finite symplectic module. Paper: §2.

Equations

• Connes.PaperICC.paperVStarBasis = Connes.PaperICC.paperVBasis.dualBasis

theorem Connes.PaperICC.paper_avStar_coeff_sl3 (s : SpecialLinear.SL3) (u : Construction.PaperKernel.AVStar) (i : Construction.PaperKernel.SymplecticIndex) : ((TensorProduct.equivFinsuppOfBasisRight paperVStarBasis) ((Construction.PaperKernel.avStarAction s 1) u)) i = (Construction.PaperKernel.sl3AAction s) (((TensorProduct.equivFinsuppOfBasisRight paperVStarBasis) u) i)

theorem Connes.PaperICC.paper_avStar_coeff_exists (u : Construction.PaperKernel.AVStar) (hu : u ≠ 0) : ∃ (i : Construction.PaperKernel.SymplecticIndex), ((TensorProduct.equivFinsuppOfBasisRight paperVStarBasis) u) i ≠ 0

theorem Connes.PaperICC.paper_ordered_coord_transvection_invariant {p : Construction.PaperKernel.OrderedBasisIndex} {i j : Fin 3} (hij : i ≠ j) (hr : i ≠ (ofLex p).1) (a : SpecialLinear.R) (x : Construction.A) : (Construction.PaperKernel.orderedBasis.coord p) ((Construction.PaperKernel.sl3AAction (Matrix.SpecialLinearGroup.transvection hij a)) x) = (Construction.PaperKernel.orderedBasis.coord p) x

theorem Connes.PaperICC.paper_A_transvection_injective {i j : Fin 3} (hij : i ≠ j) (x : Construction.A) (hj : x j ≠ 0) : Function.Injective fun (a : SpecialLinear.R) => (Construction.PaperKernel.sl3AAction (Matrix.SpecialLinearGroup.transvection hij a)) x

theorem Connes.PaperICC.paper_A_transvection_injective_avoiding (x : Construction.A) (hx : x ≠ 0) (r : Fin 3) : ∃ (i : Fin 3) (j : Fin 3) (hij : i ≠ j), i ≠ r ∧ Function.Injective fun (a : SpecialLinear.R) => (Construction.PaperKernel.sl3AAction (Matrix.SpecialLinearGroup.transvection hij a)) x

noncomputable def Connes.PaperICC.paperContractRight (φ : Construction.A →ₗ[Construction.k] Construction.k) : Construction.PaperKernel.TensorAA →ₗ[Construction.k] Construction.A

The paperContractRight construction used in the Connes rigidity formalization.

Equations

• Connes.PaperICC.paperContractRight φ = TensorProduct.lift (LinearMap.mk₂ Connes.Construction.k (fun (a b : Connes.Construction.A) => φ b • a) ⋯ ⋯ ⋯ ⋯)

@[simp]

theorem Connes.PaperICC.paperContractRight_tmul (φ : Construction.A →ₗ[Construction.k] Construction.k) (a b : Construction.A) : (paperContractRight φ) (a ⊗ₜ[Construction.k] b) = φ b • a

theorem Connes.PaperICC.paperContractRight_basisCoord (p : Construction.PaperKernel.OrderedBasisIndex) (x : Construction.PaperKernel.TensorAA) : (paperContractRight (Construction.PaperKernel.orderedBasis.coord p)) x = ((TensorProduct.equivFinsuppOfBasisRight Construction.PaperKernel.orderedBasis) x) p

theorem Connes.PaperICC.paperContractRight_equivariant {p : Construction.PaperKernel.OrderedBasisIndex} {i j : Fin 3} (hij : i ≠ j) (hr : (ofLex p).1 ≠ i) (a : SpecialLinear.R) (x : Construction.PaperKernel.TensorAA) : (paperContractRight (Construction.PaperKernel.orderedBasis.coord p)) ((Construction.PaperKernel.sl3TensorAction (Matrix.SpecialLinearGroup.transvection hij a)) x) = (Construction.PaperKernel.sl3AAction (Matrix.SpecialLinearGroup.transvection hij a)) ((paperContractRight (Construction.PaperKernel.orderedBasis.coord p)) x)

theorem Connes.PaperICC.paper_C_orbit_infinite (c : ↥Construction.PaperKernel.C) (hc : c ≠ 0) : (Set.range fun (s : SpecialLinear.SL3) => (Construction.PaperKernel.sl3CAction s) c).Infinite

Infinite orbit of a nonzero fixed tensor. Paper: §5.

theorem Connes.PaperICC.paper_AVStar_orbit_infinite (u : Construction.PaperKernel.AVStar) (hu : u ≠ 0) : (Set.range fun (s : SpecialLinear.SL3) => (Construction.PaperKernel.avStarAction s 1) u).Infinite

Infinite orbit of a nonzero tensor-dual element. Paper: §5.

theorem Connes.PaperICC.paper_D_orbit_one (d : Construction.PaperKernel.D) (hd : d ≠ 0) : (Set.range fun (s : SpecialLinear.SL3) => (Construction.PaperKernel.paperThetaOneLinear (s, 1)) d).Infinite

Infinite kernel orbit for the first action in additive coordinates. Paper: §5.

theorem Connes.PaperICC.paper_D_orbit_two (d : Construction.PaperKernel.D) (hd : d ≠ 0) : (Set.range fun (s : SpecialLinear.SL3) => (Construction.PaperKernel.thetaTwoLinearMap (s, 1)) d).Infinite

Infinite kernel orbit for the second action in additive coordinates. Paper: §5.

def Connes.PaperICC.paperCoordStar (p : Construction.PaperKernel.SymplecticIndex) : Construction.PaperKernel.VStar

The paperCoordStar construction used in the Connes rigidity formalization.

Equations

• Connes.PaperICC.paperCoordStar p = { toFun := fun (v : Connes.Construction.PaperKernel.PaperV) => v p, map_add' := ⋯, map_smul' := ⋯ }

theorem Connes.PaperICC.paper_kernel_orbit_one (a : N) (ha : a ≠ 1) : (Set.range fun (s : SpecialLinear.SL3) => (Construction.PaperKernel.paperThetaOneHom (s, 1)) a).Infinite

Infinite multiplicative kernel orbit for the first action. Paper: §5.

theorem Connes.PaperICC.paper_kernel_orbit_two (a : N) (ha : a ≠ 1) : (Set.range fun (s : SpecialLinear.SL3) => (Construction.PaperKernel.paperThetaTwoHom (s, 1)) a).Infinite

Infinite multiplicative kernel orbit for the second action. Paper: §5.

theorem Connes.PaperICC.paper_tmul_star_ne_zero (f : Construction.PaperKernel.VStar) (hf : f ≠ 0) : Construction.PaperKernel.a0 ⊗ₜ[Construction.k] f ≠ 0

theorem Connes.PaperICC.paper_q_moved_coord (q : ↥Construction.PaperKernel.Q) (hq : q ≠ 1) : ∃ (p : Construction.PaperKernel.SymplecticIndex), (Construction.PaperKernel.qVStarActionHom q) (paperCoordStar p) ≠ paperCoordStar p

theorem Connes.PaperICC.paper_q_coord_difference_ne_zero (q : ↥Construction.PaperKernel.Q) (hq : q ≠ 1) : ∃ (f : Construction.PaperKernel.VStar), f ≠ 0 ∧ ∃ (p : Construction.PaperKernel.SymplecticIndex), f = (Construction.PaperKernel.qVStarActionHom q) (paperCoordStar p) + paperCoordStar p

theorem Connes.PaperICC.paper_thetaOne_q_zero (q : ↥Construction.PaperKernel.Q) (u : Construction.PaperKernel.AVStar) : (Construction.PaperKernel.paperThetaOneLinear (1, q)) (u, 0) = ((Construction.PaperKernel.avStarAction 1 q) u, 0)

theorem Connes.PaperICC.paper_thetaTwo_q_zero (q : ↥Construction.PaperKernel.Q) (u : Construction.PaperKernel.AVStar) : (Construction.PaperKernel.thetaTwoLinearMap (1, q)) (u, 0) = ((Construction.PaperKernel.avStarAction 1 q) u, 0)

theorem Connes.PaperICC.paper_q_displacement_one (q : ↥Construction.PaperKernel.Q) (hq : q ≠ 1) : ∃ (d : Construction.PaperKernel.D), d + (Construction.PaperKernel.paperThetaOneLinear (1, q)) d ≠ 0

theorem Connes.PaperICC.paper_q_displacement_two (q : ↥Construction.PaperKernel.Q) (hq : q ≠ 1) : ∃ (d : Construction.PaperKernel.D), d + (Construction.PaperKernel.thetaTwoLinearMap (1, q)) d ≠ 0

theorem Connes.PaperICC.paper_neg_eq_self (d : Construction.PaperKernel.D) : -d = d

theorem Connes.PaperICC.paper_q_mul_displacement_one (q : ↥Construction.PaperKernel.Q) (hq : q ≠ 1) : ∃ (a : N), a * ((Construction.PaperKernel.paperThetaOneHom (1, q)) a)⁻¹ ≠ 1 ∧ (Set.range fun (s : SpecialLinear.SL3) => (Construction.PaperKernel.paperThetaOneHom (s, 1)) (a * ((Construction.PaperKernel.paperThetaOneHom (1, q)) a)⁻¹)).Infinite

Nontrivial quotient displacement for the first action. Paper: §5.

theorem Connes.PaperICC.paper_q_mul_displacement_two (q : ↥Construction.PaperKernel.Q) (hq : q ≠ 1) : ∃ (a : N), a * ((Construction.PaperKernel.paperThetaTwoHom (1, q)) a)⁻¹ ≠ 1 ∧ (Set.range fun (s : SpecialLinear.SL3) => (Construction.PaperKernel.paperThetaTwoHom (s, 1)) (a * ((Construction.PaperKernel.paperThetaTwoHom (1, q)) a)⁻¹)).Infinite

Nontrivial quotient displacement for the second action. Paper: §5.

theorem Connes.PaperICC.paper_actionData_one : ActionData Construction.PaperKernel.paperThetaOneHom

ICC orbit data for the first Zhou action. Paper: §5.

theorem Connes.PaperICC.paper_actionData_two : ActionData Construction.PaperKernel.paperThetaTwoHom

ICC orbit data for the second Zhou action. Paper: §5.

theorem Connes.PaperICC.paper_gammaOne_icc : IsICC Construction.PaperKernel.paperGammaOne

The first concrete Zhou group is ICC. This is the public §5 endpoint.

theorem Connes.PaperICC.paper_gammaTwo_icc : IsICC Construction.PaperKernel.paperGammaTwo

The second concrete Zhou group is ICC. This is the public §5 endpoint.