Thin directed categories and the extension of multiplicative bases

Abstract form of Subsection 4.4 (scalar-normalization.tex). A k-linear category is thin if its Hom spaces have dimension at most one, its endomorphisms are scalars, and it is directed (no nonzero morphisms both ways between distinct objects). A multiplicative basis on a set of objects chooses a nonzero vector on each nonzero line, identities on objects, and is closed under composition up to zero.

Lemma 4.11(1) (lem:source-basis-extension): a multiplicative basis on a finite set extends over a source. The proof is the source's: choose f_y in T(s, y), write f_y b_{yz} = μ_{yz} f_z, express μ through object values by Lemma 4.9 on the support poset of Lemma 4.10, and rescale the f_y. The representation-finiteness of the incidence algebra of the support poset is a hypothesis here; it is supplied by Lemma 4.10 for the graded covering category (SupportPoset.lean). Sinks are sources of the opposite category.

structure MultiplicativeBasisDeformations.Thin.IsThin (k : Type u) [Field k] (O : Type v) [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] : Prop

A thin directed k-linear category.

• fin (o o' : O) : FiniteDimensional k (o ⟶ o')
• thin (o o' : O) : Module.finrank k (o ⟶ o') ≤ 1
• endo (o : O) (f : o ⟶ o) : ∃ (c : k), f = c • CategoryTheory.CategoryStruct.id o
• dir (o o' : O) : o ≠ o' → ∀ (f : o ⟶ o') (g : o' ⟶ o), f ≠ 0 → g = 0

theorem MultiplicativeBasisDeformations.Thin.exists_smul {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' : O} {f : o ⟶ o'} (hf : f ≠ 0) (g : o ⟶ o') : ∃ (c : k), g = c • f

Every morphism is a multiple of a nonzero one.

structure MultiplicativeBasisDeformations.Thin.MultBasis {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (S : Set O) (β : (o o' : O) → o ⟶ o') : Prop

A multiplicative basis on a set of objects.

• ne_zero (o : O) : o ∈ S → ∀ o' ∈ S, ∀ (f : o ⟶ o'), f ≠ 0 → β o o' ≠ 0
• id (o : O) : o ∈ S → β o o = CategoryTheory.CategoryStruct.id o
• mul (o : O) : o ∈ S → ∀ o' ∈ S, ∀ o'' ∈ S, CategoryTheory.CategoryStruct.comp (β o o') (β o' o'') = 0 ∨ CategoryTheory.CategoryStruct.comp (β o o') (β o' o'') = β o o''

theorem MultiplicativeBasisDeformations.Thin.MultBasis.comp_eq {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} {β : (o o' : O) → o ⟶ o'} (hβ : MultBasis S β) {o o' o'' : O} (h : o ∈ S) (h' : o' ∈ S) (h'' : o'' ∈ S) (hne : CategoryTheory.CategoryStruct.comp (β o o') (β o' o'') ≠ 0) : CategoryTheory.CategoryStruct.comp (β o o') (β o' o'') = β o o''

A nonzero composite through basis vectors is the basis vector.

The support poset of a source

def MultiplicativeBasisDeformations.Thin.SupP {O : Type v} [CategoryTheory.Category.{w, v} O] (_s : O) (P : Finset O) (_fv : (y : O) → _s ⟶ y) : Type v

The support poset: y ≤ z if some morphism y → z acts nonzero on f_y.

@[instance_reducible]

instance MultiplicativeBasisDeformations.Thin.instFintypeSupP {O : Type v} [CategoryTheory.Category.{w, v} O] (s : O) (P : Finset O) (fv : (y : O) → s ⟶ y) : Fintype (SupP s P fv)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.Thin.instDecidableEqSupP {O : Type v} [CategoryTheory.Category.{w, v} O] (s : O) (P : Finset O) (fv : (y : O) → s ⟶ y) : DecidableEq (SupP s P fv)

def MultiplicativeBasisDeformations.Thin.supLe {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] {s : O} {P : Finset O} {fv : (y : O) → s ⟶ y} (y z : SupP s P fv) : Prop

The order relation.

theorem MultiplicativeBasisDeformations.Thin.supLe_trans {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} {P : Finset O} {fv : (y : O) → s ⟶ y} (hfv : ∀ y ∈ P, fv y ≠ 0) {y z w : SupP s P fv} (h₁ : supLe y z) (h₂ : supLe z w) : supLe y w

theorem MultiplicativeBasisDeformations.Thin.supLe_antisymm {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} {P : Finset O} {fv : (y : O) → s ⟶ y} {y z : SupP s P fv} (h₁ : supLe y z) (h₂ : supLe z y) : y = z

def MultiplicativeBasisDeformations.Thin.supOrder {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} {P : Finset O} {fv : (y : O) → s ⟶ y} (hfv : ∀ y ∈ P, fv y ≠ 0) : PartialOrder (SupP s P fv)

The support poset as a partial order.

def MultiplicativeBasisDeformations.Thin.SupRepFinite {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} {P : Finset O} {fv : (y : O) → s ⟶ y} (hfv : ∀ y ∈ P, fv y ≠ 0) : Prop

The incidence algebra of the support poset, or of its dual, is representation-finite (supplied by Lemma 4.10).

Lemma 4.11(1): extension over a source

noncomputable def MultiplicativeBasisDeformations.Thin.coef {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' : O} (f g : o ⟶ o') : k

The coefficient of g along a nonzero f.

theorem MultiplicativeBasisDeformations.Thin.coef_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) {o o' : O} {f : o ⟶ o'} (hf : f ≠ 0) (g : o ⟶ o') : g = coef hT f g • f

theorem MultiplicativeBasisDeformations.Thin.coef_eq {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' : O} {f g : o ⟶ o'} (hf : f ≠ 0) {c : k} (h : g = c • f) : coef hT f g = c

theorem MultiplicativeBasisDeformations.Thin.coef_add {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' : O} {f : o ⟶ o'} (hf : f ≠ 0) (g g' : o ⟶ o') : coef hT f (g + g') = coef hT f g + coef hT f g'

theorem MultiplicativeBasisDeformations.Thin.coef_smul {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' : O} {f : o ⟶ o'} (hf : f ≠ 0) (c : k) (g : o ⟶ o') : coef hT f (c • g) = c * coef hT f g

theorem MultiplicativeBasisDeformations.Thin.coef_zero {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' : O} {f : o ⟶ o'} (hf : f ≠ 0) : coef hT f 0 = 0

theorem MultiplicativeBasisDeformations.Thin.coef_self {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' : O} {f : o ⟶ o'} (hf : f ≠ 0) : coef hT f f = 1

theorem MultiplicativeBasisDeformations.Thin.coef_sum {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' : O} {f : o ⟶ o'} (hf : f ≠ 0) {κ : Type u_1} (t : Finset κ) (g : κ → (o ⟶ o')) : coef hT f (∑ i ∈ t, g i) = ∑ i ∈ t, coef hT f (g i)

theorem MultiplicativeBasisDeformations.Thin.coef_comp {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' o'' o''' : O} {f : o ⟶ o'} {f' : o ⟶ o''} (hf : f ≠ 0) (hf' : f' ≠ 0) (g : o' ⟶ o'') (g' : o'' ⟶ o''') {f'' : o ⟶ o'''} (hf'' : f'' ≠ 0) : coef hT f'' (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g g')) = coef hT f' (CategoryTheory.CategoryStruct.comp f g) * coef hT f'' (CategoryTheory.CategoryStruct.comp f' g')

Coefficients multiply along composites.

theorem MultiplicativeBasisDeformations.Thin.coef_comp_right {k : Type u} [Field k] {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] [CategoryTheory.Linear k O] (hT : IsThin k O) {o o' o'' t : O} {f : o ⟶ t} {f' : o' ⟶ t} {f'' : o'' ⟶ t} (hf' : f' ≠ 0) (hf'' : f'' ≠ 0) (g : o'' ⟶ o') (g' : o' ⟶ o) : coef hT f'' (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp g' f)) = coef hT f' (CategoryTheory.CategoryStruct.comp g' f) * coef hT f'' (CategoryTheory.CategoryStruct.comp g f')

Coefficients multiply along composites, on the right.

noncomputable def MultiplicativeBasisDeformations.Thin.supp {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) : Finset O

The support of T(s, -) in S.

noncomputable def MultiplicativeBasisDeformations.Thin.fvec {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s y : O) : s ⟶ y

Chosen nonzero vectors f_y ∈ T(s, y).

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

theorem MultiplicativeBasisDeformations.Thin.zero_of_not_supp {O : Type v} [CategoryTheory.Category.{w, v} O] [CategoryTheory.Preadditive O] (s : O) (S : Finset O) {y : O} (hyS : y ∈ S) (hy : y ∉ supp s S) (f : s ⟶ y) : f = 0

theorem MultiplicativeBasisDeformations.Thin.extend_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) (β : (o o' : O) → o ⟶ o') (hβ : MultBasis (↑S) β) (hrep : SupRepFinite hT ⋯) : ∃ (β' : (o o' : O) → o ⟶ o'), MultBasis (insert s ↑S) β' ∧ ∀ o ∈ S, ∀ o' ∈ S, β' o o' = β o o'

Lemma 4.11(1) (lem:source-basis-extension): a multiplicative basis on S extends over a source s.