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

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyCoordinates.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyCoordinates.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyCoordinates.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyCoordinates.H = Connes.Construction.H

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyCoordinates.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyCoordinates.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyCoordinates.PaperV : Type

The PaperV construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyCoordinates.PaperV = Connes.Construction.PaperKernel.PaperV

theorem Connes.PaperDualActionConjugacyCoordinates.coordinateAction_snd_eval (dualAction : H →* Module.Dual k Construction.PaperKernel.D ≃ₗ[k] Module.Dual k Construction.PaperKernel.D) (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) (c : ↥Construction.PaperKernel.C) : ((PaperDualActions.coordinateAction dualAction h) (z, lam)).2 c = ((dualAction h) (PaperDualCoordinates.dualEquiv.symm (z, lam))) (0, c)

theorem Connes.PaperDualActionConjugacyCoordinates.dualEquiv_symm_pairing (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) (u : Construction.PaperKernel.AVStar) (c : ↥Construction.PaperKernel.C) : (PaperDualCoordinates.dualEquiv.symm (z, lam)) (u, c) = (PaperDualCoordinates.avDualEquiv.symm z) u + lam c

theorem Connes.PaperDualActionConjugacyCoordinates.paperCoordinateActionOne_fst (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) : ((PaperDualActions.paperCoordinateActionOne h) (z, lam)).1 = PaperDualCoordinates.avDualEquiv (LinearMap.coprod (PaperDualCoordinates.avDualEquiv.symm z) lam ∘ₗ ↑(Construction.PaperKernel.paperThetaOneLinearHom h).symm ∘ₗ LinearMap.inl k Construction.PaperKernel.AVStar ↥Construction.PaperKernel.C)

theorem Connes.PaperDualActionConjugacyCoordinates.paperCoordinateActionTwo_fst (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) : ((PaperDualActions.paperCoordinateActionTwo h) (z, lam)).1 = PaperDualCoordinates.avDualEquiv (LinearMap.coprod (PaperDualCoordinates.avDualEquiv.symm z) lam ∘ₗ ↑(Construction.PaperKernel.paperThetaTwoLinearHom h).symm ∘ₗ LinearMap.inl k Construction.PaperKernel.AVStar ↥Construction.PaperKernel.C)

theorem Connes.PaperDualActionConjugacyCoordinates.paperCoordinateActionOne_snd_eval (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) (c : ↥Construction.PaperKernel.C) : ((PaperDualActions.paperCoordinateActionOne h) (z, lam)).2 c = (PaperDualCoordinates.dualEquiv.symm (z, lam)) ((Construction.PaperKernel.paperThetaOneLinearHom h).symm (0, c))

theorem Connes.PaperDualActionConjugacyCoordinates.paperCoordinateActionTwo_snd_eval (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) (c : ↥Construction.PaperKernel.C) : ((PaperDualActions.paperCoordinateActionTwo h) (z, lam)).2 c = (PaperDualCoordinates.dualEquiv.symm (z, lam)) ((Construction.PaperKernel.paperThetaTwoLinearHom h).symm (0, c))