The radical of a finite scalar mesh category is its positive part #
For a finite-dimensional scalar mesh category C(Q, c), the morphisms of degree at least m
(Ge m) are closed under composition with degrees adding (ge_comp), vanish for m large
(exists_ge_eq_zero), and a morphism is radical (1 - fg invertible for all g) exactly when
its degree-zero part vanishes (radical_iff). This is the input gr_J C = C of the proof of
Corollary 4.15 (scalar-normalization.tex).
def
MultiplicativeBasisDeformations.MeshWalk.Ge
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(c : MeshCoefficients k Q)
(m : ℕ)
{x y : V}
(f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)
:
Morphisms of degree at least m.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.ge_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 : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)
:
Ge c 0 f
theorem
MultiplicativeBasisDeformations.MeshWalk.ge_of_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}
{d m : ℕ}
{x y : V}
{f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hf : f ∈ ScalarMeshCategory.degreePart c d x y)
(hd : m ≤ d)
:
Ge c m f
theorem
MultiplicativeBasisDeformations.MeshWalk.Ge.mono
{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 m' : ℕ}
{x y : V}
{f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hf : Ge c m f)
(h : m' ≤ m)
:
Ge c m' f
theorem
MultiplicativeBasisDeformations.MeshWalk.Ge.add
{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 : ℕ}
{x y : V}
{f g : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hf : Ge c m f)
(hg : Ge c m g)
:
Ge c m (f + g)
theorem
MultiplicativeBasisDeformations.MeshWalk.Ge.sub
{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 : ℕ}
{x y : V}
{f g : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hf : Ge c m f)
(hg : Ge c m g)
:
Ge c m (f - g)
theorem
MultiplicativeBasisDeformations.MeshWalk.Ge.smul
{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 : ℕ}
{x y : V}
(t : k)
{f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hf : Ge c m f)
:
Ge c m (t • f)
theorem
MultiplicativeBasisDeformations.MeshWalk.Ge.neg
{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 : ℕ}
{x y : V}
{f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hf : Ge c m f)
:
Ge c m (-f)
theorem
MultiplicativeBasisDeformations.MeshWalk.ge_zero_mor
{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 : ℕ)
{x y : V}
:
Ge c m 0
theorem
MultiplicativeBasisDeformations.MeshWalk.ge_sum
{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 : ℕ)
{x y : V}
{ι : Type u_1}
(s : Finset ι)
{f : ι → (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)}
(hf : ∀ i ∈ s, Ge c m (f i))
:
Ge c m (∑ i ∈ s, f i)
theorem
MultiplicativeBasisDeformations.MeshWalk.degProj_eq_of_ge
{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 : ℕ}
{x y : V}
{f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
(hf : Ge c m f)
{d : ℕ}
(hd : d < m)
:
(ScalarMeshCategory.degProj c d x y) f = 0
theorem
MultiplicativeBasisDeformations.MeshWalk.ge_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}
[Finite V]
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{m m' : ℕ}
{x y z : V}
{f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y}
{g : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c z}
(hf : Ge c m f)
(hg : Ge c m' g)
:
Ge c (m + m') (CategoryTheory.CategoryStruct.comp f g)
Composition adds degrees.
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_ge_eq_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}
[Finite V]
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
:
∃ (N : ℕ), ∀ (x y : V) (f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y), Ge c N f → f = 0
theorem
MultiplicativeBasisDeformations.MeshWalk.degProj_id
{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}
[Finite V]
(x : V)
:
(ScalarMeshCategory.degProj c 0 x x) (CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c x)) = CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c x)
theorem
MultiplicativeBasisDeformations.MeshWalk.id_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}
[Finite V]
(x : V)
:
CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c x) ≠ 0
theorem
MultiplicativeBasisDeformations.MeshWalk.isNilpotent_of_ge
{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}
[Finite V]
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{x : V}
(f : CategoryTheory.End (ScalarMeshCategory.obj c x))
(hf : Ge c 1 f)
:
IsNilpotent f
theorem
MultiplicativeBasisDeformations.MeshWalk.isIso_id_sub
{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}
[Finite V]
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{x : V}
(f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c x)
(hf : Ge c 1 f)
:
CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c x) - f)
theorem
MultiplicativeBasisDeformations.MeshWalk.not_isIso_of_ge
{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}
[Finite V]
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{x : V}
(f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c x)
(hf : Ge c 1 f)
:
¬CategoryTheory.IsIso f
theorem
MultiplicativeBasisDeformations.MeshWalk.radical_iff
{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}
[Finite V]
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{x y : V}
(f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)
:
(∀ (g : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c x),
CategoryTheory.IsIso
(CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c x) - CategoryTheory.CategoryStruct.comp f g)) ↔ (ScalarMeshCategory.degProj c 0 x y) f = 0
The radical of C(Q, c) is its positive part.
theorem
MultiplicativeBasisDeformations.MeshWalk.eq_of_comp_eq_id
{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}
[Finite V]
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{x y : V}
(f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)
(g : ScalarMeshCategory.obj c y ⟶ ScalarMeshCategory.obj c x)
(h : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c x))
:
x = y
Distinct vertices are not isomorphic.