Algebraic part of Zhou §3 for the concrete tensor kernel, including the quadratic fiber shear and its characteristic-two involutivity.

@[reducible, inline]

abbrev Connes.PaperFactorIsomorphism.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorIsomorphism.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperFactorIsomorphism.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorIsomorphism.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperFactorIsomorphism.PaperV : Type

The PaperV construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorIsomorphism.PaperV = Connes.Construction.PaperKernel.PaperV

@[reducible, inline]

abbrev Connes.PaperFactorIsomorphism.SymplecticIndex : Type

The SymplecticIndex construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorIsomorphism.SymplecticIndex = Connes.OpenAIPort.SymplecticIndex

@[reducible, inline]

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

The C construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorIsomorphism.C = Connes.Construction.PaperKernel.C

@[reducible, inline]

abbrev Connes.PaperFactorIsomorphism.TensorAA : Type

The TensorAA construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorIsomorphism.TensorAA = Connes.Construction.PaperKernel.TensorAA

@[reducible, inline]

abbrev Connes.PaperFactorIsomorphism.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperFactorIsomorphism.H = Connes.Construction.H

@[reducible, inline]

abbrev Connes.PaperFactorIsomorphism.DualCoordinates : Type

The algebraic dual coordinates used by Zhou's fiber model. Paper: §3.

Equations

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

noncomputable def Connes.PaperFactorIsomorphism.coordinate (z : A →ₗ[k] PaperV) (i : SymplecticIndex) : A →ₗ[k] k

One finite coordinate of a map A → V. Paper: §3.

Equations

• Connes.PaperFactorIsomorphism.coordinate z i = { toFun := fun (a : Connes.PaperFactorIsomorphism.A) => z a i, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def Connes.PaperFactorIsomorphism.tensorFunctional (f g : A →ₗ[k] k) : TensorAA →ₗ[k] k

Bilinear evaluation on a pure tensor. Paper: §3.

Equations

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

noncomputable def Connes.PaperFactorIsomorphism.tensorFunctionalOnC (f g : A →ₗ[k] k) : ↥C →ₗ[k] k

Restriction of tensor evaluation to the flip-fixed carrier. Paper: §3.

Equations

• Connes.PaperFactorIsomorphism.tensorFunctionalOnC f g = (Connes.PaperFactorIsomorphism.tensorFunctional f g).domRestrict Connes.PaperFactorIsomorphism.C

@[simp]

theorem Connes.PaperFactorIsomorphism.tensorFunctionalOnC_diagonal (f g : A →ₗ[k] k) (a : A) : (tensorFunctionalOnC f g) (Construction.PaperKernel.diagonal a) = f a * g a

noncomputable def Connes.PaperFactorIsomorphism.quadraticMap (z : A →ₗ[k] PaperV) : ↥C →ₗ[k] k

Zhou's quadratic functional on the symmetric tensor dual. Paper: §3.

Equations

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

@[simp]

theorem Connes.PaperFactorIsomorphism.quadraticMap_diagonal (z : A →ₗ[k] PaperV) (a : A) : (quadraticMap z) (Construction.PaperKernel.diagonal a) = OpenAIPort.standardQuadraticForm (z a)

noncomputable def Connes.PaperFactorIsomorphism.fiberShear : DualCoordinates → DualCoordinates

The nontrivial fiber shear from Zhou Proposition 3.2. Paper: §3.

Equations

• Connes.PaperFactorIsomorphism.fiberShear p = (p.1, p.2 + Connes.PaperFactorIsomorphism.quadraticMap p.1)

theorem Connes.PaperFactorIsomorphism.fiberShear_involutive (p : DualCoordinates) : fiberShear (fiberShear p) = p

The characteristic-two cancellation behind the fiber shear. Paper: §3.