Documentation

LeanPool.ConnesRigidity.Paper.Section3.DualActionConjugacyQuadratic

The dual action conjugacy quadratic component of the Connes rigidity formalization.

source
@[reducible, inline]
abbrev Connes.PaperDualActionConjugacyQuadratic.k :
Type

The k construction used in the Connes rigidity formalization.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Connes.PaperDualActionConjugacyQuadratic.H :
    Type

    The H construction used in the Connes rigidity formalization.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Connes.PaperDualActionConjugacyQuadratic.A :
      Type

      The A construction used in the Connes rigidity formalization.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Connes.PaperDualActionConjugacyQuadratic.PaperV :
        Type

        The PaperV construction used in the Connes rigidity formalization.

        Equations
        Instances For
          source
          theorem Connes.PaperDualActionConjugacyQuadratic.qTensor_covariance_on_diagonal (h : H) (z : A →ₗ[k] PaperV) (a : A) :
          (PaperDualActionConjugacyAlgebra.qTensor (PaperDualActionConjugacyAlgebra.zAction h z)) ↑(Construction.PaperKernel.diagonal a) = (PaperDualCoordinates.avDualEquiv.symm z) ((PaperDualActionConjugacyAlgebra.thetaTwoTermTensor h) ↑(Construction.PaperKernel.diagonal a)) + (PaperDualActionConjugacyAlgebra.qTensor z) ((Construction.PaperKernel.sl3TensorAction h⁻¹.1) ↑(Construction.PaperKernel.diagonal a))
          source
          theorem Connes.PaperDualActionConjugacyQuadratic.qTensor_covariance (h : H) (z : A →ₗ[k] PaperV) (c : ↥Construction.PaperKernel.C) :
          (PaperDualActionConjugacyAlgebra.qTensor (PaperDualActionConjugacyAlgebra.zAction h z)) ↑c = (PaperDualCoordinates.avDualEquiv.symm z) ((PaperDualActionConjugacyAlgebra.thetaTwoTermTensor h) ↑c) + (PaperDualActionConjugacyAlgebra.qTensor z) ((Construction.PaperKernel.sl3TensorAction h⁻¹.1) ↑c)
          source
          theorem Connes.PaperDualActionConjugacyQuadratic.quadratic_covariance (h : H) (z : A →ₗ[k] PaperV) (c : ↥Construction.PaperKernel.C) :
          (PaperFactorIsomorphism.quadraticMap (PaperDualActionConjugacyAlgebra.zAction h z)) c = (PaperDualCoordinates.avDualEquiv.symm z) ((Construction.PaperKernel.thetaTwoTermMap h⁻¹) c) + (PaperFactorIsomorphism.quadraticMap z) ((Construction.PaperKernel.sl3CAction h⁻¹.1) c)