OAI/NumberTheory/DukePrimeDegree/Geometry/NeutralDiagonal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The neutral diagonal group

The kernel of one root character, inside trace-zero real weights, is the group used for the ergodic decomposition in EKL's low-entropy argument. Its diagonal representation takes values in the opposite-root centralizer.

  1. def OAI.DukePrimeDegree.neutralWeightSubgroup line 21
  2. lemma OAI.DukePrimeDegree.diagonalOneParameter_add_weights line 35
  3. def OAI.DukePrimeDegree.neutralDiagonalHom line 48
  4. lemma OAI.DukePrimeDegree.continuous_neutralDiagonalHom line 60
  5. def OAI.DukePrimeDegree.neutralDiagonalOppositeHom line 80

    Source documentation

    The opposite representation matches the right action on lattices.

    def neutralDiagonalOppositeHom {n : ℕ} {i j : Fin n} (hij : i ≠ j) :
    Multiplicative (neutralWeightSubgroup i j) →* MulOpposite (rootPairCentralizer hij) where
…

    Mentions: OAI.DukePrimeDegree.neutralWeightSubgroup, OAI.DukePrimeDegree.rootPairCentralizer

  6. lemma OAI.DukePrimeDegree.continuous_neutralDiagonalOppositeHom line 89