CongruenceQuotients.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The actual congruence quotients and diagonal holonomies

The congruence quotient is SL₃(ℤ/2^kℤ), including the singleton quotient for k = 0. Its diagonal matrices have entries t,t⁻¹,1, and the finite-level matrices are obtained by the genuine 2-adic reduction maps.

theorem OAI.CoarseAssembly.Congruence.diagonal_one line 21
theorem OAI.CoarseAssembly.Congruence.diagonal_mul line 27
def OAI.CoarseAssembly.Congruence.diagonalHom line 38
Source documentation
The diagonal assignment respects the unit-group multiplication.
```
def diagonalHom {R : Type*} [CommRing R] : Rˣ →* Matrix.SpecialLinearGroup (Fin 3) R where
…
```

theorem OAI.CoarseAssembly.Congruence.trace_diagonal_pow line 44

Source documentation

Powers of the diagonal holonomy have the expected Laurent trace.

theorem trace_diagonal_pow {R : Type*} [CommRing R] (t : Rˣ) (m : ℕ) :
    Matrix.trace ((diagonal t ^ m : Matrix.SpecialLinearGroup (Fin 3) R) : Matrix (Fin 3) (Fin 3) R) =
      (t ^ m : Rˣ) + ((t ^ m)⁻¹ : Rˣ) + 1 := by
…

Mentions: OAI.CoarseAssembly.Congruence.diagonal

theorem OAI.CoarseAssembly.Congruence.trace_diagonal_zpow line 52

theorem OAI.CoarseAssembly.Congruence.trace_diagonal_neg line 62

Source documentation

Reversing the signed charge leaves the diagonal trace unchanged.

theorem trace_diagonal_neg {R : Type*} [CommRing R] (t : Rˣ) (m : ℤ) :
    Matrix.trace ((diagonal t ^ (-m) : Matrix.SpecialLinearGroup (Fin 3) R) :
      Matrix (Fin 3) (Fin 3) R) =
    Matrix.trace ((diagonal t ^ m : Matrix.SpecialLinearGroup (Fin 3) R) :
      Matrix (Fin 3) (Fin 3) R) := by
…

Mentions: OAI.CoarseAssembly.Congruence.diagonal

theorem OAI.CoarseAssembly.Congruence.trace_conjugate line 71
theorem OAI.CoarseAssembly.Congruence.trace_reduce line 80
Source documentation
Integral word traces reduce to their ordinary residue classes.
```
theorem trace_reduce (k : ℕ) (w : ArithmeticGroup) :
    Matrix.trace (reduce k w : Matrix (Fin 3) (Fin 3) (ZMod (2 ^ k))) =
      ((Matrix.trace (w : Matrix (Fin 3) (Fin 3) ℤ) : ℤ) : ZMod (2 ^ k)) := by
…
```
Mentions: OAI.CoarseAssembly.Congruence.ArithmeticGroup, OAI.CoarseAssembly.Congruence.reduce