SupportFromTrace.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Balanced support data from trace-zero actions

For the Cartan model, the diagonal entries of the action in a homogeneous word basis are sums of the letter weights. Unimodularity makes the trace zero, yielding the balanced multiplicities of the support datum.

theorem OAI.PolycyclicRecognition.balanced_letter_counts line 25

Source documentation

The total letter count in a word basis turns the diagonal trace identity into the positive relation among the generator weights.

theorem balanced_letter_counts
    (α : I → Module.Dual ℝ W) (count : B → J → I → ℕ)
    (action : B → W → Matrix J J ℝ)
    (diagonal : ∀ b w j, action b w j j = ∑ i, (count b j i : ℝ) * α i w)
    (trace_zero : ∀ b w, Matrix.trace (action b w) = 0) (b : B) (w : W) :
    ∑ i, ((∑ j, count b j i : ℕ) : ℝ) * α i w = 0 := by
…

def OAI.PolycyclicRecognition.supportDatumOfTrace line 38

Source documentation

Build the segment-support norm data from homogeneous word counts and the trace-zero matrix identity for the action on the nilpotent ideal.

def supportDatumOfTrace
    (α : I → Module.Dual ℝ W) (count : B → J → I → ℕ)
    (action : B → W → Matrix J J ℝ)
    (mandatory : ∀ b i, 0 < ∑ j, count b j i)
    (diagonal : ∀ b w j, action b w j j = ∑ i, (count b j i : ℝ) * α i w)
    (trace_zero : ∀ b w, Matrix.trace (action b w) = 0)
    (separates : ∀ w, (∀ i, α i w = 0) → w = 0) : SupportDatum W I B where
…

Mentions: OAI.PolycyclicRecognition.SupportDatum

theorem OAI.PolycyclicRecognition.trace_zero_matrix_of_trace_zero line 52

Source documentation

For a linear action, its trace-zero property can be checked in any basis.

theorem trace_zero_matrix_of_trace_zero
    {N : Type*} [AddCommGroup N] [Module ℝ N] [DecidableEq J]
    (basis : Basis J ℝ N) (A : W →ₗ[ℝ] Module.End ℝ N)
    (h : ∀ w, LinearMap.trace ℝ N (A w) = 0) (w : W) :
    Matrix.trace (LinearMap.toMatrix basis basis (A w)) = 0 := by
…