A₀ has a normed multiplicative basis

Proposition 4.14 (scalar-normalization.tex): "The endpoint chains and Corollary 3.3 show that the intersection of the resulting basis with each radical power is a basis of that power."

The path-length grading of the scalar mesh category grades A₀ = (Alg F₀)ᵒᵖ (lenA0); the basis of Proposition 4.14 consists of homogeneous elements of corners, so by the layer argument (GradedLayers.lean) it is adapted to every radical power, and A₀ has a normed multiplicative basis (hasNormedBasis_A0).

theorem MultiplicativeBasisDeformations.algebraRadicalPow_mul_left {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {n : ℕ} (hn : 1 ≤ n) (a : A) {z : A} (hz : z ∈ algebraRadicalPow k A n) : a * z ∈ algebraRadicalPow k A n

theorem MultiplicativeBasisDeformations.algebraRadicalPow_mul_right {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {n : ℕ} (hn : 1 ≤ n) (a : A) {z : A} (hz : z ∈ algebraRadicalPow k A n) : z * a ∈ algebraRadicalPow k A n

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.degProj_of_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {d e : ℕ} {x y : V} {g : obj c x ⟶ obj c y} (hg : g ∈ degreePart c e x y) : (degProj c d x y) g = if e = d then g else 0

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.degProj_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (d : ℕ) {x y : V} (f : obj c x ⟶ obj c y) : (degProj c d x y) f ∈ degreePart c d x y

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.comp_mem_degreePart' {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {d e : ℕ} {x y z : V} {f : obj c x ⟶ obj c y} {g : obj c y ⟶ obj c z} (hf : f ∈ degreePart c d x y) (hg : g ∈ degreePart c e y z) : CategoryTheory.CategoryStruct.comp f g ∈ degreePart c (d + e) x z

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.eq_sum_degProj {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {N : ℕ} (hN : ∀ (d : ℕ) (x y : V), N ≤ d → degreePart c d x y = ⊥) {x y : V} (f : obj c x ⟶ obj c y) : f = ∑ d ∈ Finset.range N, (degProj c d x y) f

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.degreePart_zero_eq {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x : V} {f : obj c x ⟶ obj c x} (hf : f ∈ degreePart c 0 x x) : ∃ (t : k), f = t • CategoryTheory.CategoryStruct.id (obj c x)

theorem MultiplicativeBasisDeformations.ScalarMeshCategory.exists_degreePart_eq_bot {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) [Finite V] (hfin : ∀ (x y : V), FiniteDimensional k (obj c x ⟶ obj c y)) : ∃ (N : ℕ), ∀ (d : ℕ) (x y : V), N ≤ d → degreePart c d x y = ⊥

noncomputable def MultiplicativeBasisDeformations.MeshWalk.projA0 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (d : ℕ) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

The degree-d part of an element of A₀.

theorem MultiplicativeBasisDeformations.MeshWalk.projA0_apply {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (d : ℕ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (p q : D.PV) : MulOpposite.unop ((projA0 D d) a) p q = (ScalarMeshCategory.degProj c d ↑p ↑q) (MulOpposite.unop a p q)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.lenA0 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) : LenGrading k (CatAlg.Alg D.F0)ᵐᵒᵖ

The length grading of A₀.

theorem MultiplicativeBasisDeformations.MeshWalk.idTo_mem_degreePart {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (p x : D.PV) : CatAlg.idTo p x ∈ ScalarMeshCategory.degreePart c 0 ↑p ↑x

theorem MultiplicativeBasisDeformations.MeshWalk.unitM_isHom {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {d : ℕ} {x y : D.PV} {f : D.F0 x ⟶ D.F0 y} (hf : f ∈ ScalarMeshCategory.degreePart c d ↑x ↑y) : (lenA0 D hfin).IsHom d (MulOpposite.op (CatAlg.unitM x y f))

theorem MultiplicativeBasisDeformations.MeshWalk.deck_part_le {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} (v₀ : V) (g : Deck Q v₀) (x y : V) : (deckGrading Q c v₀).part g x y ≤ ScalarMeshCategory.degreePart c (hgt Q v₀ g).toNat x y

The normed basis

theorem MultiplicativeBasisDeformations.MeshWalk.op_unitM_corner_mul {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x y : D.PV) (f : D.F0 x ⟶ D.F0 y) : MulOpposite.op (CatAlg.unitM y y (CategoryTheory.CategoryStruct.id (D.F0 y))) * MulOpposite.op (CatAlg.unitM x y f) * MulOpposite.op (CatAlg.unitM x x (CategoryTheory.CategoryStruct.id (D.F0 x))) = MulOpposite.op (CatAlg.unitM x y f)

theorem MultiplicativeBasisDeformations.MeshWalk.hasNormedBasis_A0 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) : HasNormedMultiplicativeBasis k (CatAlg.Alg D.F0)ᵐᵒᵖ

A₀ has a normed multiplicative basis (Proposition 4.14 with Corollary 3.3).