Documentation

LeanPool.ConnesRigidity.Paper.Section3.GroupQuotient

The group quotient component of the Connes rigidity formalization.

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

The D construction used in the Connes rigidity formalization.

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

    The H construction used in the Connes rigidity formalization.

    Equations
    Instances For
      source
      theorem Connes.PaperGroupQuotient.paperGroupFactorUnitaryOne_conj_inr (h : H) :
      PaperGroupFactor.paperGroupFactorUnitaryOne.conjStarAlgEquiv ↑(leftRegularUnitary (SemidirectProduct.inr h)) = ↑↑(CrossedProduct.crossedGroupUnitary PaperCrossedHaar.paperHaarActionOne h)
      source
      theorem Connes.PaperGroupQuotient.paperGroupFactorUnitaryTwo_conj_inr (h : H) :
      PaperGroupFactor.paperGroupFactorUnitaryTwo.conjStarAlgEquiv ↑(leftRegularUnitary (SemidirectProduct.inr h)) = ↑↑(CrossedProduct.crossedGroupUnitary PaperCrossedHaar.paperHaarActionTwo h)