Special-linear conjugacy and ICC for Zhou §5

theorem Connes.SpecialLinear.conjugates_eq_iff_quotient_commutes {G : Type u_1} [Group G] (u v g : G) : u * g * u⁻¹ = v * g * v⁻¹ ↔ Commute (v⁻¹ * u) g

Conjugacy equality is equivalent to commuting with a quotient conjugator. Paper: §5.

theorem Connes.SpecialLinear.transvection_conjugates_eq_iff_commutes {ι : Type u_1} {A : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing A] {i j : ι} (hij : i ≠ j) (a b : A) (g : Matrix.SpecialLinearGroup ι A) : Matrix.SpecialLinearGroup.transvection hij a * g * (Matrix.SpecialLinearGroup.transvection hij a)⁻¹ = Matrix.SpecialLinearGroup.transvection hij b * g * (Matrix.SpecialLinearGroup.transvection hij b)⁻¹ ↔ Commute (Matrix.SpecialLinearGroup.transvection hij (a - b)) g

Transvection conjugacy equality is equivalent to a commuting relation. Paper: §5.

theorem Connes.SpecialLinear.commute_matrixUnit_of_commute_nonzero_transvection {ι : Type u_1} {A : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing A] [IsDomain A] {i j : ι} (hij : i ≠ j) (a : A) (ha : a ≠ 0) (g : Matrix.SpecialLinearGroup ι A) (h : Commute (Matrix.SpecialLinearGroup.transvection hij a) g) : Commute (Matrix.single i j 1) ↑g

A nonzero commuting transvection forces its matrix unit to commute. Paper: §5.

theorem Connes.SpecialLinear.transvection_conjugates_injective_of_not_commute_matrixUnit {ι : Type u_1} {A : Type u_2} [Fintype ι] [DecidableEq ι] [CommRing A] [IsDomain A] {i j : ι} (hij : i ≠ j) (g : Matrix.SpecialLinearGroup ι A) (hnot : ¬Commute (Matrix.single i j 1) ↑g) : Function.Injective fun (a : A) => Matrix.SpecialLinearGroup.transvection hij a * g * (Matrix.SpecialLinearGroup.transvection hij a)⁻¹

Noncommuting matrix units make transvection conjugation injective. Paper: §5.

theorem Connes.SpecialLinear.sl3_isICC : IsICC sl3Group

ICC boundary for the special-linear group. Paper: §5.