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

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyFirst.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyFirst.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyFirst.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyFirst.H = Connes.Construction.H

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyFirst.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyFirst.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperDualActionConjugacyFirst.PaperV : Type

The PaperV construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActionConjugacyFirst.PaperV = Connes.Construction.PaperKernel.PaperV

theorem Connes.PaperDualActionConjugacyFirst.first_coordinate_eq_zAction (h : H) (z : A →ₗ[k] PaperV) (lam : ↥Construction.PaperKernel.C →ₗ[k] k) : PaperDualCoordinates.avDualEquiv (LinearMap.coprod (PaperDualCoordinates.avDualEquiv.symm z) lam ∘ₗ ↑(Construction.PaperKernel.paperThetaOneLinear h).symm ∘ₗ LinearMap.inl k Construction.PaperKernel.AVStar ↥Construction.PaperKernel.C) = PaperDualActionConjugacyAlgebra.zAction h z