The deck grading of a scalar mesh category, as a graded family

Subsection 4.2 (scalar-normalization.tex): the covering formula eq:walk-hom-sum and the height. For a translation quiver with homogeneous meshes, the walk-class weight deg of DeckGrading.lean grades the Hom spaces of C(Q, c) between all vertices (deckGrading), and the length of walk classes is a height in the sense of HeightData (deckHeight): nonzero morphisms of degree g are combinations of paths of length ℓ(g), and in length zero only identities occur.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.meshFam {k : Type u} [Field k] {V : Type} [Quiver V] (Q : TranslationQuiver V) [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) : V → ScalarMeshCategory k Q c

The mesh category objects as a family.

theorem MultiplicativeBasisDeformations.MeshWalk.pathMor_nil {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) (x : V) : ScalarMeshCategory.pathMor c Quiver.Path.nil = CategoryTheory.CategoryStruct.id (ScalarMeshCategory.obj c x)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.deckGrading {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) : CatAlg.HomGrading (meshFam Q c) (Deck Q v₀)

The deck grading of the Hom spaces between all vertices.

theorem MultiplicativeBasisDeformations.MeshWalk.isHom_iff {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} {f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y} : (deckGrading Q c v₀).IsHom g f ↔ f ∈ ScalarMeshCategory.wPart c (degW Q v₀) g x y

theorem MultiplicativeBasisDeformations.MeshWalk.wPart_le_span {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) : ScalarMeshCategory.wPart c (degW Q v₀) g x y ≤ Submodule.span k {f : ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y | ∃ (p : Quiver.Path x y), (degW Q v₀).deg p = g ∧ ScalarMeshCategory.pathMor c p = f}

Paths of a given weight: if none has a property, the weight part lies in the span of those that do.

def MultiplicativeBasisDeformations.MeshWalk.deckHeight {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) : CatAlg.HeightData (deckGrading Q c v₀)

The height of the deck grading.