Proposition 4.14 for a scalar mesh category

prop:scalar-normalization (scalar-normalization.tex), for the deck grading of a scalar mesh category with at most one arrow between vertices and mesh data (in the application, k(Γ_A) with arMeshData). The cover L of the projective labels is thin with a multiplicative basis (Lemmas 4.8–4.12), the deck group is free (Lemma 4.2) and countable, and weights on L are ratios of object values (Lemma 4.13). The descent (Descent.lean) gives one vector on each nonzero deck-homogeneous piece of A₀, closed under composition up to zero (exists_deckVectors); these form a multiplicative basis of A₀ = (Alg F₀)ᵒᵖ containing the primitive idempotents of the labels (exists_multBasis_A0).

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.D0 {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) {L : CatAlg.LocalFamily (meshFam Q c)} (D : CatAlg.MeshData (meshFam Q c) L) : CatAlg.HomGrading D.F0 (Deck Q v₀)

The grading of A₀ by the deck group.

instance MultiplicativeBasisDeformations.MeshWalk.instFiniteDimensionalHomScalarMeshCategoryF0 {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} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (x y : D.PV) : FiniteDimensional k (D.F0 x ⟶ D.F0 y)

theorem MultiplicativeBasisDeformations.MeshWalk.ratio_hyp {k : Type u} [Field k] [IsAlgClosed k] [Infinite 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} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) (d : CatAlg.CovObj (D0 Q c v₀ D) → CatAlg.CovObj (D0 Q c v₀ D) → k) (hd : Thin.IsWeight Set.univ d) : ∃ (ζ : CatAlg.CovObj (D0 Q c v₀ D) → k), (∀ (o : CatAlg.CovObj (D0 Q c v₀ D)), ζ o ≠ 0) ∧ ∀ (o o' : CatAlg.CovObj (D0 Q c v₀ D)) (f : o ⟶ o'), f ≠ 0 → d o o' = ζ o' / ζ o

Lemma 4.13 in the form used by the descent.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_deckVectors {k : Type u} [Field k] [IsAlgClosed k] [Infinite 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} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) : ∃ (b : (x y : D.PV) → Deck Q v₀ → (D.F0 x ⟶ D.F0 y)), (∀ (x y : D.PV) (g : Deck Q v₀), b x y g ∈ (D0 Q c v₀ D).part g x y) ∧ (∀ (x y : D.PV) (g : Deck Q v₀), ∀ f ∈ (D0 Q c v₀ D).part g x y, ∃ (c_1 : k), f = c_1 • b x y g) ∧ (∀ (x y : D.PV) (g : Deck Q v₀), (D0 Q c v₀ D).part g x y ≠ ⊥ → b x y g ≠ 0) ∧ (∀ (x : D.PV), b x x 1 = CategoryTheory.CategoryStruct.id (D.F0 x)) ∧ ∀ (x y z : D.PV) (g h : Deck Q v₀), 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)

Proposition 4.14, descent: one vector on each nonzero deck-homogeneous piece of A₀, with identities, closed under composition up to zero.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_multBasis_A0 {k : Type u} [Field k] [IsAlgClosed k] [Infinite 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} [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) : ∃ (b : (x y : D.PV) → Deck Q v₀ → (D.F0 x ⟶ D.F0 y)) (hmem : ∀ (x y : D.PV) (g : Deck Q v₀), b x y g ∈ (D0 Q c v₀ D).part g x y) (hspan : ∀ (x y : D.PV) (g : Deck Q v₀), ∀ f ∈ (D0 Q c v₀ D).part g x y, ∃ (c_1 : k), f = c_1 • b x y g) (hne : ∀ (x y : D.PV) (g : Deck Q v₀), (D0 Q c v₀ D).part g x y ≠ ⊥ → b x y g ≠ 0) (hid : ∀ (x : D.PV), b x x 1 = CategoryTheory.CategoryStruct.id (D.F0 x)), IsMultiplicativeBasis (CatAlg.basisA0 b hmem hspan hne) ∧ ∀ (hid0 : ∀ (x : D.PV), CategoryTheory.CategoryStruct.id (D.F0 x) ≠ 0), (CompleteOrthogonalIdempotents fun (x : D.PV) => (CatAlg.basisA0 b hmem hspan hne) (CatAlg.idIdx b hmem hid hid0 x)) ∧ ∀ (x : D.PV), IsPrimitiveIdempotent ((CatAlg.basisA0 b hmem hspan hne) (CatAlg.idIdx b hmem hid hid0 x))

Proposition 4.14: A₀ has a multiplicative basis of deck-homogeneous matrix units containing the primitive idempotents of the labels.