The chart orbits component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperChartOrbits.F : Type

The F construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.F = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperChartOrbits.R : Type

The R construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.R = Connes.Construction.R

@[reducible, inline]

abbrev Connes.PaperChartOrbits.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.A = Connes.Construction.A

theorem Connes.PaperChartOrbits.h10 : 1 ≠ 0

theorem Connes.PaperChartOrbits.h01 : 0 ≠ 1

theorem Connes.PaperChartOrbits.h20 : 2 ≠ 0

theorem Connes.PaperChartOrbits.h02 : 0 ≠ 2

noncomputable def Connes.PaperChartOrbits.t10 : SpecialLinear.SL3

The t10 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.t10 = Matrix.SpecialLinearGroup.transvection Connes.PaperChartOrbits.h10 1

noncomputable def Connes.PaperChartOrbits.t01 : SpecialLinear.SL3

The t01 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.t01 = Matrix.SpecialLinearGroup.transvection Connes.PaperChartOrbits.h01 1

noncomputable def Connes.PaperChartOrbits.t20 : SpecialLinear.SL3

The t20 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.t20 = Matrix.SpecialLinearGroup.transvection Connes.PaperChartOrbits.h20 1

noncomputable def Connes.PaperChartOrbits.t02 : SpecialLinear.SL3

The t02 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.t02 = Matrix.SpecialLinearGroup.transvection Connes.PaperChartOrbits.h02 1

noncomputable def Connes.PaperChartOrbits.moveOne : SpecialLinear.SL3

The moveOne construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.moveOne = Connes.PaperChartOrbits.t10 * (Connes.PaperChartOrbits.t01 * Connes.PaperChartOrbits.t10)

noncomputable def Connes.PaperChartOrbits.moveTwo : SpecialLinear.SL3

The moveTwo construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.moveTwo = Connes.PaperChartOrbits.t20 * (Connes.PaperChartOrbits.t02 * Connes.PaperChartOrbits.t20)

noncomputable def Connes.PaperChartOrbits.basisMove (s : Fin 3) : SpecialLinear.SL3

The basisMove construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.basisMove s = if s = 0 then 1 else if s = 1 then Connes.PaperChartOrbits.moveOne else Connes.PaperChartOrbits.moveTwo

theorem Connes.PaperChartOrbits.transvection_action_vector {i j : Fin 3} (hij : i ≠ j) (a : R) (x : A) : (Construction.PaperKernel.sl3AAction (Matrix.SpecialLinearGroup.transvection hij a)) x = fun (r : Fin 3) => if r = i then x r + a * x j else x r

theorem Connes.PaperChartOrbits.moveOne_apply : (Construction.PaperKernel.sl3AAction moveOne) (PaperFiniteCharts.basisVector 0) = PaperFiniteCharts.basisVector 1

theorem Connes.PaperChartOrbits.moveTwo_apply : (Construction.PaperKernel.sl3AAction moveTwo) (PaperFiniteCharts.basisVector 0) = PaperFiniteCharts.basisVector 2

theorem Connes.PaperChartOrbits.basisMove_apply (s : Fin 3) : (Construction.PaperKernel.sl3AAction (basisMove s)) (PaperFiniteCharts.basisVector 0) = PaperFiniteCharts.basisVector s

noncomputable def Connes.PaperChartOrbits.chartOrbitWitness (s : Fin 3) (f h : R) : SpecialLinear.SL3

The chartOrbitWitness construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartOrbits.chartOrbitWitness s f h = Matrix.SpecialLinearGroup.transvection ⋯ h * (Matrix.SpecialLinearGroup.transvection ⋯ f * Connes.PaperChartOrbits.basisMove s)

theorem Connes.PaperChartOrbits.chartOrbitWitness_apply (s : Fin 3) (f h : R) : (Construction.PaperKernel.sl3AAction (chartOrbitWitness s f h)) (PaperFiniteCharts.basisVector 0) = PaperFiniteCharts.chartVector s f h

theorem Connes.PaperChartOrbits.chartPoint_in_orbit (N : ℕ) (s : Fin 3) (f h : Fin N → F) : ∃ (g : SpecialLinear.SL3), (Construction.PaperKernel.sl3AAction g) (PaperFiniteCharts.basisVector 0) = PaperFiniteCharts.chartPoint N (s, f, h)

theorem Connes.PaperChartOrbits.chartSquare_in_orbit (N : ℕ) (s : Fin 3) (f h : Fin N → F) : ∃ (g : SpecialLinear.SL3), (Construction.PaperKernel.sl3CAction g) (Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0)) = PaperFiniteCharts.chartSquare N (s, f, h)