The special-linear carrier in Zhou's construction

@[reducible, inline]

abbrev Connes.SpecialLinear.F : Type

Characteristic-two scalar field. Paper: §§2, 4.

Equations

• Connes.SpecialLinear.F = ZMod 2

@[reducible, inline]

abbrev Connes.SpecialLinear.R : Type

Polynomial coefficient ring. Paper: §2.

Equations

• Connes.SpecialLinear.R = Polynomial Connes.SpecialLinear.F

@[reducible, inline]

abbrev Connes.SpecialLinear.SL3 : Type

Special-linear group carrier. Paper: §§2, 4.

Equations

• Connes.SpecialLinear.SL3 = Matrix.SpecialLinearGroup (Fin 3) Connes.SpecialLinear.R

instance Connes.SpecialLinear.instCountableR : Countable R

Countability of the polynomial ring. Paper: §4.

instance Connes.SpecialLinear.instCountableMatrixFinOfNatNatR : Countable (Matrix (Fin 3) (Fin 3) R)

Countability of the matrix carrier. Paper: §4.

instance Connes.SpecialLinear.instCountableSL3 : Countable SL3

Countability of the special-linear carrier. Paper: §4.

noncomputable def Connes.SpecialLinear.sl3Group : CountableDiscreteGroup

Countable discrete acting-group carrier. Paper: §§4, 5.

Equations

• Connes.SpecialLinear.sl3Group = { Carrier := Connes.SpecialLinear.SL3, group := inferInstance, countable := Connes.SpecialLinear.sl3Group._proof_1 }