Nonisomorphism foundations for Zhou §6. The quotient representations and semisimplicity predicates are the concrete k[Sp₄(F₂)] modules attached to the two actions from §2.

@[reducible, inline]

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

The Q construction used in the Connes rigidity formalization.

Equations

• Connes.PaperNonisomorphism.Q = Connes.Construction.PaperKernel.Q

@[reducible, inline]

abbrev Connes.PaperNonisomorphism.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperNonisomorphism.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperNonisomorphism.Ring : Type

The Ring construction used in the Connes rigidity formalization.

Equations

• Connes.PaperNonisomorphism.Ring = MonoidAlgebra Connes.Construction.k ↥Connes.PaperNonisomorphism.Q

noncomputable def Connes.PaperNonisomorphism.qToH : ↥Q →* Construction.H

The quotient action map Sp₄(F₂) → SL₃(R) × Sp₄(F₂). Paper: §§2, 6.

Equations

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

noncomputable def Connes.PaperNonisomorphism.qLinearActionOne : ↥Q →* D ≃ₗ[Construction.k] D

The first quotient action on the actual additive kernel. Paper: §6.

Equations

• Connes.PaperNonisomorphism.qLinearActionOne = Connes.Construction.PaperKernel.paperThetaOneLinearHom.comp Connes.PaperNonisomorphism.qToH

noncomputable def Connes.PaperNonisomorphism.qLinearActionTwo : ↥Q →* D ≃ₗ[Construction.k] D

The second quotient action on the actual additive kernel. Paper: §6.

Equations

• Connes.PaperNonisomorphism.qLinearActionTwo = Connes.Construction.PaperKernel.paperThetaTwoLinearHom.comp Connes.PaperNonisomorphism.qToH

noncomputable def Connes.PaperNonisomorphism.qRepresentationOne : Representation Construction.k (↥Q) D

Linear representation attached to the first actual quotient action.

Equations

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

noncomputable def Connes.PaperNonisomorphism.qRepresentationTwo : Representation Construction.k (↥Q) D

Linear representation attached to the second actual quotient action.

Equations

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

noncomputable def Connes.PaperNonisomorphism.qRepresentationTwoAlong (σ : ↥Q ≃* ↥Q) : Representation Construction.k (↥Q) D

Pull back the second quotient action along the quotient automorphism induced by a hypothetical group isomorphism. Paper: §6.

Equations

• Connes.PaperNonisomorphism.qRepresentationTwoAlong σ = { toFun := fun (q : ↥Connes.PaperNonisomorphism.Q) => Connes.PaperNonisomorphism.qRepresentationTwo (σ q), map_one' := ⋯, map_mul' := ⋯ }

@[instance_reducible]

noncomputable instance Connes.PaperNonisomorphism.representationAsModuleAddCommGroup (ρ : Representation Construction.k (↥Q) D) : AddCommGroup ρ.asModule

Equations

• Connes.PaperNonisomorphism.representationAsModuleAddCommGroup ρ = { toAddGroup := ρ.instAddCommGroupAsModule.toAddGroup, add_comm := ⋯ }

@[reducible, inline]

abbrev Connes.PaperNonisomorphism.moduleOneSemisimple : Prop

The actual first quotient module is semisimple over the group algebra.

Equations

• Connes.PaperNonisomorphism.moduleOneSemisimple = IsSemisimpleModule Connes.PaperNonisomorphism.Ring Connes.PaperNonisomorphism.qRepresentationOne.asModule

@[reducible, inline]

abbrev Connes.PaperNonisomorphism.moduleTwoSemisimple : Prop

The actual second quotient module is semisimple over the group algebra.

Equations

• Connes.PaperNonisomorphism.moduleTwoSemisimple = IsSemisimpleModule Connes.PaperNonisomorphism.Ring Connes.PaperNonisomorphism.qRepresentationTwo.asModule

@[reducible, inline]

abbrev Connes.PaperNonisomorphism.moduleTwoSemisimpleAlong (σ : ↥Q ≃* ↥Q) : Prop

Semisimplicity predicate after the quotient automorphism from §6.

Equations

• Connes.PaperNonisomorphism.moduleTwoSemisimpleAlong σ = IsSemisimpleModule Connes.PaperNonisomorphism.Ring (Connes.PaperNonisomorphism.qRepresentationTwoAlong σ).asModule

@[reducible, inline]

abbrev Connes.PaperNonisomorphism.FiniteCocycle.W : Type

The W construction used in the Connes rigidity formalization.

Equations

• Connes.PaperNonisomorphism.FiniteCocycle.W = Connes.OpenAIPort.ModTwoSpace

def Connes.PaperNonisomorphism.FiniteCocycle.cocycle (q : ↥Q) (v : W) : Construction.k

The finite quadratic correction appearing in the second action. Paper: §2, §6.

Equations

• Connes.PaperNonisomorphism.FiniteCocycle.cocycle q v = Connes.OpenAIPort.standardQuadraticForm (q⁻¹ • v) + Connes.OpenAIPort.standardQuadraticForm v

@[reducible, inline]

abbrev Connes.PaperNonisomorphism.FiniteCocycle.IsLinearCoboundary : Prop

Linear coboundary predicate for the finite quotient correction. Paper: §6.

Equations

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

def Connes.PaperNonisomorphism.FiniteCocycle.coordinateFunctional (c v : W) : Construction.k

A coordinate functional on the four-dimensional quotient module. Paper: §6.

Equations

• Connes.PaperNonisomorphism.FiniteCocycle.coordinateFunctional c v = ∑ i : Connes.OpenAIPort.SymplecticIndex, c i * v i

theorem Connes.PaperNonisomorphism.FiniteCocycle.not_linearCoboundary : ¬IsLinearCoboundary

The finite correction is not a linear coboundary. This is the proved four-dimensional obstruction used by the §6 module argument. Paper: §6.

@[simp]

theorem Connes.PaperNonisomorphism.finiteCocycle_eq (q : ↥Q) (v : FiniteCocycle.W) : FiniteCocycle.cocycle q v = OpenAIPort.standardQuadraticForm (q⁻¹ • v) + OpenAIPort.standardQuadraticForm v

theorem Connes.PaperNonisomorphism.finiteCocycle_not_linearCoboundary : ¬FiniteCocycle.IsLinearCoboundary

The finite correction is not a linear coboundary. Paper: §6.

theorem Connes.PaperNonisomorphism.thetaTwo_q_correction (q : ↥Q) (c : ↥Construction.PaperKernel.C) : ((Construction.PaperKernel.thetaTwoLinearMap (1, q)) (0, c)).1 = Construction.PaperKernel.delta c ⊗ₜ[Construction.k] OpenAIPort.quadraticDefectLinear q

The actual second action contains the finite quadratic correction on the quotient fiber. Paper: §2, §6.