Integral weights on the graded covering category (Proposition 7.2(2))

weights-and-parameters.tex: "Every additive weight on L, with values in any abelian group, is a difference of object values." The generic statement Thin.addWeight_eq_diff applied to the graded covering category, whose exhaustion hypotheses are those of Lemma 4.12 (cov_exists_multBasis).

theorem MultiplicativeBasisDeformations.CatAlg.cov_addWeight_eq_diff {k : Type u} [Field k] [Infinite k] {𝒞 : Type v} [CategoryTheory.Category.{u, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} (H : HeightData D) [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (hF : IsRepresentationFinite k (Alg F)ᵐᵒᵖ) [Countable G] (hratio : ∀ (w' : CovObj D → CovObj D → Additive kˣ), Thin.IsAddWeight Set.univ w' → ∃ (ζ : CovObj D → Additive kˣ), ∀ (o o' : CovObj D), Thin.Line o o' → w' o o' = ζ o' - ζ o) {M : Type z} [AddCommGroup M] (w' : CovObj D → CovObj D → M) (hw : Thin.IsAddWeight Set.univ w') : ∃ (ζ : CovObj D → M), ∀ (o o' : CovObj D), Thin.Line o o' → w' o o' = ζ o' - ζ o

Proposition 7.2(2) for the graded covering category: given Lemma 4.13 (k*-weights are object ratios), additive weights with values in any abelian group are object differences.