MeshNilpotence.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The published finite-Dynkin path input

MeshNilpotent is the positive-degree nilpotence assertion for the preprojective (mesh) algebra of an induced finite Dynkin graph. Its relations are displayed explicitly, rather than asserted for a complex. The standard finite-dimensionality input is Amiot, On the structure of triangulated categories with finitely many indecomposables, Bull. Soc. Math. France 135 (2007), Proposition 9.1; the essential-path formulation is Coquereaux (2002), §§3.1–3.2, and Cooper (2007), Theorem 5.4.3 and Proposition 5.6.10. On a bipartite Dynkin graph the usual signed mesh relations have the same zero sets as the displayed all-plus relations.

This module proves evaluation of the abstract relations. It does not assume their vanishing for coefficient maps of the target paper's complexes, nor assume any stabilizer or bounded-height conclusion.

def OAI.HarmonicArtin.ParabolicIntersections.meshRelation line 29
def OAI.HarmonicArtin.ParabolicIntersections.meshRelations line 32
def OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent line 39
Source documentation
Exact abstract algebra input: sufficiently long positive words lie in the two-sided ideal generated by the mesh relations.
```
def MeshNilpotent (U : Set V) : Prop :=
…
```

theorem OAI.HarmonicArtin.ParabolicIntersections.mesh_word_evaluate line 44

Source documentation

Evaluation of one abstract path identity into an arbitrary complex algebra.

theorem mesh_word_evaluate {U : Set V}
    {R : Type*} [Ring R] [Algebra ℂ R] (B : A → R)
    (houtside : ∀ a, Q.source a ∉ U ∨ Q.target a ∉ U → B a = 0)
    (hpath : ∀ a b, Q.target a ≠ Q.source b → B a * B b = 0)
    (hmesh : ∀ v ∈ U, (∑ a, if Q.source a = v then B a * B (Q.reverse a) else 0) = 0)
    (w : List A) (hw : (w.map (FreeAlgebra.ι ℂ)).prod ∈
      TwoSidedIdeal.span (meshRelations Q U)) : (w.map B).prod = 0 := by
…

Mentions: OAI.HarmonicArtin.ParabolicIntersections.meshRelations

theorem OAI.HarmonicArtin.ParabolicIntersections.meshNilpotent_evaluate line 73

Source documentation

The nilpotence exponent depends only on the graph, not on the algebra in which the paths are evaluated.

theorem meshNilpotent_evaluate {U : Set V} (h : MeshNilpotent Q U)
    {R : Type*} [Ring R] [Algebra ℂ R] (B : A → R)
    (houtside : ∀ a, Q.source a ∉ U ∨ Q.target a ∉ U → B a = 0)
    (hpath : ∀ a b, Q.target a ≠ Q.source b → B a * B b = 0)
    (hmesh : ∀ v ∈ U, (∑ a, if Q.source a = v then B a * B (Q.reverse a) else 0) = 0) :
    ∃ N : ℕ, 0 < N ∧ ∀ w : List A, w.length = N → (w.map B).prod = 0 := by
…

Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent