Integral weights on thin categories (Proposition 7.2, first part)

weights-and-parameters.tex (prop:integral-ray-weights): "For a finite directed thin representation-finite category T […] let U(T) be the abelian group generated by symbols [r] for the nonidentity morphism lines r of T, with relations [rr'] = [r] + [r'] whenever rr' ≠ 0. For a source s, put T' = T ∖ {s} and form the category R of Lemma 4.11 […] Lemma 4.9 gives object values u_y ∈ U(T'), normalized to zero at one root y_D in each connected component D of R. The new nonzero-product relations are exactly [sy] + [b_yz] = [sz]. They have the universal solutions [sy] = c_D + u_y. […] Thus U(T) ≅ U(T') ⊕ ℤ^{π₀(R)}, preserving the old generators. The sink assertion follows by opposites. […] a nonzero element of the free group U(L) has a nonzero integer coordinate m, detected by a character to k* […] But Lemma 4.13 says that every such character is an object ratio".

Formalization. Weights are recorded additively (IsAddWeight), a k*-weight being an Additive kˣ-valued one. The induction over sources and sinks proves the separation property Sep T: an integer combination of lines killed by every k*-weight is killed by every weight with values in any abelian group. This is the form in which the freeness of U(T) and of its split extensions is used for the detection by characters: the universal solutions [sy] = c_D + u_y appear as the decomposition ev_insert_source, the summand ℤ^{π₀(R)} as the free constants c_D (extW), and the character detecting a nonzero coordinate as exists_zpow_ne_one. Combined with Lemma 4.13 this gives Proposition 7.2(2) (addWeight_eq_diff).

def MultiplicativeBasisDeformations.Thin.Line {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (o o' : O) : Prop

A nonzero morphism line o → o'.

structure MultiplicativeBasisDeformations.Thin.IsAddWeight {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (S : Set O) (w : O → O → M) : Prop

An additive weight on the lines of S.

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

theorem MultiplicativeBasisDeformations.Thin.IsAddWeight.mono {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] {S S' : Set O} {w : O → O → M} (hw : IsAddWeight S w) (h : S' ⊆ S) : IsAddWeight S' w

theorem MultiplicativeBasisDeformations.Thin.IsAddWeight.self {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] {S : Set O} {w : O → O → M} (hw : IsAddWeight S w) {o : O} (ho : o ∈ S) (h1 : CategoryTheory.CategoryStruct.id o ≠ 0) : w o o = 0

def MultiplicativeBasisDeformations.Thin.ev {O : Type v} {M : Type u_1} [AddCommGroup M] (w : O → O → M) (u : O × O →₀ ℤ) : M

Evaluation of a weight on an integer combination of lines.

@[simp]

theorem MultiplicativeBasisDeformations.Thin.ev_zero {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w : O → O → M) : ev w 0 = 0

theorem MultiplicativeBasisDeformations.Thin.ev_add {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w : O → O → M) (u u' : O × O →₀ ℤ) : ev w (u + u') = ev w u + ev w u'

@[simp]

theorem MultiplicativeBasisDeformations.Thin.ev_single {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w : O → O → M) (p : O × O) (n : ℤ) : (ev w fun₀ | p => n) = n • w p.1 p.2

theorem MultiplicativeBasisDeformations.Thin.ev_smul {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w : O → O → M) (n : ℤ) (u : O × O →₀ ℤ) : ev w (n • u) = n • ev w u

theorem MultiplicativeBasisDeformations.Thin.ev_neg {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w : O → O → M) (u : O × O →₀ ℤ) : ev w (-u) = -ev w u

theorem MultiplicativeBasisDeformations.Thin.ev_sub {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w : O → O → M) (u u' : O × O →₀ ℤ) : ev w (u - u') = ev w u - ev w u'

theorem MultiplicativeBasisDeformations.Thin.ev_sum {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w : O → O → M) {ι : Type u_2} (s : Finset ι) (u : ι → O × O →₀ ℤ) : ev w (∑ i ∈ s, u i) = ∑ i ∈ s, ev w (u i)

theorem MultiplicativeBasisDeformations.Thin.ev_add_weight {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w w' : O → O → M) (u : O × O →₀ ℤ) : ev (w + w') u = ev w u + ev w' u

theorem MultiplicativeBasisDeformations.Thin.ev_congr {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] {w w' : O → O → M} {u : O × O →₀ ℤ} (h : ∀ p ∈ u.support, w p.1 p.2 = w' p.1 p.2) : ev w u = ev w' u

theorem MultiplicativeBasisDeformations.Thin.ev_eq_sum {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w : O → O → M) [DecidableEq O] {T : Finset O} {u : O × O →₀ ℤ} (hu : ∀ p ∈ u.support, p.1 ∈ T ∧ p.2 ∈ T) : ev w u = ∑ o ∈ T, ∑ o' ∈ T, u (o, o') • w o o'

def MultiplicativeBasisDeformations.Thin.Supp {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) (u : O × O →₀ ℤ) : Prop

u is a combination of lines of S.

def MultiplicativeBasisDeformations.Thin.KillsK {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (k : Type u) [Field k] [CategoryTheory.Linear k O] (S : Set O) (u : O × O →₀ ℤ) : Prop

u is killed by every k*-weight on S.

def MultiplicativeBasisDeformations.Thin.KillsAll {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) (u : O × O →₀ ℤ) : Prop

u is killed by every weight on S with values in an abelian group of universe z.

def MultiplicativeBasisDeformations.Thin.Sep (k : Type u) [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (S : Set O) : Prop

Separation: on S, k*-weights detect all weights.

theorem MultiplicativeBasisDeformations.Thin.sep_empty {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] : Sep k ∅

theorem MultiplicativeBasisDeformations.Thin.exists_zpow_ne_one {k : Type u} [Field k] [Infinite k] {m : ℤ} (hm : m ≠ 0) : ∃ (t : kˣ), t ^ m ≠ 1

A unit of an infinite field which is not an m-th root of unity.

The universal group of a finite set

def MultiplicativeBasisDeformations.Thin.lineSet {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) : Set (O × O)

The lines of S.

def MultiplicativeBasisDeformations.Thin.relGens {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) : Set (O × O →₀ ℤ)

Generators of the relations of U(S); pairs that are not lines are killed.

noncomputable def MultiplicativeBasisDeformations.Thin.RelS {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) : AddSubgroup (O × O →₀ ℤ)

The relations of U(S).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Thin.US {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) : Type v

The universal group U(S) of additive weights on S.

noncomputable def MultiplicativeBasisDeformations.Thin.nw {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (S : Set O) (w : O → O → M) : O → O → M

A weight, set to zero off the lines of S.

theorem MultiplicativeBasisDeformations.Thin.ev_nw {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] {S : Set O} (w : O → O → M) {u : O × O →₀ ℤ} (hu : Supp S u) : ev (nw S w) u = ev w u

theorem MultiplicativeBasisDeformations.Thin.ev_nw_rel {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] {S : Set O} {w : O → O → M} (hw : IsAddWeight S w) (r : O × O →₀ ℤ) : r ∈ RelS S → ev (nw S w) r = 0

noncomputable def MultiplicativeBasisDeformations.Thin.liftW {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] {S : Set O} {w : O → O → M} (hw : IsAddWeight S w) : US S →+ M

The homomorphism U(S) → M of a weight.

theorem MultiplicativeBasisDeformations.Thin.liftW_mk {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] {S : Set O} {w : O → O → M} (hw : IsAddWeight S w) (u : O × O →₀ ℤ) : (liftW hw) ↑u = ev (nw S w) u

noncomputable def MultiplicativeBasisDeformations.Thin.toLines {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) (u : O × O →₀ ℤ) : O × O →₀ ℤ

The part of u on the lines of S.

theorem MultiplicativeBasisDeformations.Thin.supp_toLines {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) (u : O × O →₀ ℤ) : Supp S (toLines S u)

theorem MultiplicativeBasisDeformations.Thin.sub_toLines_mem {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) (u : O × O →₀ ℤ) : u - toLines S u ∈ RelS S

theorem MultiplicativeBasisDeformations.Thin.mk_toLines {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) (u : O × O →₀ ℤ) : ↑(toLines S u) = ↑u

Extension over a source

def MultiplicativeBasisDeformations.Thin.SLe {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s y z : O) : Prop

The support order y ≤ z of the source s.

theorem MultiplicativeBasisDeformations.Thin.comp_ne_of_sle {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {s : O} {S : Finset O} {y z x : O} (hy : y ∈ supp s S) (h₁ : ∃ (g : y ⟶ z), CategoryTheory.CategoryStruct.comp (fvec s y) g ≠ 0) (h₂ : ∃ (g : z ⟶ x), CategoryTheory.CategoryStruct.comp (fvec s z) g ≠ 0) (hz : z ∈ supp s S) : ∃ (g : y ⟶ z) (g' : z ⟶ x), CategoryTheory.CategoryStruct.comp g g' ≠ 0

theorem MultiplicativeBasisDeformations.Thin.one_ne_of_mem_supp {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {s : O} {S : Finset O} {y : O} (hy : y ∈ supp s S) : CategoryTheory.CategoryStruct.id y ≠ 0

theorem MultiplicativeBasisDeformations.Thin.line_of_sle {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {s : O} {S : Finset O} {y z : O} (hy : y ∈ supp s S) (h : SLe s y z) : Line y z

theorem MultiplicativeBasisDeformations.Thin.mem_S_of_supp {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {s : O} {S : Finset O} {y : O} (hy : y ∈ supp s S) : y ∈ S

theorem MultiplicativeBasisDeformations.Thin.exists_zz {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {s : O} {S : Finset O} [Infinite k] (hrep : SupRepFinite hT ⋯) : ∃ (zz : O → O × O →₀ ℤ), (∀ (y : O), Supp (↑S) (zz y)) ∧ ∀ y ∈ supp s S, ∀ x ∈ supp s S, SLe s y x → (↑fun₀ | (y, x) => 1) = ↑(zz x) - ↑(zz y)

Universal object values on the support poset (Lemma 4.9 applied to the universal weight [y z] with values in U(S)): fixed integer combinations zz y of lines of S with w(y,z) = w(zz z) − w(zz y) for every weight w.

theorem MultiplicativeBasisDeformations.Thin.zz_eval {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {s : O} {S : Finset O} {zz : O → O × O →₀ ℤ} (hzz₁ : ∀ (y : O), Supp (↑S) (zz y)) (hzzU : ∀ y ∈ supp s S, ∀ x ∈ supp s S, SLe s y x → (↑fun₀ | (y, x) => 1) = ↑(zz x) - ↑(zz y)) {M : Type u_1} [AddCommGroup M] {w : O → O → M} (hw : IsAddWeight (↑S) w) {y x : O} (hy : y ∈ supp s S) (hx : x ∈ supp s S) (hyx : SLe s y x) : w y x = ev w (zz x) - ev w (zz y)

The values w(zz y) are object values of every weight on the support poset.

theorem MultiplicativeBasisDeformations.Thin.exists_root {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {s : O} {S : Finset O} : ∃ (root : O → O), (∀ y ∈ supp s S, root y ∈ supp s S) ∧ (∀ y ∈ supp s S, ∀ x ∈ supp s S, SLe s y x → root y = root x) ∧ (∀ y ∈ supp s S, root (root y) = root y) ∧ ∀ y ∈ supp s S, Relation.EqvGen (fun (a b : O) => a ∈ supp s S ∧ b ∈ supp s S ∧ SLe s a b) y (root y)

Roots of the components of the support poset.

noncomputable def MultiplicativeBasisDeformations.Thin.extW {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (s : O) (S : Finset O) (zz : O → O × O →₀ ℤ) (root : O → O) (w₀ : O → O → M) (a : O → M) : O → O → M

The weight on S ∪ {s} extending w₀ with constants a on the components.

theorem MultiplicativeBasisDeformations.Thin.ev_extW {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {s : O} {S : Finset O} {zz : O → O × O →₀ ℤ} {root : O → O} (hsS : s ∉ S) {M : Type u_1} [AddCommGroup M] (w₀ : O → O → M) (a : O → M) {v : O × O →₀ ℤ} (hv : Supp (↑S) v) : ev (extW s S zz root w₀ a) v = ev w₀ v

theorem MultiplicativeBasisDeformations.Thin.extW_isAddWeight {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {s : O} {S : Finset O} {zz : O → O × O →₀ ℤ} {root : O → O} (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) (hzz₁ : ∀ (y : O), Supp (↑S) (zz y)) (hzz₂ : ∀ y ∈ supp s S, ∀ x ∈ supp s S, SLe s y x → (↑fun₀ | (y, x) => 1) = ↑(zz x) - ↑(zz y)) (hr₂ : ∀ y ∈ supp s S, ∀ x ∈ supp s S, SLe s y x → root y = root x) {M : Type u_1} [AddCommGroup M] {w₀ : O → O → M} (hw₀ : IsAddWeight (↑S) w₀) (a : O → M) : IsAddWeight (insert s ↑S) (extW s S zz root w₀ a)

theorem MultiplicativeBasisDeformations.Thin.ev_insert_source {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {s : O} {S : Finset O} {zz : O → O × O →₀ ℤ} {root : O → O} (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) (hzz₁ : ∀ (y : O), Supp (↑S) (zz y)) (hzz₂ : ∀ y ∈ supp s S, ∀ x ∈ supp s S, SLe s y x → (↑fun₀ | (y, x) => 1) = ↑(zz x) - ↑(zz y)) (hr₄ : ∀ y ∈ supp s S, Relation.EqvGen (fun (a b : O) => a ∈ supp s S ∧ b ∈ supp s S ∧ SLe s a b) y (root y)) {M : Type u_1} [AddCommGroup M] {w : O → O → M} (hw : IsAddWeight (insert s ↑S) w) {u : O × O →₀ ℤ} (hu : Supp (insert s ↑S) u) : ev w u = ev w (toLines (↑S) u + ∑ y ∈ supp s S, u (s, y) • zz y) + ∑ r ∈ Finset.image root (supp s S), (∑ y ∈ supp s S with root y = r, u (s, y)) • (w s r - ev w (zz r))

The universal solutions [sy] = c_D + u_y: decomposition of a combination of lines of S ∪ {s}.

theorem MultiplicativeBasisDeformations.Thin.ev_zero_weight {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (u : O × O →₀ ℤ) : ev 0 u = 0

theorem MultiplicativeBasisDeformations.Thin.Supp.add {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {u u' : O × O →₀ ℤ} (hu : Supp S u) (hu' : Supp S u') : Supp S (u + u')

theorem MultiplicativeBasisDeformations.Thin.Supp.smul {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {u : O × O →₀ ℤ} (hu : Supp S u) (n : ℤ) : Supp S (n • u)

theorem MultiplicativeBasisDeformations.Thin.Supp.sum {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {ι : Type u_1} (t : Finset ι) {u : ι → O × O →₀ ℤ} (hu : ∀ i ∈ t, Supp S (u i)) : Supp S (∑ i ∈ t, u i)

theorem MultiplicativeBasisDeformations.Thin.sep_insert_source {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) [Infinite k] {s : O} {S : Finset O} (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) (hrep : SupRepFinite hT ⋯) (hS : Sep k ↑S) : Sep k (insert s ↑S)

Separation passes to the extension by a source (U(T) ≅ U(T') ⊕ ℤ^{π₀(R)}).

Opposites and the sink step

noncomputable def MultiplicativeBasisDeformations.Thin.uop {O : Type v} (u : O × O →₀ ℤ) : Oᵒᵖ × Oᵒᵖ →₀ ℤ

The reversed combination of lines in Oᵒᵖ.

def MultiplicativeBasisDeformations.Thin.wop {O : Type v} {M : Type u_1} (w : O → O → M) : Oᵒᵖ → Oᵒᵖ → M

The reversed weight.

def MultiplicativeBasisDeformations.Thin.wunop {O : Type v} {M : Type u_1} (W : Oᵒᵖ → Oᵒᵖ → M) : O → O → M

The weight on O of a weight on Oᵒᵖ.

theorem MultiplicativeBasisDeformations.Thin.wop_wunop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} (W : Oᵒᵖ → Oᵒᵖ → M) : wop (wunop W) = W

theorem MultiplicativeBasisDeformations.Thin.ev_uop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (w : O → O → M) (u : O × O →₀ ℤ) : ev (wop w) (uop u) = ev w u

theorem MultiplicativeBasisDeformations.Thin.line_op_iff {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {X Y : Oᵒᵖ} : Line X Y ↔ Line (Opposite.unop Y) (Opposite.unop X)

theorem MultiplicativeBasisDeformations.Thin.isAddWeight_wop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] {S : Set O} {w : O → O → M} (hw : IsAddWeight S w) : IsAddWeight (Opposite.unop ⁻¹' S) (wop w)

theorem MultiplicativeBasisDeformations.Thin.isAddWeight_wunop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] {S : Set O} {W : Oᵒᵖ → Oᵒᵖ → M} (hW : IsAddWeight (Opposite.unop ⁻¹' S) W) : IsAddWeight S (wunop W)

theorem MultiplicativeBasisDeformations.Thin.supp_uop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {u : O × O →₀ ℤ} (hu : Supp S u) : Supp (Opposite.unop ⁻¹' S) (uop u)

theorem MultiplicativeBasisDeformations.Thin.sep_of_sep_op {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S : Set O} (h : Sep k (Opposite.unop ⁻¹' S)) : Sep k S

noncomputable def MultiplicativeBasisDeformations.Thin.uunop {O : Type v} (U : Oᵒᵖ × Oᵒᵖ →₀ ℤ) : O × O →₀ ℤ

The reversed combination of lines of O from Oᵒᵖ.

theorem MultiplicativeBasisDeformations.Thin.ev_uunop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (W : Oᵒᵖ → Oᵒᵖ → M) (U : Oᵒᵖ × Oᵒᵖ →₀ ℤ) : ev (wunop W) (uunop U) = ev W U

theorem MultiplicativeBasisDeformations.Thin.supp_uunop {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {U : Oᵒᵖ × Oᵒᵖ →₀ ℤ} (hU : Supp (Opposite.unop ⁻¹' S) U) : Supp S (uunop U)

theorem MultiplicativeBasisDeformations.Thin.sep_op_of_sep {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S : Set O} (h : Sep k S) : Sep k (Opposite.unop ⁻¹' S)

theorem MultiplicativeBasisDeformations.Thin.sep_insert_sink {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) [Infinite k] {t : O} {S : Finset O} (htS : t ∉ S) (hsnk : ∀ o ∈ S, ∀ (f : t ⟶ o), f = 0) (hrep : SupRepFinite ⋯ ⋯) (hS : Sep k ↑S) : Sep k (insert t ↑S)

Separation passes to the extension by a sink, by opposites.

Extension of weights over one step

theorem MultiplicativeBasisDeformations.Thin.ext_insert_source {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) [Infinite k] {s : O} {S : Finset O} (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) (hrep : SupRepFinite hT ⋯) {M : Type u_1} [AddCommGroup M] {w₀ : O → O → M} (hw₀ : IsAddWeight (↑S) w₀) : ∃ (w : O → O → M), IsAddWeight (insert s ↑S) w ∧ ∀ o ∈ S, ∀ o' ∈ S, w o o' = w₀ o o'

theorem MultiplicativeBasisDeformations.Thin.ext_insert_sink {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) [Infinite k] {t : O} {S : Finset O} (htS : t ∉ S) (hsnk : ∀ o ∈ S, ∀ (f : t ⟶ o), f = 0) (hrep : SupRepFinite ⋯ ⋯) {M : Type u_1} [AddCommGroup M] {w₀ : O → O → M} (hw₀ : IsAddWeight (↑S) w₀) : ∃ (w : O → O → M), IsAddWeight (insert t ↑S) w ∧ ∀ o ∈ S, ∀ o' ∈ S, w o o' = w₀ o o'

Filling and the exhaustion

theorem MultiplicativeBasisDeformations.Thin.fill_sep {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [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 ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) [DecidableEq O] (n : ℕ) (T T' : Finset O) : (T' \ T).card = n → T ⊆ T' → Convex ↑T → Convex ↑T' → (Sep k ↑T → Sep k ↑T') ∧ ∀ (M : Type z₂) [inst : AddCommGroup M] (w₀ : O → O → M), IsAddWeight (↑T) w₀ → ∃ (w : O → O → M), IsAddWeight (↑T') w ∧ ∀ o ∈ T, ∀ o' ∈ T, w o o' = w₀ o o'

Filling a convex set: separation and extension of weights.

theorem MultiplicativeBasisDeformations.Thin.sep_exT {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [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 ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) (e : ℕ → O) [DecidableEq O] (n : ℕ) : Sep k ↑(exT hgt hR hsucc e n)

def MultiplicativeBasisDeformations.Thin.extSeq {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [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 ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) (e : ℕ → O) [DecidableEq O] (n : ℕ) (M : Type z₂) [AddCommGroup M] (w₀ : O → O → M) (hw₀ : IsAddWeight (↑(exT hgt hR hsucc e n)) w₀) (j : ℕ) : { w' : O → O → M // IsAddWeight (↑(exT hgt hR hsucc e (n + j))) w' }

The sequence of extensions of a weight along the exhaustion.

theorem MultiplicativeBasisDeformations.Thin.extSeq_succ {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [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 ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) (e : ℕ → O) [DecidableEq O] (n : ℕ) (M : Type z₂) [AddCommGroup M] (w₀ : O → O → M) (hw₀ : IsAddWeight (↑(exT hgt hR hsucc e n)) w₀) (j : ℕ) (o : O) : o ∈ exT hgt hR hsucc e (n + j) → ∀ o' ∈ exT hgt hR hsucc e (n + j), ↑(extSeq hT hgt hR hsrcRep hsnkRep hsucc e n M w₀ hw₀ (j + 1)) o o' = ↑(extSeq hT hgt hR hsrcRep hsnkRep hsucc e n M w₀ hw₀ j) o o'

theorem MultiplicativeBasisDeformations.Thin.extSeq_agree {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [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 ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) (e : ℕ → O) [DecidableEq O] (n : ℕ) (M : Type z₂) [AddCommGroup M] (w₀ : O → O → M) (hw₀ : IsAddWeight (↑(exT hgt hR hsucc e n)) w₀) {i j : ℕ} (hij : i ≤ j) (o : O) : o ∈ exT hgt hR hsucc e (n + i) → ∀ o' ∈ exT hgt hR hsucc e (n + i), ↑(extSeq hT hgt hR hsrcRep hsnkRep hsucc e n M w₀ hw₀ j) o o' = ↑(extSeq hT hgt hR hsrcRep hsnkRep hsucc e n M w₀ hw₀ i) o o'

theorem MultiplicativeBasisDeformations.Thin.exists_ext_univ {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [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 ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) (e : ℕ → O) [DecidableEq O] (he : Function.Surjective e) (n : ℕ) (M : Type z₂) [AddCommGroup M] (w₀ : O → O → M) (hw₀ : IsAddWeight (↑(exT hgt hR hsucc e n)) w₀) : ∃ (w' : O → O → M), IsAddWeight Set.univ w' ∧ ∀ o ∈ exT hgt hR hsucc e n, ∀ o' ∈ exT hgt hR hsucc e n, w' o o' = w₀ o o'

Weights on a stage of the exhaustion extend to all objects.

Boundaries and the main theorem

noncomputable def MultiplicativeBasisDeformations.Thin.bd {O : Type v} (u : O × O →₀ ℤ) : O →₀ ℤ

The boundary ∂[o → o'] = e_{o'} − e_o.

theorem MultiplicativeBasisDeformations.Thin.bd_add {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (u u' : O × O →₀ ℤ) : bd (u + u') = bd u + bd u'

@[simp]

theorem MultiplicativeBasisDeformations.Thin.bd_single {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (p : O × O) (n : ℤ) : (bd fun₀ | p => n) = (fun₀ | p.2 => n) - fun₀ | p.1 => n

theorem MultiplicativeBasisDeformations.Thin.bd_zero {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] : bd 0 = 0

theorem MultiplicativeBasisDeformations.Thin.bd_neg {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (u : O × O →₀ ℤ) : bd (-u) = -bd u

theorem MultiplicativeBasisDeformations.Thin.bd_sub {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (u u' : O × O →₀ ℤ) : bd (u - u') = bd u - bd u'

theorem MultiplicativeBasisDeformations.Thin.ev_diff {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {M : Type u_1} [AddCommGroup M] (ζ : O → M) (u : O × O →₀ ℤ) : ev (fun (o o' : O) => ζ o' - ζ o) u = (bd u).sum fun (o : O) (n : ℤ) => n • ζ o

A weight of object differences evaluates through the boundary.

theorem MultiplicativeBasisDeformations.Thin.exists_zigzag {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {a b : O} (h : Relation.EqvGen (fun (o o' : O) => Line o o') a b) : ∃ (u : O × O →₀ ℤ), Supp Set.univ u ∧ bd u = (fun₀ | b => 1) - fun₀ | a => 1

theorem MultiplicativeBasisDeformations.Thin.addWeight_eq_diff {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] [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 ⋯) (hsnkRep : ∀ (t : O) (S : Finset O), SupRepFinite ⋯ ⋯) (hsucc : ∀ (o : O), {o' : O | Rl o o'}.Finite) (e : ℕ → O) (he : Function.Surjective e) (hratio : ∀ (w' : O → O → Additive kˣ), IsAddWeight Set.univ w' → ∃ (ζ : O → Additive kˣ), ∀ (o o' : O), Line o o' → w' o o' = ζ o' - ζ o) {M : Type z} [AddCommGroup M] (w' : O → O → M) (hw : IsAddWeight Set.univ w') : ∃ (ζ : O → M), ∀ (o o' : O), Line o o' → w' o o' = ζ o' - ζ o

Proposition 7.2(2) (prop:integral-ray-weights), in the generic form: if every k*-weight on the whole category is a ratio of object values (Lemma 4.13), then every additive weight with values in any abelian group is a difference of object values.