The local structure of a finite-dimensional scalar mesh category

Proof of Lemma 2.7 (graded-category.tex): "The positive-degree ideal is nilpotent, each degree-zero endomorphism ring is k, and degree-zero maps between distinct objects vanish; so this ideal is the categorical radical." For a finite-dimensional scalar mesh category on a finite translation quiver we take as radical the span of the images of paths of positive length (radN 1) and verify the axioms of LocalFamily.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.radN {k : Type u} [Field k] {V : Type} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (n : ℕ) (x y : V) : Submodule k (obj c x ⟶ obj c y)

The span of the images of paths of length at least n.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.pathMor_mem_radN {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {n : ℕ} {x y : V} (p : Quiver.Path x y) (hp : n ≤ p.length) : pathMor c p ∈ radN c n x y

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.radN_comp {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {m n : ℕ} {x y z : V} {f : obj c x ⟶ obj c y} {g : obj c y ⟶ obj c z} (hf : f ∈ radN c m x y) (hg : g ∈ radN c n y z) : CategoryTheory.CategoryStruct.comp f g ∈ radN c (m + n) x z

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.mem_radN_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x y : V} (f : obj c x ⟶ obj c y) : f ∈ radN c 0 x y

Every morphism lies in radN 0.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.radN_eq_bot {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (obj c x ⟶ obj c y)) : ∃ (N : ℕ), ∀ (x y : V), radN c N x y = ⊥

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.proj_zero_mem_ideal {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x y : V} {F : LinearPaths.obj x ⟶ LinearPaths.obj y} (hF : (RelationCategory.functor k (meshRelations c)).map F = 0) : (LinearPaths.proj 0 x y) F = 0

The degree-zero projection kills the mesh ideal.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.sub_proj_zero_mem {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x y : V} (F : LinearPaths.obj x ⟶ LinearPaths.obj y) : (RelationCategory.functor k (meshRelations c)).map (F - (LinearPaths.proj 0 x y) F) ∈ radN c 1 x y

The positive-length part of a morphism of kQ maps into radN 1.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.pathMor_nil_ne_zero {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x : V) : pathMor c Quiver.Path.nil ≠ 0

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.id_not_mem_radN {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x : V) : CategoryTheory.CategoryStruct.id (obj c x) ∉ radN c 1 x x

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.pow_mem_radN {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x : V} {f : CategoryTheory.End (obj c x)} (hf : f ∈ radN c 1 x x) (n : ℕ) : f ^ n ∈ radN c n x x

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.prod_mem_radN {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (l : List (CatAlg.Alg fun (x : V) => obj c x)) (hl : ∀ a ∈ l, ∀ (y z : V), a y z ∈ radN c 1 y z) (y z : V) : l.prod y z ∈ radN c l.length y z

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.exists_lastArrow {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {w x : V} {f : obj c w ⟶ obj c x} (hf : f ∈ radN c 1 w x) : ∃ (g : (a : (y : V) × (y ⟶ x)) → obj c w ⟶ obj c a.fst), f = ∑ a : (y : V) × (y ⟶ x), CategoryTheory.CategoryStruct.comp (g a) (arrowMor c a.snd)

graded-category.tex: every positive-degree morphism into x is a sum of composites with the arrows ending at x.

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.arrowMor_mem_radN {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x y : V} (a : x ⟶ y) : arrowMor c a ∈ radN c 1 x y

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.localFamily {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (hfin : ∀ (x y : V), FiniteDimensional k (obj c x ⟶ obj c y)) : CatAlg.LocalFamily fun (x : V) => obj c x

The local structure of a finite-dimensional scalar mesh category.