Documentation

LeanPool.ConnesRigidity.Paper.Section3.GroupFactor

The group factor component of the Connes rigidity formalization.

source
@[reducible, inline]
abbrev Connes.PaperGroupFactor.D :
Type

The D construction used in the Connes rigidity formalization.

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

    The H construction used in the Connes rigidity formalization.

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev Connes.PaperGroupFactor.CrossedOne :
      AddSubgroup (PreLp fun (x : PaperCrossedHaar.H) => ↥(CrossedProduct.crossedBaseHilbert PaperCrossedHaar.paperHaarActionOne))

      The CrossedOne construction used in the Connes rigidity formalization.

      Equations
      Instances For
        source
        @[reducible, inline]
        noncomputable abbrev Connes.PaperGroupFactor.CrossedTwo :
        AddSubgroup (PreLp fun (x : PaperCrossedHaar.H) => ↥(CrossedProduct.crossedBaseHilbert PaperCrossedHaar.paperHaarActionTwo))

        The CrossedTwo construction used in the Connes rigidity formalization.

        Equations
        Instances For
          source
          noncomputable def Connes.PaperGroupFactor.paperGroupFactorUnitaryOne :
          ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom)) ≃ₗᵢ[ℂ] ↥CrossedOne

          The paperGroupFactorUnitaryOne 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.PaperGroupFactor.paperGroupFactorUnitaryTwo :
            ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom)) ≃ₗᵢ[ℂ] ↥CrossedTwo

            The second concrete Zhou group-factor unitary. Paper: §3.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem Connes.PaperGroupFactor.paperGroupFactorUnitaryOne_apply (ξ : ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom))) (h : H) :
              ↑(paperGroupFactorUnitaryOne ξ) h = PaperFourierCoordinates.paperFourierCoordinateUnitary (↑((SemidirectFubini.semidirectFubini Construction.PaperKernel.paperThetaOneHom) ξ) h)
              source
              @[simp]
              theorem Connes.PaperGroupFactor.paperGroupFactorUnitaryTwo_apply (ξ : ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom))) (h : H) :
              ↑(paperGroupFactorUnitaryTwo ξ) h = PaperFourierCoordinates.paperFourierCoordinateUnitary (↑((SemidirectFubini.semidirectFubini Construction.PaperKernel.paperThetaTwoHom) ξ) h)
              source
              theorem Connes.PaperGroupFactor.paperGroupFactorUnitaryOne_conj_inl (d : D) :
              paperGroupFactorUnitaryOne.conjStarAlgEquiv ↑(leftRegularUnitary (SemidirectProduct.inl (Multiplicative.ofAdd d))) = PaperCrossedKernel.crossedKernelMultiplier d
              source
              theorem Connes.PaperGroupFactor.paperGroupFactorUnitaryTwo_conj_inl (d : D) :
              paperGroupFactorUnitaryTwo.conjStarAlgEquiv ↑(leftRegularUnitary (SemidirectProduct.inl (Multiplicative.ofAdd d))) = CrossedProduct.crossedMultiplier PaperCrossedHaar.paperHaarActionTwo (PaperCrossedKernel.coordinateCharacterCoefficient d)