Documentation

LeanPool.ConnesRigidity.Paper.Section6.NonisomorphismProofs

The nonisomorphism proofs component of the Connes rigidity formalization.

source
@[reducible, inline]
abbrev Connes.PaperNonisomorphism.PaperEll :
Type

The PaperEll construction used in the Connes rigidity formalization.

Equations
Instances For
    source
    def Connes.PaperNonisomorphism.paperEllMap (q : ↥Construction.PaperKernel.Q) :
    PaperEll →ₗ[Construction.k] PaperEll

    The paperEllMap construction used in the Connes rigidity formalization.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Connes.PaperNonisomorphism.paperEllRepresentation :
      Representation Construction.k (↥Construction.PaperKernel.Q) PaperEll

      The paperEllRepresentation construction used in the Connes rigidity formalization.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Connes.PaperNonisomorphism.paperEllVStarRepresentation :
        Representation Construction.k (↥Construction.PaperKernel.Q) Construction.PaperKernel.VStar

        The paperEllVStarRepresentation construction used in the Connes rigidity formalization.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Connes.PaperNonisomorphism.paperEllScalarRepresentation :
          Representation Construction.k (↥Construction.PaperKernel.Q) Construction.k

          The paperEllScalarRepresentation construction used in the Connes rigidity formalization.

          Equations
          Instances For
            source
            def Connes.PaperNonisomorphism.paperEllInclusionLinear :
            Construction.PaperKernel.VStar →ₗ[Construction.k] PaperEll

            The paperEllInclusionLinear construction used in the Connes rigidity formalization.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Connes.PaperNonisomorphism.paperEllInclusionIntertwining :
              paperEllVStarRepresentation.IntertwiningMap paperEllRepresentation

              The paperEllInclusionIntertwining construction used in the Connes rigidity formalization.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Connes.PaperNonisomorphism.paperEllProjectionLinear :
                PaperEll →ₗ[Construction.k] Construction.k

                The paperEllProjectionLinear construction used in the Connes rigidity formalization.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Connes.PaperNonisomorphism.paperEllProjectionIntertwining :
                  paperEllRepresentation.IntertwiningMap paperEllScalarRepresentation

                  The paperEllProjectionIntertwining construction used in the Connes rigidity formalization.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Connes.PaperNonisomorphism.paperEllInclusion :
                    paperEllVStarRepresentation.asModule →ₗ[Ring] paperEllRepresentation.asModule

                    The paperEllInclusion construction used in the Connes rigidity formalization.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Connes.PaperNonisomorphism.paperEllProjection :
                      paperEllRepresentation.asModule →ₗ[Ring] paperEllScalarRepresentation.asModule

                      The paperEllProjection construction used in the Connes rigidity formalization.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem Connes.PaperNonisomorphism.paperEll_projection_surjective :
                        Function.Surjective ⇑paperEllProjection
                        source
                        theorem Connes.PaperNonisomorphism.paperEll_exact :
                        Function.Exact ⇑paperEllInclusion ⇑paperEllProjection
                        source
                        theorem Connes.PaperNonisomorphism.paperEll_extension_not_splits :
                        ¬∃ (section_ : paperEllScalarRepresentation.asModule →ₗ[Ring] paperEllRepresentation.asModule), paperEllProjection ∘ₗ section_ = LinearMap.id
                        source
                        theorem Connes.PaperNonisomorphism.paperEll_not_semisimple :
                        ¬IsSemisimpleModule Ring paperEllRepresentation.asModule