The factor closure component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperFactorClosure.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorClosure.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperFactorClosure.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorClosure.H = Connes.Construction.H

theorem Connes.PaperFactorClosure.paperHaarProbability (X : CrossedProduct.HaarProbabilityAction H PaperFactorIsomorphism.DualCoordinates) : MeasureTheory.IsProbabilityMeasure X.measure

def Connes.PaperFactorClosure.reducedCrossedGeneratorSetOne : Set (↥PaperGroupFactor.CrossedOne →L[ℂ] ↥PaperGroupFactor.CrossedOne)

The reducedCrossedGeneratorSetOne construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

def Connes.PaperFactorClosure.reducedCrossedGeneratorSetTwo : Set (↥PaperGroupFactor.CrossedTwo →L[ℂ] ↥PaperGroupFactor.CrossedTwo)

The reducedCrossedGeneratorSetTwo construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem Connes.PaperFactorClosure.paperGroupFactorUnitaryOne_generatorSet_image : ⇑PaperGroupFactor.paperGroupFactorUnitaryOne.conjStarAlgEquiv '' SemidirectGeneratorTransport.generatorSet Construction.PaperKernel.paperThetaOneHom = reducedCrossedGeneratorSetOne

theorem Connes.PaperFactorClosure.paperGroupFactorUnitaryTwo_generatorSet_image : ⇑PaperGroupFactor.paperGroupFactorUnitaryTwo.conjStarAlgEquiv '' SemidirectGeneratorTransport.generatorSet Construction.PaperKernel.paperThetaTwoHom = reducedCrossedGeneratorSetTwo

theorem Connes.PaperFactorClosure.paperGroupFactorUnitaryOne_mem_reducedClosure_iff (T : ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom)) →L[ℂ] ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom))) : T ∈ vonNeumannClosure (Set.range fun (x : Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom) => ↑((leftRegularRepresentation (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom)) x)) ↔ PaperGroupFactor.paperGroupFactorUnitaryOne.conjStarAlgEquiv T ∈ vonNeumannClosure reducedCrossedGeneratorSetOne

theorem Connes.PaperFactorClosure.paperGroupFactorUnitaryTwo_mem_reducedClosure_iff (T : ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom)) →L[ℂ] ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom))) : T ∈ vonNeumannClosure (Set.range fun (x : Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom) => ↑((leftRegularRepresentation (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom)) x)) ↔ PaperGroupFactor.paperGroupFactorUnitaryTwo.conjStarAlgEquiv T ∈ vonNeumannClosure reducedCrossedGeneratorSetTwo

theorem Connes.PaperFactorClosure.coordinateComplexCharacter_star (d : D) : star (PaperCrossedKernel.coordinateComplexCharacter d) = PaperCrossedKernel.coordinateComplexCharacter (-d)

noncomputable def Connes.PaperFactorClosure.coordinateCharacterSubalgebra : StarSubalgebra ℂ C(PaperFactorIsomorphism.DualCoordinates, ℂ)

The coordinateCharacterSubalgebra construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem Connes.PaperFactorClosure.coordinateCharacterSubalgebra_toSubmodule : Subalgebra.toSubmodule coordinateCharacterSubalgebra.toSubalgebra = Submodule.span ℂ (Set.range PaperCrossedKernel.coordinateComplexCharacter)

theorem Connes.PaperFactorClosure.coordinateComplexCharacter_span_closure_eq_top : (Submodule.span ℂ (Set.range PaperCrossedKernel.coordinateComplexCharacter)).topologicalClosure = ⊤

theorem Connes.PaperFactorClosure.continuousCrossedMultiplier_coordinate_one (d : D) : (CrossedProduct.continuousCrossedMultiplier PaperCrossedHaar.paperHaarActionOne) (PaperCrossedKernel.coordinateComplexCharacter d) = PaperCrossedKernel.crossedKernelMultiplier d

theorem Connes.PaperFactorClosure.continuousCrossedMultiplier_coordinate_two (d : D) : (CrossedProduct.continuousCrossedMultiplier PaperCrossedHaar.paperHaarActionTwo) (PaperCrossedKernel.coordinateComplexCharacter d) = CrossedProduct.crossedMultiplier PaperCrossedHaar.paperHaarActionTwo (PaperCrossedKernel.coordinateCharacterCoefficient d)

def Connes.PaperFactorClosure.continuousCrossedGeneratorSetOne : Set (↥PaperGroupFactor.CrossedOne →L[ℂ] ↥PaperGroupFactor.CrossedOne)

The continuousCrossedGeneratorSetOne construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorClosure.continuousCrossedGeneratorSetOne = Connes.CrossedProduct.continuousCrossedGeneratorSet Connes.PaperCrossedHaar.paperHaarActionOne

def Connes.PaperFactorClosure.continuousCrossedGeneratorSetTwo : Set (↥PaperGroupFactor.CrossedTwo →L[ℂ] ↥PaperGroupFactor.CrossedTwo)

The continuousCrossedGeneratorSetTwo construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorClosure.continuousCrossedGeneratorSetTwo = Connes.CrossedProduct.continuousCrossedGeneratorSet Connes.PaperCrossedHaar.paperHaarActionTwo

theorem Connes.PaperFactorClosure.reducedCrossedGeneratorSetOne_eq_continuousCoefficients : reducedCrossedGeneratorSetOne = CrossedProduct.crossedGeneratorSetOfContinuousCoefficients PaperCrossedHaar.paperHaarActionOne PaperCrossedKernel.coordinateComplexCharacter

theorem Connes.PaperFactorClosure.reducedCrossedGeneratorSetTwo_eq_continuousCoefficients : reducedCrossedGeneratorSetTwo = CrossedProduct.crossedGeneratorSetOfContinuousCoefficients PaperCrossedHaar.paperHaarActionTwo PaperCrossedKernel.coordinateComplexCharacter

theorem Connes.PaperFactorClosure.reducedClosureOne_eq_continuousClosure : vonNeumannClosure reducedCrossedGeneratorSetOne = vonNeumannClosure continuousCrossedGeneratorSetOne

theorem Connes.PaperFactorClosure.reducedClosureTwo_eq_continuousClosure : vonNeumannClosure reducedCrossedGeneratorSetTwo = vonNeumannClosure continuousCrossedGeneratorSetTwo

theorem Connes.PaperFactorClosure.paperHaarEquiv_mem_continuousClosure_iff (T : ↥PaperGroupFactor.CrossedOne →L[ℂ] ↥PaperGroupFactor.CrossedOne) : T ∈ vonNeumannClosure continuousCrossedGeneratorSetOne ↔ (CrossedProduct.crossedHaarHilbertEquiv PaperCrossedHaar.paperHaarEquiv).conjStarAlgEquiv T ∈ vonNeumannClosure continuousCrossedGeneratorSetTwo

noncomputable def Connes.PaperFactorClosure.paperSpatialUnitary : ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom)) ≃ₗᵢ[ℂ] ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom))

The paperSpatialUnitary construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem Connes.PaperFactorClosure.paperSpatialUnitary_maps_group_factor (T : ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom)) →L[ℂ] ↥(GroupL2 (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom))) : T ∈ vonNeumannClosure (Set.range fun (x : Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom) => ↑((leftRegularRepresentation (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaOneHom)) x)) ↔ paperSpatialUnitary.conjStarAlgEquiv T ∈ vonNeumannClosure (Set.range fun (x : Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom) => ↑((leftRegularRepresentation (Construction.PaperKernel.paperGammaCarrier Construction.PaperKernel.paperThetaTwoHom)) x))

The spatial equivalence carries the first regular group factor onto the second. Paper: §3.

theorem Connes.PaperFactorClosure.paperSpatialUnitary_maps_vacuum : paperSpatialUnitary PaperGroupVacuum.paperIdentityOne = PaperGroupVacuum.paperIdentityTwo

noncomputable def Connes.PaperFactorClosure.paperSpatialWitness : FactorWitness.SpatialWitness Construction.PaperKernel.paperGammaOne Construction.PaperKernel.paperGammaTwo

The paperSpatialWitness construction used in the Connes rigidity formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem Connes.PaperFactorClosure.paperGroupFactors_isomorphic : TracialGroupFactorsIsomorphic Construction.PaperKernel.paperGammaOne Construction.PaperKernel.paperGammaTwo