Lemma 4.12, last clause: Scal(L) is an abelian divisible group

lem:cover-exhaustion (scalar-normalization.tex): "Consequently L has a multiplicative basis, and Scal(L) is an abelian divisible group."

Scal(L) is the group of multiplicative k*-valued weights on the nonzero morphism lines of L (Thin.ScalGroup.Scal on all objects of the graded covering category). It is a subgroup of a commutative group, hence abelian. For divisibility we use Lemma 4.13 (weight_eq_ratio): every weight is a ratio of object values ζ_y / ζ_x; n-th roots of the object values (k is algebraically closed) give an n-th root of the weight. The source instead identifies Scal(L) with the inverse limit along the exhaustion, split at each step by Lemma 4.11(2).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.LCat {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) (v₀ : V) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) : Type

The category L of lifted projective vertices.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.scalFun {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} {v₀ : V} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} (d : ↥(Thin.ScalGroup.Scal k Set.univ)) : LCat Q c v₀ D → LCat Q c v₀ D → k

An element of Scal(L) as a function of pairs of objects (one off the nonzero lines).

theorem MultiplicativeBasisDeformations.MeshWalk.scalFun_isWeight {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} {v₀ : V} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (d : ↥(Thin.ScalGroup.Scal k Set.univ)) : Thin.IsWeight Set.univ (scalFun d)

theorem MultiplicativeBasisDeformations.MeshWalk.scal_abelian_divisible {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} {v₀ : V} [IsAlgClosed k] [Infinite k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) : (∀ (a b : ↥(Thin.ScalGroup.Scal k Set.univ)), a * b = b * a) ∧ ∀ (d : ↥(Thin.ScalGroup.Scal k Set.univ)) (n : ℕ), 0 < n → ∃ (e : ↥(Thin.ScalGroup.Scal k Set.univ)), e ^ n = d

Scal(L) is an abelian divisible group (Lemma 4.12, last clause).