Lemma 4.11(2): restriction of multiplicative weights over a source

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, meaning assignments d(r) with d(rr') = d(r)d(r') whenever rr' ≠ 0. 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."

Here T = S ∪ {s} for a source s (NzLine, Scal, res). The kernel is identified with the functions on the connected components of the support poset of s (kerEquiv): a weight trivial on T' is determined by its values on the new lines s → y, which are constant along the comparabilities. The splitting (ext, res_ext) is the source's: on each component the new values are the object values of Lemma 4.9 (ratio_of_mult), normalized to one at a chosen root; the normalization makes them unique, hence multiplicative in the weight.

Lines and weights

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

A nonzero morphism line between objects of S.

• o : O
• o' : O
• mem : self.o ∈ S
• mem' : self.o' ∈ S
• nz : ∃ (f : self.o ⟶ self.o'), f ≠ 0

def MultiplicativeBasisDeformations.Thin.ScalGroup.mkLine {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {o o' : O} (h : o ∈ S) (h' : o' ∈ S) (f : o ⟶ o') (hf : f ≠ 0) : NzLine S

The line of a nonzero morphism.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.NzLine.ext' {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S : Set O} {ℓ ℓ' : NzLine S} (h1 : ℓ.o = ℓ'.o) (h2 : ℓ.o' = ℓ'.o') : ℓ = ℓ'

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.left_ne {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {o o' o'' : O} {f : o ⟶ o'} {g : o' ⟶ o''} (h : CategoryTheory.CategoryStruct.comp f g ≠ 0) : f ≠ 0

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.right_ne {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {o o' o'' : O} {f : o ⟶ o'} {g : o' ⟶ o''} (h : CategoryTheory.CategoryStruct.comp f g ≠ 0) : g ≠ 0

def MultiplicativeBasisDeformations.Thin.ScalGroup.Scal (k : Type u) [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) : Subgroup (NzLine S → kˣ)

Scal(S): multiplicative k*-valued weights on the nonzero lines of S.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.scal_mul {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S : Set O} (d : ↥(Scal k S)) {o o' o'' : O} (h : o ∈ S) (h' : o' ∈ S) (h'' : o'' ∈ S) (f : o ⟶ o') (g : o' ⟶ o'') (hfg : CategoryTheory.CategoryStruct.comp f g ≠ 0) : ↑d (mkLine h h'' (CategoryTheory.CategoryStruct.comp f g) hfg) = ↑d (mkLine h h' f ⋯) * ↑d (mkLine h' h'' g ⋯)

def MultiplicativeBasisDeformations.Thin.ScalGroup.NzLine.incl {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S S' : Set O} (hS : S' ⊆ S) (ℓ : NzLine S') : NzLine S

Lines of a subset are lines of the set.

def MultiplicativeBasisDeformations.Thin.ScalGroup.res (k : Type u) [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {S S' : Set O} (hS : S' ⊆ S) : ↥(Scal k S) →* ↥(Scal k S')

Restriction Scal(S) → Scal(S').

@[simp]

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.res_apply {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] {S S' : Set O} (hS : S' ⊆ S) (d : ↥(Scal k S)) (ℓ : NzLine S') : ↑((res k hS) d) ℓ = ↑d (NzLine.incl hS ℓ)

Over a source

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Thin.ScalGroup.Tset {O : Type v} (s : O) (S : Finset O) : Set O

T = T' ∪ {s}.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.sub_T {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) : ↑S ⊆ Tset s S

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Thin.ScalGroup.Sp {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) : Type v

The support poset of the source.

def MultiplicativeBasisDeformations.Thin.ScalGroup.compSetoid {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) : Setoid (Sp s S)

The connected components of the support poset (the components of R).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Thin.ScalGroup.Comp {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) : Type v

The set of components.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.supp_sub {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

noncomputable def MultiplicativeBasisDeformations.Thin.ScalGroup.newLine {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) (y : Sp s S) : NzLine (Tset s S)

The new line s → y.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.ne_s_of_mem {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) (hsS : s ∉ S) {y : O} (hy : y ∈ S) : y ≠ s

noncomputable def MultiplicativeBasisDeformations.Thin.ScalGroup.onNew {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) (d : ↥(Scal k (Tset s S))) (y : Sp s S) : kˣ

The values of a weight on the new lines.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.onNew_le {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) (d : ↥(Scal k (Tset s S))) (hd : (res k ⋯) d = 1) {a b : Sp s S} (hab : supLe a b) : onNew s S d b = onNew s S d a

In the kernel, the new values are constant along comparabilities.

noncomputable def MultiplicativeBasisDeformations.Thin.ScalGroup.kerToComp {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) (d : ↥(res k ⋯).ker) : Comp s S → kˣ

The kernel values, on components.

noncomputable def MultiplicativeBasisDeformations.Thin.ScalGroup.dfun {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) (κ : Comp s S → kˣ) (ℓ : NzLine (Tset s S)) : kˣ

The weight with prescribed values on the new lines and trivial on T'.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.mem_S_of_ne {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) {o : O} (h : o ∈ Tset s S) (hs : o ≠ s) : o ∈ S

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.dfun_new {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (s : O) (S : Finset O) (κ : Comp s S → kˣ) {y : O} (hy : y ∈ supp s S) (ℓ : NzLine (Tset s S)) (h1 : ℓ.o = s) (h2 : ℓ.o' = y) : dfun s S κ ℓ = κ ⟦⟨y, hy⟩⟧

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.dfun_old {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (s : O) (S : Finset O) (κ : Comp s S → kˣ) (ℓ : NzLine (Tset s S)) (h : ¬(ℓ.o = s ∧ ℓ.o' ∈ supp s S)) : dfun s S κ ℓ = 1

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.dfun_mem {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) (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) (κ : Comp s S → kˣ) : dfun s S κ ∈ Scal k (Tset s S)

noncomputable def MultiplicativeBasisDeformations.Thin.ScalGroup.compToKer {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) (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) (κ : Comp s S → kˣ) : ↥(res k ⋯).ker

The kernel element with prescribed values on the components.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.scal_diag {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' : Set O} (d : ↥(Scal k S')) (ℓ : NzLine S') (h : ℓ.o' = ℓ.o) : ↑d ℓ = 1

A weight is one on the line of an object to itself.

noncomputable def MultiplicativeBasisDeformations.Thin.ScalGroup.kerEquiv {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) (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) : ↥(res k ⋯).ker ≃* (Comp s S → kˣ)

The kernel of restriction is a product of copies of k*, one for each connected component of the support poset.

The splitting

def MultiplicativeBasisDeformations.Thin.ScalGroup.oldLine {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) (a b : Sp s S) (g : ↑a ⟶ ↑b) (hg : g ≠ 0) : NzLine ↑S

The old line a → b of a comparability in the support poset.

def MultiplicativeBasisDeformations.Thin.ScalGroup.IsNormVal {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) (d : ↥(Scal k ↑S)) (ζ : Sp s S → kˣ) : Prop

Normalized object values for a weight d on T': they change by d along every comparability, and are one at the chosen root of each component.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.normVal_unique {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) {d : ↥(Scal k ↑S)} {ζ ζ' : Sp s S → kˣ} (h : IsNormVal s S d ζ) (h' : IsNormVal s S d ζ') : ζ = ζ'

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.exists_normVal {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 ⋯) (d : ↥(Scal k ↑S)) : ∃ (ζ : Sp s S → kˣ), IsNormVal s S d ζ

noncomputable def MultiplicativeBasisDeformations.Thin.ScalGroup.zeta {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 ⋯) (d : ↥(Scal k ↑S)) : Sp s S → kˣ

The chosen normalized object values.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.zeta_spec {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 ⋯) (d : ↥(Scal k ↑S)) : IsNormVal s S d (zeta hT s S hrep d)

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.zeta_mul {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 ⋯) (d e : ↥(Scal k ↑S)) : zeta hT s S hrep (d * e) = zeta hT s S hrep d * zeta hT s S hrep e

noncomputable def MultiplicativeBasisDeformations.Thin.ScalGroup.extFun {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 ⋯) (d : ↥(Scal k ↑S)) (ℓ : NzLine (Tset s S)) : kˣ

The extended weight: normalized object values on the new lines.

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.extFun_new {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 ⋯) (d : ↥(Scal k ↑S)) {y : O} (hy : y ∈ supp s S) (ℓ : NzLine (Tset s S)) (h1 : ℓ.o = s) (h2 : ℓ.o' = y) : extFun hT s S hrep d ℓ = zeta hT s S hrep d ⟨y, hy⟩

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.extFun_old {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) (hsS : s ∉ S) [Infinite k] (hrep : SupRepFinite hT ⋯) (d : ↥(Scal k ↑S)) (ℓ : NzLine (Tset s S)) (h1 : ℓ.o ∈ S) (h2 : ℓ.o' ∈ S) : extFun hT s S hrep d ℓ = ↑d { o := ℓ.o, o' := ℓ.o', mem := ⋯, mem' := ⋯, nz := ⋯ }

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.extFun_ss {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) (hsS : s ∉ S) [Infinite k] (hrep : SupRepFinite hT ⋯) (d : ↥(Scal k ↑S)) (ℓ : NzLine (Tset s S)) (h1 : ℓ.o = s) (h2 : ℓ.o' = s) : extFun hT s S hrep d ℓ = 1

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.extFun_mem {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) (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) [Infinite k] (hrep : SupRepFinite hT ⋯) (d : ↥(Scal k ↑S)) : extFun hT s S hrep d ∈ Scal k (Tset s S)

noncomputable def MultiplicativeBasisDeformations.Thin.ScalGroup.ext {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) (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) [Infinite k] (hrep : SupRepFinite hT ⋯) : ↥(Scal k ↑S) →* ↥(Scal k (Tset s S))

The splitting Scal(T') → Scal(T).

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.res_ext {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) (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) [Infinite k] (hrep : SupRepFinite hT ⋯) (d : ↥(Scal k ↑S)) : (res k ⋯) ((ext hT s S hsS hsrc hrep) d) = d

theorem MultiplicativeBasisDeformations.Thin.ScalGroup.sourceScalSplit {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) (hsS : s ∉ S) (hsrc : ∀ o ∈ S, ∀ (f : o ⟶ s), f = 0) [Infinite k] (hrep : SupRepFinite hT ⋯) : (∃ (e : ↥(Scal k ↑S) →* ↥(Scal k (Tset s S))), ∀ (d : ↥(Scal k ↑S)), (res k ⋯) (e d) = d) ∧ Function.Surjective ⇑(res k ⋯) ∧ Nonempty (↥(res k ⋯).ker ≃* (Comp s S → kˣ))

Lemma 4.11(2) (lem:source-basis-extension): for a source s of T = T' ∪ {s}, restriction Scal(T) → Scal(T') is a split surjection, and its kernel is a product of copies of k*, one for each connected component of the support poset of s (the components of R).