OAI/Topology/ArtinGroups/ParabolicIntersections/MeshQuiverAlgebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite positive Cartan quivers satisfy the explicit mesh ideal bound.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.meshArrowValues_relation line 16
  2. theorem OAI.HarmonicArtin.ParabolicIntersections.quiver_mesh_words_vanish line 50
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.meshNilpotent_of_positive_cartan line 71

    Source documentation

    The exact free-algebra ideal statement used in the conditional main theorems, now proved for every finite simple positive Cartan quiver.

    theorem meshNilpotent_of_positive_cartan
    (hcartan : ((2 : ℝ) • (1 : Matrix U U ℝ)-(meshQuiverGraph Q U hloop).adjMatrix ℝ).PosDef) :
    MeshNilpotent Q U := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshQuiverGraph, OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent