The dual coordinates component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperDualCoordinates.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperDualCoordinates.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperDualCoordinates.V : Type

The V construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.V = Connes.Construction.PaperKernel.PaperV

@[reducible, inline]

abbrev Connes.PaperDualCoordinates.VStar : Type

The VStar construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.VStar = Connes.Construction.PaperKernel.VStar

@[reducible, inline]

abbrev Connes.PaperDualCoordinates.AVStar : Type

The AVStar construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.AVStar = Connes.Construction.PaperKernel.AVStar

@[reducible, inline]

abbrev Connes.PaperDualCoordinates.C : Submodule Construction.k Construction.PaperKernel.TensorAA

The C construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.C = Connes.Construction.PaperKernel.C

@[reducible, inline]

abbrev Connes.PaperDualCoordinates.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperDualCoordinates.DualCoordinates : Type

The DualCoordinates construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.DualCoordinates = Connes.PaperFactorIsomorphism.DualCoordinates

noncomputable def Connes.PaperDualCoordinates.vStarDualEquiv : Module.Dual k VStar ≃ₗ[k] V

The vStarDualEquiv construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.vStarDualEquiv = (Module.evalEquiv Connes.PaperDualCoordinates.k Connes.PaperDualCoordinates.V).symm

noncomputable def Connes.PaperDualCoordinates.transposeToDual : (A →ₗ[k] V) →ₗ[k] VStar →ₗ[k] Module.Dual k A

The transposeToDual construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperDualCoordinates.transposeFromDual : (VStar →ₗ[k] Module.Dual k A) →ₗ[k] A →ₗ[k] V

The transposeFromDual construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperDualCoordinates.transposeFromDual_left_inverse (f : A →ₗ[k] V) : transposeFromDual (transposeToDual f) = f

theorem Connes.PaperDualCoordinates.transposeFromDual_right_inverse (g : VStar →ₗ[k] Module.Dual k A) : transposeToDual (transposeFromDual g) = g

noncomputable def Connes.PaperDualCoordinates.transposeEquiv : (A →ₗ[k] V) ≃ₗ[k] VStar →ₗ[k] Module.Dual k A

The transposeEquiv construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperDualCoordinates.dualTensorToPartial : Module.Dual k AVStar →ₗ[k] VStar →ₗ[k] Module.Dual k A

The dualTensorToPartial construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperDualCoordinates.partialToDual : (VStar →ₗ[k] Module.Dual k A) →ₗ[k] Module.Dual k AVStar

The partialToDual construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperDualCoordinates.partialToDual_left_inverse (f : Module.Dual k AVStar) : partialToDual (dualTensorToPartial f) = f

theorem Connes.PaperDualCoordinates.partialToDual_right_inverse (g : VStar →ₗ[k] Module.Dual k A) : dualTensorToPartial (partialToDual g) = g

noncomputable def Connes.PaperDualCoordinates.dualTensorPartialEquiv : Module.Dual k AVStar ≃ₗ[k] VStar →ₗ[k] Module.Dual k A

The dualTensorPartialEquiv construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperDualCoordinates.avDualEquiv : Module.Dual k AVStar ≃ₗ[k] A →ₗ[k] V

The avDualEquiv construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualCoordinates.avDualEquiv = Connes.PaperDualCoordinates.dualTensorPartialEquiv.trans Connes.PaperDualCoordinates.transposeEquiv.symm

noncomputable def Connes.PaperDualCoordinates.dualEquiv : Module.Dual k D ≃ₗ[k] DualCoordinates

The dualEquiv construction used in the Connes rigidity formalization.

Equations

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