The dual topology component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperDualTopology.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualTopology.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperDualTopology.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualTopology.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperDualTopology.TensorAA : Type

The TensorAA construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualTopology.TensorAA = Connes.Construction.PaperKernel.TensorAA

@[reducible, inline]

abbrev Connes.PaperDualTopology.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualTopology.CharacterSpace = Connes.PaperDualHaar.PaperCharacterSpace

@[reducible, inline]

abbrev Connes.PaperDualTopology.Coordinates : Type

The Coordinates construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualTopology.Coordinates = Connes.PaperFactorIsomorphism.DualCoordinates

theorem Connes.PaperDualTopology.avDualEquiv_apply_proj (F : Module.Dual k Construction.PaperKernel.AVStar) (a : Construction.A) (v : OpenAIPort.SymplecticIndex) : (PaperDualCoordinates.avDualEquiv F) a v = F (a ⊗ₜ[k] LinearMap.proj v)

theorem Connes.PaperDualTopology.continuous_characterLinear_eval (d : D) : Continuous fun (χ : CharacterSpace) => (BinaryPontryaginDual.characterLinear (Additive.toMul χ)) d

theorem Connes.PaperDualTopology.character_coordinate_eval (χ : CharacterSpace) (a : Construction.A) (v : OpenAIPort.SymplecticIndex) : (PaperDualHaar.characterCoordinatesEquiv χ).1 a v = (BinaryPontryaginDual.characterLinear (Additive.toMul χ)) (a ⊗ₜ[k] LinearMap.proj v, 0)

theorem Connes.PaperDualTopology.character_second_eval (χ : CharacterSpace) (c : ↥Construction.PaperKernel.C) : (PaperDualHaar.characterCoordinatesEquiv χ).2 c = (BinaryPontryaginDual.characterLinear (Additive.toMul χ)) (0, c)

theorem Connes.PaperDualTopology.continuous_character_quadratic_eval (c : ↥Construction.PaperKernel.C) : Continuous fun (χ : CharacterSpace) => (PaperFactorIsomorphism.quadraticMap (PaperDualHaar.characterCoordinatesEquiv χ).1) c

noncomputable def Connes.PaperDualTopology.shearedLinear (χ : CharacterSpace) : Module.Dual k D

The shearedLinear construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperDualTopology.shearedLinear_eval (χ : CharacterSpace) (d : D) : (shearedLinear χ) d = (BinaryPontryaginDual.characterLinear (Additive.toMul χ)) d + (PaperFactorIsomorphism.quadraticMap (PaperDualHaar.characterCoordinatesEquiv χ).1) d.2

theorem Connes.PaperDualTopology.continuous_shearedLinear_eval (d : D) : Continuous fun (χ : CharacterSpace) => (shearedLinear χ) d

Every fixed kernel element has a continuous value after the fiber shear. Paper: §3.

noncomputable def Connes.PaperDualTopology.characterFiberShearMul (χ : CharacterSpace) : PontryaginDual (Multiplicative D)

The characterFiberShearMul construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualTopology.characterFiberShearMul χ = Connes.PaperDualHaar.linearCharacter (Connes.PaperDualTopology.shearedLinear χ)

theorem Connes.PaperDualTopology.continuous_characterFiberShearMul : Continuous characterFiberShearMul

The character-valued shear is continuous in the compact-open topology. Paper: §3.

noncomputable def Connes.PaperDualTopology.characterFiberShear (χ : CharacterSpace) : CharacterSpace

The characterFiberShear construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualTopology.characterFiberShear χ = Additive.ofMul (Connes.PaperDualTopology.characterFiberShearMul χ)

theorem Connes.PaperDualTopology.characterFiberShear_eq_transport (χ : CharacterSpace) : characterFiberShear χ = PaperDualHaar.characterCoordinatesEquiv.symm (PaperFactorIsomorphism.fiberShear (PaperDualHaar.characterCoordinatesEquiv χ))

theorem Connes.PaperDualTopology.continuous_characterFiberShear : Continuous characterFiberShear

@[instance_reducible]

noncomputable instance Connes.PaperDualTopology.paperCoordinatesTopology : TopologicalSpace Coordinates

Equations

• Connes.PaperDualTopology.paperCoordinatesTopology = TopologicalSpace.induced (⇑Connes.PaperDualHaar.characterCoordinatesEquiv.symm) inferInstance

noncomputable def Connes.PaperDualTopology.characterCoordinatesHomeomorph : CharacterSpace ≃ₜ Coordinates

The character/coordinate equivalence is a homeomorphism for the transported topology. Paper: §3.

Equations

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

instance Connes.PaperDualTopology.coordinatesCompactSpace : CompactSpace Coordinates

instance Connes.PaperDualTopology.coordinatesIsTopologicalAddGroup : IsTopologicalAddGroup Coordinates

@[instance_reducible]

noncomputable instance Connes.PaperDualTopology.coordinatesMeasurableSpace : MeasurableSpace Coordinates

Equations

• Connes.PaperDualTopology.coordinatesMeasurableSpace = borel Connes.PaperDualTopology.Coordinates

instance Connes.PaperDualTopology.coordinatesBorelSpace : BorelSpace Coordinates

theorem Connes.PaperDualTopology.continuous_fiberShear : Continuous PaperFactorIsomorphism.fiberShear

theorem Connes.PaperDualTopology.measurable_fiberShear : Measurable PaperFactorIsomorphism.fiberShear

noncomputable def Connes.PaperDualTopology.coordinatesHaar : MeasureTheory.Measure Coordinates

The normalized Haar probability in raw Zhou coordinates. Paper: §3.

Equations

• Connes.PaperDualTopology.coordinatesHaar = Connes.NormalizedHaar.normalizedAddHaar Connes.PaperDualTopology.Coordinates

instance Connes.PaperDualTopology.coordinatesHaar_isProbability : MeasureTheory.IsProbabilityMeasure coordinatesHaar

instance Connes.PaperDualTopology.coordinatesHaar_isAddHaar : coordinatesHaar.IsAddLeftInvariant