The dual action conjugacy component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacy.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacy.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacy.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacy.H = Connes.Construction.H

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacy.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacy.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacy.PaperV : Type

The PaperV construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacy.PaperV = Connes.Construction.PaperKernel.PaperV

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacy.Coordinates : Type

The Coordinates construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacy.Coordinates = Connes.PaperFactorIsomorphism.DualCoordinates

theorem Connes.PaperDualActionConjugacy.paperThetaOneTwo_symm_inl (h : H) (u : Construction.PaperKernel.AVStar) : (Construction.PaperKernel.paperThetaOneLinearHom h).symm (u, 0) = (Construction.PaperKernel.paperThetaTwoLinearHom h).symm (u, 0)

theorem Connes.PaperDualActionConjugacy.paperCoordinateActionOneTwo_fst_eq (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) : ((PaperDualActions.paperCoordinateActionOne h) (z, lam)).1 = ((PaperDualActions.paperCoordinateActionTwo h) (z, lam + PaperFactorIsomorphism.quadraticMap z)).1

theorem Connes.PaperDualActionConjugacy.paperCoordinateActionOne_fst_eq_zAction (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) : ((PaperDualActions.paperCoordinateActionOne h) (z, lam)).1 = PaperDualActionConjugacyAlgebra.zAction h z

theorem Connes.PaperDualActionConjugacy.paperCoordinateActionOne_snd_linear (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) (c : ↥Construction.PaperKernel.C) : ((PaperDualActions.paperCoordinateActionOne h) (z, lam)).2 c = lam ((Construction.PaperKernel.sl3CAction h⁻¹.1) c)

theorem Connes.PaperDualActionConjugacy.paperCoordinateActionTwo_snd_linear (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) (c : ↥Construction.PaperKernel.C) : ((PaperDualActions.paperCoordinateActionTwo h) (z, lam)).2 c = (PaperDualCoordinates.avDualEquiv.symm z) ((Construction.PaperKernel.thetaTwoTermMap h⁻¹) c) + lam ((Construction.PaperKernel.sl3CAction h⁻¹.1) c)

theorem Connes.PaperDualActionConjugacy.paperCoordinateActionOneTwo_snd_eq (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) : (PaperFactorIsomorphism.fiberShear ((PaperDualActions.paperCoordinateActionOne h) (z, lam))).2 = ((PaperDualActions.paperCoordinateActionTwo h) (PaperFactorIsomorphism.fiberShear (z, lam))).2

theorem Connes.PaperDualActionConjugacy.paperFiberShear_conjugates_paperActions (h : H) (p : Coordinates) : PaperFactorIsomorphism.fiberShear ((PaperDualActions.paperCoordinateActionOne h) p) = (PaperDualActions.paperCoordinateActionTwo h) (PaperFactorIsomorphism.fiberShear p)