Documentation

LeanPool.ConnesRigidity.Paper.Section6.NonisomorphismEmbedding

The nonisomorphism embedding component of the Connes rigidity formalization.

source
noncomputable def Connes.PaperNonisomorphism.paperDTwoEmbeddingLinear :
PaperEll →ₗ[Construction.k] Construction.PaperKernel.D

The paperDTwoEmbeddingLinear construction used in the Connes rigidity formalization.

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

    The paperDTwoEmbeddingIntertwining 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.paperDTwoEmbedding_injective :
      Function.Injective ⇑paperDTwoEmbeddingLinear
      source
      noncomputable def Connes.PaperNonisomorphism.paperDTwoEmbedding :
      paperEllRepresentation.asModule →ₗ[Ring] qRepresentationTwo.asModule

      The paperDTwoEmbedding 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.paperDTwoEmbedding_module_injective :
        Function.Injective ⇑paperDTwoEmbedding
        source
        theorem Connes.PaperNonisomorphism.paper_moduleTwo_not_semisimple :
        ¬moduleTwoSemisimple
        source
        def Connes.PaperNonisomorphism.paperEllRepresentationAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
        Representation Construction.k (↥Construction.PaperKernel.Q) PaperEll

        The paperEllRepresentationAlong construction used in the Connes rigidity formalization.

        Equations
        Instances For
          source
          noncomputable def Connes.PaperNonisomorphism.paperDTwoEmbeddingIntertwiningAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
          (paperEllRepresentationAlong σ).IntertwiningMap (qRepresentationTwoAlong σ)

          The paperDTwoEmbeddingIntertwiningAlong construction used in the Connes rigidity formalization.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def Connes.PaperNonisomorphism.paperDTwoEmbeddingAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
            (paperEllRepresentationAlong σ).asModule →ₗ[Ring] (qRepresentationTwoAlong σ).asModule

            The paperDTwoEmbeddingAlong 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.paperDTwoEmbeddingAlong_injective (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
              Function.Injective ⇑(paperDTwoEmbeddingAlong σ)
              source
              def Connes.PaperNonisomorphism.paperEllVStarRepresentationAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
              Representation Construction.k (↥Construction.PaperKernel.Q) Construction.PaperKernel.VStar

              The paperEllVStarRepresentationAlong construction used in the Connes rigidity formalization.

              Equations
              Instances For
                source
                def Connes.PaperNonisomorphism.paperEllScalarRepresentationAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                Representation Construction.k (↥Construction.PaperKernel.Q) Construction.k

                The paperEllScalarRepresentationAlong construction used in the Connes rigidity formalization.

                Equations
                Instances For
                  source
                  def Connes.PaperNonisomorphism.paperEllInclusionIntertwiningAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                  (paperEllVStarRepresentationAlong σ).IntertwiningMap (paperEllRepresentationAlong σ)

                  The paperEllInclusionIntertwiningAlong 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.paperEllProjectionIntertwiningAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                    (paperEllRepresentationAlong σ).IntertwiningMap (paperEllScalarRepresentationAlong σ)

                    The paperEllProjectionIntertwiningAlong 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.paperEllInclusionAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                      (paperEllVStarRepresentationAlong σ).asModule →ₗ[Ring] (paperEllRepresentationAlong σ).asModule

                      The paperEllInclusionAlong 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.paperEllProjectionAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                        (paperEllRepresentationAlong σ).asModule →ₗ[Ring] (paperEllScalarRepresentationAlong σ).asModule

                        The paperEllProjectionAlong 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.paperEllProjectionAlong_surjective (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                          Function.Surjective ⇑(paperEllProjectionAlong σ)
                          source
                          theorem Connes.PaperNonisomorphism.paperEllExactAlong (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                          Function.Exact ⇑(paperEllInclusionAlong σ) ⇑(paperEllProjectionAlong σ)
                          source
                          theorem Connes.PaperNonisomorphism.paperEllExtensionAlong_not_splits (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                          ¬∃ (section_ : (paperEllScalarRepresentationAlong σ).asModule →ₗ[Ring] (paperEllRepresentationAlong σ).asModule), paperEllProjectionAlong σ ∘ₗ section_ = LinearMap.id
                          source
                          theorem Connes.PaperNonisomorphism.paperEllAlong_not_semisimple (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                          ¬IsSemisimpleModule Ring (paperEllRepresentationAlong σ).asModule
                          source
                          theorem Connes.PaperNonisomorphism.paper_moduleTwoAlong_not_semisimple (σ : ↥Construction.PaperKernel.Q ≃* ↥Construction.PaperKernel.Q) :
                          ¬moduleTwoSemisimpleAlong σ