The module semisimple component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperModuleSemisimple.Q : Submonoid (Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) (ZMod 2))

The Q construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.Q = Connes.Construction.PaperKernel.Q

@[reducible, inline]

abbrev Connes.PaperModuleSemisimple.W : Type

The W construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.W = Connes.Construction.PaperKernel.VStar

def Connes.PaperModuleSemisimple.pairing : Construction.PaperKernel.PaperV →ₗ[Construction.k] W

The pairing construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperModuleSemisimple.pairing_injective : Function.Injective ⇑pairing

The symplectic pairing has trivial kernel. Paper: §6.

theorem Connes.PaperModuleSemisimple.pairing_surjective : Function.Surjective ⇑pairing

theorem Connes.PaperModuleSemisimple.pairing_smul (q : ↥Q) (d : Construction.PaperKernel.PaperV) : (Construction.PaperKernel.qVStarActionHom q) (pairing d) = pairing (q • d)

theorem Connes.PaperModuleSemisimple.qV_transitive_on_nonzero_test (v : Construction.PaperKernel.PaperV) : v ≠ 0 → ∀ (w : Construction.PaperKernel.PaperV), w ≠ 0 → ∃ (q : ↥Q), q • v = w

theorem Connes.PaperModuleSemisimple.qVStar_transitive_on_nonzero_test (f : W) : f ≠ 0 → ∀ (g : W), g ≠ 0 → ∃ (q : ↥Q), (Construction.PaperKernel.qVStarActionHom q) f = g

def Connes.PaperModuleSemisimple.qVStarRepresentation : Representation Construction.k (↥Q) W

The qVStarRepresentation construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperModuleSemisimple.qVStar_nontrivial : Nontrivial W

The finite dual representation is nontrivial. Paper: §6.

theorem Connes.PaperModuleSemisimple.qVStar_simple : IsSimpleModule PaperNonisomorphism.Ring qVStarRepresentation.asModule

@[reducible, inline]

abbrev Connes.PaperModuleSemisimple.I : Type

The I construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.I = Connes.Construction.PaperKernel.OrderedBasisIndex

@[reducible, inline]

abbrev Connes.PaperModuleSemisimple.AV : Type

The AV construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.AV = Connes.Construction.PaperKernel.AVStar

@[reducible, inline]

abbrev Connes.PaperModuleSemisimple.DS : Type

The DS construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.DS = DirectSum Connes.PaperModuleSemisimple.I fun (x : Connes.PaperModuleSemisimple.I) => Connes.PaperModuleSemisimple.W

noncomputable def Connes.PaperModuleSemisimple.avStarActionQEquivHom : ↥Q →* AV ≃ₗ[Construction.k] AV

The avStarActionQEquivHom construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.avStarActionQEquivHom = Connes.Construction.PaperKernel.avStarActionHom.comp Connes.PaperNonisomorphism.qToH

noncomputable def Connes.PaperModuleSemisimple.avStarRepresentation : Representation Construction.k (↥Q) AV

The tensor summand carries the actual quotient action. Paper: §6.

Equations

• Connes.PaperModuleSemisimple.avStarRepresentation = LinearEquiv.automorphismGroup.toLinearMapMonoidHom.comp Connes.PaperModuleSemisimple.avStarActionQEquivHom

noncomputable def Connes.PaperModuleSemisimple.directSumRepresentation : Representation Construction.k (↥Q) DS

The direct sum of copies of the finite dual representation is explicit. Paper: §6.

Equations

• Connes.PaperModuleSemisimple.directSumRepresentation = Representation.directSum fun (x : Connes.PaperModuleSemisimple.I) => Connes.PaperModuleSemisimple.qVStarRepresentation

noncomputable def Connes.PaperModuleSemisimple.directSumFinsuppEquiv : (I →₀ qVStarRepresentation.asModule) ≃ₗ[Construction.k] DS

The direct sum is identified with its finitely supported coordinate model. Paper: §6.

Equations

• Connes.PaperModuleSemisimple.directSumFinsuppEquiv = finsuppLequivDFinsupp Connes.Construction.k

noncomputable def Connes.PaperModuleSemisimple.tensorDirectSumEquiv : AV ≃ₗ[Construction.k] DS

The ordered tensor basis identifies AVStar with the direct sum coordinates. Paper: §6.

Equations

• Connes.PaperModuleSemisimple.tensorDirectSumEquiv = (TensorProduct.equivFinsuppOfBasisLeft Connes.Construction.PaperKernel.orderedBasis).trans (finsuppLequivDFinsupp Connes.Construction.k)

theorem Connes.PaperModuleSemisimple.tensorDirectSumEquiv_intertwines (q : ↥Q) (x : AV) : tensorDirectSumEquiv ((avStarRepresentation q) x) = (directSumRepresentation q) (tensorDirectSumEquiv x)

The tensor coordinate equivalence respects the quotient representations. Paper: §6.

noncomputable def Connes.PaperModuleSemisimple.tensorDirectSumEquivRep : avStarRepresentation.IntertwiningMap directSumRepresentation

The tensorDirectSumEquivRep construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperModuleSemisimple.directSumPointwiseEquiv : directSumRepresentation.asModule ≃ₗ[PaperNonisomorphism.Ring] I →₀ qVStarRepresentation.asModule

The direct sum action and its pointwise finitely supported action agree. Paper: §6.

Equations

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

theorem Connes.PaperModuleSemisimple.avStar_semisimple : IsSemisimpleModule PaperNonisomorphism.Ring avStarRepresentation.asModule

The tensor summand is semisimple over the finite group algebra. Paper: §6.

def Connes.PaperModuleSemisimple.scalarRepresentation : Representation Construction.k (↥Q) Construction.k

The scalarRepresentation construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.scalarRepresentation = Representation.trivial Connes.Construction.k (↥Connes.PaperModuleSemisimple.Q) Connes.Construction.k

theorem Connes.PaperModuleSemisimple.scalar_simple : IsSimpleModule PaperNonisomorphism.Ring scalarRepresentation.asModule

The trivial scalar module is simple over the group algebra. Paper: §6.

@[reducible, inline]

abbrev Connes.PaperModuleSemisimple.CI : Type

The CI construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.CI = Module.Free.ChooseBasisIndex Connes.Construction.k ↥Connes.Construction.PaperKernel.C

noncomputable def Connes.PaperModuleSemisimple.cBasis : Module.Basis CI Construction.k ↥Construction.PaperKernel.C

The cBasis construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.cBasis = Module.Free.chooseBasis Connes.Construction.k ↥Connes.Construction.PaperKernel.C

noncomputable def Connes.PaperModuleSemisimple.cRepresentation : Representation Construction.k ↥Q ↥Construction.PaperKernel.C

The quotient action on C is trivial in the first module. Paper: §6.

Equations

• Connes.PaperModuleSemisimple.cRepresentation = Representation.trivial Connes.Construction.k ↥Connes.PaperModuleSemisimple.Q ↥Connes.Construction.PaperKernel.C

noncomputable def Connes.PaperModuleSemisimple.cFinsuppRepresentation : Representation Construction.k (↥Q) (CI →₀ Construction.k)

The coordinate representation on the C basis is trivial. Paper: §6.

Equations

• Connes.PaperModuleSemisimple.cFinsuppRepresentation = Representation.trivial Connes.Construction.k (↥Connes.PaperModuleSemisimple.Q) (Connes.PaperModuleSemisimple.CI →₀ Connes.Construction.k)

theorem Connes.PaperModuleSemisimple.cFinsupp_pointwise_semisimple : IsSemisimpleModule PaperNonisomorphism.Ring (CI →₀ scalarRepresentation.asModule)

The coordinate copies form a semisimple module. Paper: §6.

def Connes.PaperModuleSemisimple.cPointwiseEquiv : cFinsuppRepresentation.asModule ≃ₗ[PaperNonisomorphism.Ring] CI →₀ scalarRepresentation.asModule

The cPointwiseEquiv construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperModuleSemisimple.cFinsupp_semisimple : IsSemisimpleModule PaperNonisomorphism.Ring cFinsuppRepresentation.asModule

The trivial coordinate representation is semisimple. Paper: §6.

noncomputable def Connes.PaperModuleSemisimple.cBasisIntertwining : cRepresentation.IntertwiningMap cFinsuppRepresentation

The cBasisIntertwining construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperModuleSemisimple.cRepresentation_semisimple : IsSemisimpleModule PaperNonisomorphism.Ring cRepresentation.asModule

The actual trivial C representation is semisimple. Paper: §6.

noncomputable def Connes.PaperModuleSemisimple.firstProductRepresentation : Representation Construction.k (↥Q) (AV × ↥Construction.PaperKernel.C)

The firstProductRepresentation construction used in the Connes rigidity formalization.

Equations

• Connes.PaperModuleSemisimple.firstProductRepresentation = Connes.PaperModuleSemisimple.avStarRepresentation.prod Connes.PaperModuleSemisimple.cRepresentation

noncomputable def Connes.PaperModuleSemisimple.firstProductInl : avStarRepresentation.asModule →ₗ[PaperNonisomorphism.Ring] firstProductRepresentation.asModule

The tensor summand embeds as a group-algebra submodule of the product. Paper: §6.

Equations

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

noncomputable def Connes.PaperModuleSemisimple.firstProductInr : cRepresentation.asModule →ₗ[PaperNonisomorphism.Ring] firstProductRepresentation.asModule

The C summand embeds as a group-algebra submodule of the product. Paper: §6.

Equations

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

@[simp]

theorem Connes.PaperModuleSemisimple.firstProductInl_apply (x : avStarRepresentation.asModule) : firstProductInl x = (x, 0)

@[simp]

theorem Connes.PaperModuleSemisimple.firstProductInr_apply (x : cRepresentation.asModule) : firstProductInr x = (0, x)

theorem Connes.PaperModuleSemisimple.firstProduct_semisimple : IsSemisimpleModule PaperNonisomorphism.Ring firstProductRepresentation.asModule