Lemma 4.11(2): weights on finite subcategories are divisible

lem:source-basis-extension(2) (scalar-normalization.tex): "Let Scal(T) denote the group of multiplicative k*-valued weights on the nonzero morphism lines of T […]. Restriction gives a split surjection Scal(T) → Scal(T'), whose kernel is a product of copies of k*, one for each connected component of R." The splitting: "Give the new line from s to the root weight one, and propagate this value along the walks by multiplying old weights […]. Lemma 4.9 ensures that the values satisfy every comparison."

We use the consequence needed in Lemma 4.13: over an algebraically closed field, the weight group of a finite subcategory is divisible (it is an iterated split extension by products of k*). Given d and n, an n-th root on T' extends over the source s by Lemma 4.9 (ratio_of_mult), and the defect on the new lines is constant along comparabilities of the support poset (the kernel), so it has a consistent n-th root.

structure MultiplicativeBasisDeformations.Thin.IsWeight {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) (d : O → O → k) : Prop

A multiplicative weight on the nonzero lines among a set of objects.

• ne (o : O) : o ∈ S → ∀ o' ∈ S, ∀ (f : o ⟶ o'), f ≠ 0 → d o o' ≠ 0
• mul (o : O) : o ∈ S → ∀ o' ∈ S, ∀ o'' ∈ S, ∀ (f : o ⟶ o') (g : o' ⟶ o''), CategoryTheory.CategoryStruct.comp f g ≠ 0 → d o o'' = d o o' * d o' o''

theorem MultiplicativeBasisDeformations.Thin.IsWeight.self {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S : Set O} {d : O → O → k} (hd : IsWeight S d) {o : O} (ho : o ∈ S) (h1 : CategoryTheory.CategoryStruct.id o ≠ 0) : d o o = 1

theorem MultiplicativeBasisDeformations.Thin.IsWeight.mono {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S S' : Set O} {d : O → O → k} (hd : IsWeight S d) (h : S' ⊆ S) : IsWeight S' d

theorem MultiplicativeBasisDeformations.Thin.weight_divisible {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [IsAlgClosed k] [Infinite k] (hT : IsThin k O) (hgt : O → ℤ) (hR : ∀ (o o' : O), Rl o o' → hgt o < hgt o') (hsrcRep : ∀ (s : O) (S : Finset O), SupRepFinite hT ⋯) {n : ℕ} (hn : 0 < n) [DecidableEq O] (m : ℕ) (S : Finset O) : S.card = m → ∀ (d : O → O → k), IsWeight (↑S) d → ∃ (e : O → O → k), IsWeight (↑S) e ∧ ∀ o ∈ S, ∀ o' ∈ S, ∀ (f : o ⟶ o'), f ≠ 0 → d o o' = e o o' ^ n

Weights on finite subcategories are divisible (Lemma 4.11(2)).