RootCentralizer.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The root-pair centralizer

The common centralizer of opposite elementary root groups has a scalar block on their two coordinates. This gives the concrete matrix form needed to apply the integral scalar-block obstruction to orbit returns.

def OAI.DukePrimeDegree.rootPairCentralizer line 22
lemma OAI.DukePrimeDegree.rootPairCentralizer_isClosed line 26
lemma OAI.DukePrimeDegree.mem_rootPairCentralizer line 30
lemma OAI.DukePrimeDegree.rootPairCentralizer_entries line 50

theorem OAI.DukePrimeDegree.rootPairCentralizer_block line 63

Source documentation

Reindexing the common centralizer of opposite roots separates its scalar two-dimensional block from the complementary matrix.

theorem rootPairCentralizer_block {n m : ℕ}
    (e : Fin n ≃ Fin 2 ⊕ Fin m)
    (hij : e.symm (Sum.inl 0) ≠ e.symm (Sum.inl 1))
    (g : G n) (hg : g ∈ rootPairCentralizer hij) :
    ∃ c : ℝ, ∃ B : Matrix (Fin m) (Fin m) ℝ,
      Matrix.reindex e e g.val =
        Matrix.fromBlocks (Matrix.diagonal (fun _ : Fin 2 => c)) 0 0 B := by
…

Mentions: OAI.DukePrimeDegree.rootPairCentralizer

theorem OAI.DukePrimeDegree.reindexed_integral_scalar_block line 96

Source documentation

The scalar-block obstruction after the coordinate reindexing used for an arbitrary opposite-root pair in the arithmetic quotient.

theorem reindexed_integral_scalar_block {n m : ℕ}
    (e : Fin n ≃ Fin 2 ⊕ Fin m)
    (q : G n) (γ : Matrix.SpecialLinearGroup (Fin n) ℤ)
    (c : ℝ) (B : Matrix (Fin m) (Fin m) ℝ) (hsep : B.charpoly.Separable)
    (hblock : Matrix.reindex e e
      (q⁻¹ * Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) γ * q).val =
        Matrix.fromBlocks (Matrix.diagonal (fun _ : Fin 2 => c)) 0 0 B) :
    c = 1 ∨ c = -1 := by
…