The dual action conjugacy algebra component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyAlgebra.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyAlgebra.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyAlgebra.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyAlgebra.H = Connes.Construction.H

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyAlgebra.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyAlgebra.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyAlgebra.PaperV : Type

The PaperV construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyAlgebra.PaperV = Connes.Construction.PaperKernel.PaperV

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyAlgebra.VStar : Type

The VStar construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyAlgebra.VStar = Connes.Construction.PaperKernel.VStar

theorem Connes.PaperDualActionConjugacyAlgebra.avDualEquiv_symm_eval (z : A →ₗ[k] PaperV) (a : A) (φ : VStar) : (PaperDualCoordinates.avDualEquiv.symm z) (a ⊗ₜ[k] φ) = φ (z a)

theorem Connes.PaperDualActionConjugacyAlgebra.avDualEquiv_eval (F : Module.Dual k Construction.PaperKernel.AVStar) (a : A) (φ : VStar) : φ ((PaperDualCoordinates.avDualEquiv F) a) = F (a ⊗ₜ[k] φ)

noncomputable def Connes.PaperDualActionConjugacyAlgebra.qTensor (z : A →ₗ[k] PaperV) : Construction.PaperKernel.TensorAA →ₗ[k] k

The qTensor construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperDualActionConjugacyAlgebra.zAction (h : H) (z : A →ₗ[k] PaperV) : A →ₗ[k] PaperV

The transformed first dual coordinate. Paper: §3.

Equations

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

noncomputable def Connes.PaperDualActionConjugacyAlgebra.thetaTwoTermTensor (h : H) : Construction.PaperKernel.TensorAA →ₗ[k] Construction.PaperKernel.AVStar

The tensor form of the second-action correction. Paper: §3.

Equations

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

theorem Connes.PaperDualActionConjugacyAlgebra.zAction_apply (h : H) (z : A →ₗ[k] PaperV) (a : A) : (zAction h z) a = (Construction.PaperKernel.qVAction h.2) (z ((Construction.PaperKernel.sl3AAction h⁻¹.1) a))

theorem Connes.PaperDualActionConjugacyAlgebra.paperThetaOne_symm_inl (h : H) (u : Construction.PaperKernel.AVStar) : (Construction.PaperKernel.paperThetaOneLinear h).symm (u, 0) = ((Construction.PaperKernel.avStarAction h⁻¹.1 h⁻¹.2) u, 0)

theorem Connes.PaperDualActionConjugacyAlgebra.standardQuadraticForm_qVAction (q : ↥Construction.PaperKernel.Q) (v : PaperV) : OpenAIPort.standardQuadraticForm ((Construction.PaperKernel.qVAction q) v) = (OpenAIPort.quadraticDefectLinear q⁻¹) v + OpenAIPort.standardQuadraticForm v

theorem Connes.PaperDualActionConjugacyAlgebra.paperThetaOne_symm_inr (h : H) (c : ↥Construction.PaperKernel.C) : (Construction.PaperKernel.paperThetaOneLinearHom h).symm (0, c) = (0, (Construction.PaperKernel.sl3CAction h⁻¹.1) c)

theorem Connes.PaperDualActionConjugacyAlgebra.paperThetaTwo_symm_inr (h : H) (c : ↥Construction.PaperKernel.C) : (Construction.PaperKernel.paperThetaTwoLinearHom h).symm (0, c) = ((Construction.PaperKernel.thetaTwoTermMap h⁻¹) c, (Construction.PaperKernel.sl3CAction h⁻¹.1) c)

theorem Connes.PaperDualActionConjugacyAlgebra.paperThetaOneHom_symm_eq (h : H) : (Construction.PaperKernel.paperThetaOneLinearHom h).symm = (Construction.PaperKernel.paperThetaOneLinear h).symm