A multiplicative basis of A₀ from homogeneous vectors

Proposition 4.14 (scalar-normalization.tex): the invariant basis "descends to one vector on each homogeneous ray line of A₀: such a line lies in one deck degree […]. Products lift uniquely, so every nonzero coefficient downstairs is one."

For a graded family whose nonzero homogeneous pieces A(x, y)_g are lines spanned by chosen vectors b(x, y, g) closed under composition up to zero, with identities b(x, x, 1) = 𝟙, the matrix units of the b(x, y, g) form a basis of (Alg F)ᵒᵖ (basisA0) which is multiplicative and contains the idempotents of the labels (basisA0_isMultiplicative, basisA0_idempotents).

Matrix units of the category algebra

def MultiplicativeBasisDeformations.CatAlg.unitM {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [DecidableEq ι] {F : ι → 𝒞} (x y : ι) (f : F x ⟶ F y) : Alg F

The matrix unit of a morphism f : F x → F y.

theorem MultiplicativeBasisDeformations.CatAlg.unitM_apply {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x y : ι) (f : F x ⟶ F y) (p q : ι) : unitM x y f p q = CategoryTheory.CategoryStruct.comp (idTo p x) (CategoryTheory.CategoryStruct.comp f (idTo y q))

theorem MultiplicativeBasisDeformations.CatAlg.unitM_self {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x y : ι) (f : F x ⟶ F y) : unitM x y f x y = f

theorem MultiplicativeBasisDeformations.CatAlg.unitM_add {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x y : ι) (f f' : F x ⟶ F y) : unitM x y (f + f') = unitM x y f + unitM x y f'

theorem MultiplicativeBasisDeformations.CatAlg.unitM_smul {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x y : ι) (c : k) (f : F x ⟶ F y) : unitM x y (c • f) = c • unitM x y f

theorem MultiplicativeBasisDeformations.CatAlg.unitM_zero {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x y : ι) : unitM x y 0 = 0

theorem MultiplicativeBasisDeformations.CatAlg.unitM_mul {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (x y z : ι) (f : F x ⟶ F y) (f' : F y ⟶ F z) : unitM x y f * unitM y z f' = unitM x z (CategoryTheory.CategoryStruct.comp f f')

theorem MultiplicativeBasisDeformations.CatAlg.unitM_mul_ne {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {x y y' z : ι} (h : y ≠ y') (f : F x ⟶ F y) (f' : F y' ⟶ F z) : unitM x y f * unitM y' z f' = 0

theorem MultiplicativeBasisDeformations.CatAlg.eq_sum_unitM {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} (a : Alg F) : a = ∑ x : ι, ∑ y : ι, unitM x y (a x y)

The basis

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CatAlg.Idx {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) : Type

The nonzero homogeneous pieces.

def MultiplicativeBasisDeformations.CatAlg.vecA0 {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} (b : (x y : ι) → G → (F x ⟶ F y)) (t : Idx D) : (Alg F)ᵐᵒᵖ

The basis vector of a nonzero piece.

theorem MultiplicativeBasisDeformations.CatAlg.proj_vecA0 {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (t t₀ : Idx D) : (D.proj (↑t₀).2.2 (↑t₀).1 (↑t₀).2.1) (MulOpposite.unop (vecA0 b t) (↑t₀).1 (↑t₀).2.1) = if t = t₀ then b (↑t₀).1 (↑t₀).2.1 (↑t₀).2.2 else 0

The coordinate functional of a piece kills the other basis vectors.

theorem MultiplicativeBasisDeformations.CatAlg.linearIndependent_vecA0 {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (hne : ∀ (x y : ι) (g : G), D.part g x y ≠ ⊥ → b x y g ≠ 0) : LinearIndependent k (vecA0 b)

theorem MultiplicativeBasisDeformations.CatAlg.span_vecA0 {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hspan : ∀ (x y : ι) (g : G), ∀ f ∈ D.part g x y, ∃ (c : k), f = c • b x y g) : ⊤ ≤ Submodule.span k (Set.range (vecA0 b))

noncomputable def MultiplicativeBasisDeformations.CatAlg.basisA0 {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (hspan : ∀ (x y : ι) (g : G), ∀ f ∈ D.part g x y, ∃ (c : k), f = c • b x y g) (hne : ∀ (x y : ι) (g : G), D.part g x y ≠ ⊥ → b x y g ≠ 0) : Module.Basis (Idx D) k (Alg F)ᵐᵒᵖ

The basis of A₀ given by the chosen homogeneous vectors.

theorem MultiplicativeBasisDeformations.CatAlg.basisA0_apply {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (hspan : ∀ (x y : ι) (g : G), ∀ f ∈ D.part g x y, ∃ (c : k), f = c • b x y g) (hne : ∀ (x y : ι) (g : G), D.part g x y ≠ ⊥ → b x y g ≠ 0) (t : Idx D) : (basisA0 b hmem hspan hne) t = vecA0 b t

theorem MultiplicativeBasisDeformations.CatAlg.basisA0_isMultiplicative {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (hspan : ∀ (x y : ι) (g : G), ∀ f ∈ D.part g x y, ∃ (c : k), f = c • b x y g) (hne : ∀ (x y : ι) (g : G), D.part g x y ≠ ⊥ → b x y g ≠ 0) (hmul : ∀ (x y z : ι) (g h : G), CategoryTheory.CategoryStruct.comp (b x y g) (b y z h) = 0 ∨ CategoryTheory.CategoryStruct.comp (b x y g) (b y z h) = b x z (g * h)) : IsMultiplicativeBasis (basisA0 b hmem hspan hne)

The basis of A₀ is multiplicative.

theorem MultiplicativeBasisDeformations.CatAlg.part_one_ne_bot {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (hid : ∀ (x : ι), b x x 1 = CategoryTheory.CategoryStruct.id (F x)) (hid0 : ∀ (x : ι), CategoryTheory.CategoryStruct.id (F x) ≠ 0) (x : ι) : D.part 1 x x ≠ ⊥

def MultiplicativeBasisDeformations.CatAlg.idIdx {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (hid : ∀ (x : ι), b x x 1 = CategoryTheory.CategoryStruct.id (F x)) (hid0 : ∀ (x : ι), CategoryTheory.CategoryStruct.id (F x) ≠ 0) (x : ι) : Idx D

The identity piece of a label.

theorem MultiplicativeBasisDeformations.CatAlg.basisA0_idIdx {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (hspan : ∀ (x y : ι) (g : G), ∀ f ∈ D.part g x y, ∃ (c : k), f = c • b x y g) (hne : ∀ (x y : ι) (g : G), D.part g x y ≠ ⊥ → b x y g ≠ 0) (hid : ∀ (x : ι), b x x 1 = CategoryTheory.CategoryStruct.id (F x)) (hid0 : ∀ (x : ι), CategoryTheory.CategoryStruct.id (F x) ≠ 0) (x : ι) : (basisA0 b hmem hspan hne) (idIdx b hmem hid hid0 x) = MulOpposite.op (unitM x x (CategoryTheory.CategoryStruct.id (F x)))

theorem MultiplicativeBasisDeformations.CatAlg.sum_unitM_id {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} : ∑ x : ι, unitM x x (CategoryTheory.CategoryStruct.id (F x)) = 1

theorem MultiplicativeBasisDeformations.CatAlg.idIdx_complete {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (hspan : ∀ (x y : ι) (g : G), ∀ f ∈ D.part g x y, ∃ (c : k), f = c • b x y g) (hne : ∀ (x y : ι) (g : G), D.part g x y ≠ ⊥ → b x y g ≠ 0) (hid : ∀ (x : ι), b x x 1 = CategoryTheory.CategoryStruct.id (F x)) (hid0 : ∀ (x : ι), CategoryTheory.CategoryStruct.id (F x) ≠ 0) : CompleteOrthogonalIdempotents fun (x : ι) => (basisA0 b hmem hspan hne) (idIdx b hmem hid hid0 x)

The labels give a complete set of orthogonal idempotents.

theorem MultiplicativeBasisDeformations.CatAlg.eq_unitM_of_corner {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {x : ι} {a : Alg F} (h1 : a * unitM x x (CategoryTheory.CategoryStruct.id (F x)) = a) (h2 : unitM x x (CategoryTheory.CategoryStruct.id (F x)) * a = a) : a = unitM x x (a x x)

theorem MultiplicativeBasisDeformations.CatAlg.idIdx_primitive {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] {D : HomGrading F G} [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (b : (x y : ι) → G → (F x ⟶ F y)) (hmem : ∀ (x y : ι) (g : G), b x y g ∈ D.part g x y) (hspan : ∀ (x y : ι) (g : G), ∀ f ∈ D.part g x y, ∃ (c : k), f = c • b x y g) (hne : ∀ (x y : ι) (g : G), D.part g x y ≠ ⊥ → b x y g ≠ 0) (hid : ∀ (x : ι), b x x 1 = CategoryTheory.CategoryStruct.id (F x)) (hid0 : ∀ (x : ι), CategoryTheory.CategoryStruct.id (F x) ≠ 0) (hloc : ∀ (x : ι) (φ : F x ⟶ F x), CategoryTheory.CategoryStruct.comp φ φ = φ → φ = 0 ∨ φ = CategoryTheory.CategoryStruct.id (F x)) (x : ι) : IsPrimitiveIdempotent ((basisA0 b hmem hspan hne) (idIdx b hmem hid hid0 x))

The label idempotents are primitive when the endomorphism rings have no nontrivial idempotents.