The dual actions component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperDualActions.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActions.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperDualActions.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActions.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperDualActions.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActions.H = Connes.Construction.H

@[reducible, inline]

abbrev Connes.PaperDualActions.Dual : Type

The Dual construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActions.Dual = Module.Dual Connes.PaperDualActions.k Connes.PaperDualActions.D

@[reducible, inline]

abbrev Connes.PaperDualActions.Coordinates : Type

The Coordinates construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualActions.Coordinates = Connes.PaperFactorIsomorphism.DualCoordinates

noncomputable def Connes.PaperDualActions.dualPrecomp (e : D ≃ₗ[k] D) : Dual ≃ₗ[k] Dual

Precomposition by the inverse is the contragredient of a kernel automorphism. Paper: §3.

Equations

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

@[simp]

theorem Connes.PaperDualActions.dualPrecomp_apply (e : D ≃ₗ[k] D) (ℓ : Dual) (d : D) : ((dualPrecomp e) ℓ) d = ℓ (e⁻¹ d)

noncomputable def Connes.PaperDualActions.dualPrecompHom (theta : H →* D ≃ₗ[k] D) : H →* Dual ≃ₗ[k] Dual

Contragredient action associated to a homomorphism of kernel actions. Paper: §§3--4.

Equations

• Connes.PaperDualActions.dualPrecompHom theta = { toFun := fun (h : Connes.PaperDualActions.H) => Connes.PaperDualActions.dualPrecomp (theta h), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Connes.PaperDualActions.dualPrecompHom_apply (theta : H →* D ≃ₗ[k] D) (h : H) (ℓ : Dual) (d : D) : (((dualPrecompHom theta) h) ℓ) d = ℓ ((theta h)⁻¹ d)

noncomputable def Connes.PaperDualActions.paperDualActionOne : H →* Dual ≃ₗ[k] Dual

The first actual Zhou contragredient action on the full dual. Paper: §3.

Equations

• Connes.PaperDualActions.paperDualActionOne = Connes.PaperDualActions.dualPrecompHom Connes.Construction.PaperKernel.paperThetaOneLinearHom

noncomputable def Connes.PaperDualActions.paperDualActionTwo : H →* Dual ≃ₗ[k] Dual

The second actual Zhou contragredient action on the full dual. Paper: §3.

Equations

• Connes.PaperDualActions.paperDualActionTwo = Connes.PaperDualActions.dualPrecompHom Connes.Construction.PaperKernel.paperThetaTwoLinearHom

noncomputable def Connes.PaperDualActions.coordinateAction (dualAction : H →* Dual ≃ₗ[k] Dual) (h : H) : Coordinates ≃+ Coordinates

Transport a full-dual additive equivalence to Zhou's raw coordinates. Paper: §3.

Equations

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

theorem Connes.PaperDualActions.coordinateAction_one (dualAction : H →* Dual ≃ₗ[k] Dual) : coordinateAction dualAction 1 = AddEquiv.refl Coordinates

theorem Connes.PaperDualActions.coordinateAction_mul (dualAction : H →* Dual ≃ₗ[k] Dual) (h h' : H) : coordinateAction dualAction (h * h') = (coordinateAction dualAction h').trans (coordinateAction dualAction h)

noncomputable def Connes.PaperDualActions.paperCoordinateActionOne (h : H) : Coordinates ≃+ Coordinates

The first actual Zhou action on the raw dual coordinates. Paper: §3.

Equations

• Connes.PaperDualActions.paperCoordinateActionOne h = Connes.PaperDualActions.coordinateAction Connes.PaperDualActions.paperDualActionOne h

noncomputable def Connes.PaperDualActions.paperCoordinateActionTwo (h : H) : Coordinates ≃+ Coordinates

The second actual Zhou action on the raw dual coordinates. Paper: §3.

Equations

• Connes.PaperDualActions.paperCoordinateActionTwo h = Connes.PaperDualActions.coordinateAction Connes.PaperDualActions.paperDualActionTwo h

@[simp]

theorem Connes.PaperDualActions.paperCoordinateActionOne_apply (h : H) (p : Coordinates) : (paperCoordinateActionOne h) p = PaperDualCoordinates.dualEquiv ((paperDualActionOne h) (PaperDualCoordinates.dualEquiv.symm p))

@[simp]

theorem Connes.PaperDualActions.paperCoordinateActionTwo_apply (h : H) (p : Coordinates) : (paperCoordinateActionTwo h) p = PaperDualCoordinates.dualEquiv ((paperDualActionTwo h) (PaperDualCoordinates.dualEquiv.symm p))

noncomputable def Connes.PaperDualActions.paperCoordinatePermAction (dualAction : H →* Dual ≃ₗ[k] Dual) : H →* Equiv.Perm Coordinates

Forget the additive structure when the factor witness needs permutation actions. Paper: §3.

Equations

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

noncomputable def Connes.PaperDualActions.paperCoordinatePermActionOne : H →* Equiv.Perm Coordinates

The first Zhou coordinate action as a permutation action. Paper: §3.

Equations

• Connes.PaperDualActions.paperCoordinatePermActionOne = Connes.PaperDualActions.paperCoordinatePermAction Connes.PaperDualActions.paperDualActionOne

noncomputable def Connes.PaperDualActions.paperCoordinatePermActionTwo : H →* Equiv.Perm Coordinates

The second Zhou coordinate action as a permutation action. Paper: §3.

Equations

• Connes.PaperDualActions.paperCoordinatePermActionTwo = Connes.PaperDualActions.paperCoordinatePermAction Connes.PaperDualActions.paperDualActionTwo