Documentation

LeanPool.ConnesRigidity.Paper.Section3.CrossedAction

The crossed action component of the Connes rigidity formalization.

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

The k construction used in the Connes rigidity formalization.

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

    The D construction used in the Connes rigidity formalization.

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

      The H construction used in the Connes rigidity formalization.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Connes.PaperCrossedAction.Coordinates :
        Type

        The Coordinates construction used in the Connes rigidity formalization.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev Connes.PaperCrossedAction.CharacterSpace :
          Type

          The CharacterSpace construction used in the Connes rigidity formalization.

          Equations
          Instances For
            source
            noncomputable def Connes.PaperCrossedAction.characterActionOfLinear (e : D ≃ₗ[k] D) :
            CharacterSpace ≃+ CharacterSpace

            The characterActionOfLinear 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.PaperCrossedAction.characterLinearEquiv_characterActionOfLinear (e : D ≃ₗ[k] D) (χ : CharacterSpace) :
              PaperDualHaar.characterLinearEquiv ((characterActionOfLinear e) χ) = (PaperDualActions.dualPrecomp e) (PaperDualHaar.characterLinearEquiv χ)
              source
              theorem Connes.PaperCrossedAction.continuous_characterActionOfLinear (e : D ≃ₗ[k] D) :
              Continuous ⇑(characterActionOfLinear e)
              source
              theorem Connes.PaperCrossedAction.coordinateAction_eq_characterTransport (theta : H →* D ≃ₗ[k] D) (h : H) (p : Coordinates) :
              (PaperDualActions.coordinateAction (PaperDualActions.dualPrecompHom theta) h) p = PaperDualHaar.characterCoordinatesEquiv ((characterActionOfLinear (theta h)) (PaperDualHaar.characterCoordinatesEquiv.symm p))
              source
              theorem Connes.PaperCrossedAction.continuous_paperCoordinateActionOne (h : H) :
              Continuous ⇑(PaperDualActions.paperCoordinateActionOne h)
              source
              theorem Connes.PaperCrossedAction.continuous_paperCoordinateActionTwo (h : H) :
              Continuous ⇑(PaperDualActions.paperCoordinateActionTwo h)