The characteristic component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperCharacteristic.R : Type

The R construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristic.R = Connes.SpecialLinear.R

@[reducible, inline]

abbrev Connes.PaperCharacteristic.I : Type

The I construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristic.I = Fin 3

@[reducible, inline]

abbrev Connes.PaperCharacteristic.M : Type

The M construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristic.M = Matrix Connes.PaperCharacteristic.I Connes.PaperCharacteristic.I Connes.PaperCharacteristic.R

@[reducible, inline]

abbrev Connes.PaperCharacteristic.G : Type

The G construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristic.G = Connes.SpecialLinear.SL3

noncomputable def Connes.PaperCharacteristic.paperTransvection (i j : I) (hij : i ≠ j) (f : R) : G

The paperTransvection construction used in the Connes rigidity formalization.

Equations

• Connes.PaperCharacteristic.paperTransvection i j hij f = Matrix.SpecialLinearGroup.transvection hij f

theorem Connes.PaperCharacteristic.paperTransvection_square (i j : I) (hij : i ≠ j) (f : R) : paperTransvection i j hij f * paperTransvection i j hij f = 1

theorem Connes.PaperCharacteristic.paperDiagonalEntryEquation (i j : I) (hij : i ≠ j) (b : G) (f : R) (hcomm : Commute b (paperTransvection i j hij f * b * (paperTransvection i j hij f)⁻¹)) : f * (↑b * ↑b) j i + f ^ 2 * (↑b j i * ↑b j i) = 0

theorem Connes.PaperCharacteristic.paperOffDiagonalZeroOfMemNormalCommuting (B : Subgroup G) (hBnormal : B.Normal) (hcommute : ∀ (x y : ↥B), x * y = y * x) (b : G) (hb : b ∈ B) {i j : I} (hij : i ≠ j) : ↑b j i = 0

theorem Connes.PaperCharacteristic.paperSL3NoNontrivialAbelianNormalSubgroup (B : Subgroup G) (hBnormal : B.Normal) (hcommute : ∀ (x y : ↥B), x * y = y * x) : B = ⊥