Documentation

LeanPool.ConnesRigidity.Paper.Section6.ModuleSemisimpleTransport

Transport the concrete first-module semisimplicity proof into the paper-facing predicate and expose the resulting Section 6 nonisomorphism theorem.

source
@[reducible, inline]
abbrev Connes.PaperModuleSemisimpleTransport.Q :
Submonoid (Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) (ZMod 2))

The Q construction used in the Connes rigidity formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Connes.PaperModuleSemisimpleTransport.D :
    Type

    The D construction used in the Connes rigidity formalization.

    Equations
    Instances For
      source
      noncomputable def Connes.PaperModuleSemisimpleTransport.paperFirstProductRepresentation :
      Representation Construction.k (↥Q) D

      The paperFirstProductRepresentation construction used in the Connes rigidity formalization.

      Equations
      Instances For
        source
        theorem Connes.PaperModuleSemisimpleTransport.paper_qRepresentationOne_eq_firstProduct :
        PaperNonisomorphism.qRepresentationOne = paperFirstProductRepresentation
        source
        theorem Connes.PaperModuleSemisimpleTransport.paper_moduleOne_semisimple :
        PaperNonisomorphism.moduleOneSemisimple
        source
        theorem Connes.PaperModuleSemisimpleTransport.paperGroups_not_isomorphic :
        ¬Nonempty (Construction.PaperKernel.paperGammaOne.Carrier ≃* Construction.PaperKernel.paperGammaTwo.Carrier)

        The two concrete paper groups are nonisomorphic. This is the public §6 endpoint.