The mesh derivative and the brick hypothesis

Section 5 of the manuscript (mesh-deformations.tex).

• The derivative D_m (eq:mesh-derivative): for a family f = (f_a)_a of morphisms parallel to the arrows, (D_m f)_x = ∑_{a : y → x} c_{x,a} (f_{σ a} a + (σ a) f_a). It is recorded here as a function on all parallel families; the manuscript restricts it to families of path degree m, with values of degree m + 1.
• The object quotient C/[Σ] by the ideal generated by the identities of a set Σ of objects, and the brick hypothesis (Subsection 5.2): every object quotient that is not zero has an object whose endomorphism ring is k.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.arrowMor {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) {x y : V} (a : x ⟶ y) : obj c x ⟶ obj c y

The image of an arrow in the scalar mesh category.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.ArrowFamily {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) : Type (max (max (max w v) v) (max u v) w)

A family of morphisms parallel to the arrows of Q.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.MeshFamily {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) : Type (max v (max u v) w)

A family of morphisms τ x ⟶ x at the nonprojective vertices.

noncomputable def MultiplicativeBasisDeformations.ScalarMeshCategory.meshDerivative {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (f : ArrowFamily c) : MeshFamily c

The mesh derivative (D f)_x = ∑_{a : y → x} c_{x,a} (f_{σ a} a + (σ a) f_a) (eq:mesh-derivative).

def MultiplicativeBasisDeformations.ScalarMeshCategory.MeshDerivativeSurjective {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (m : ℕ) : Prop

The derivative D_m is surjective in degree m: every family of degree-(m+1) mesh errors is D f for a family f of degree m.

def MultiplicativeBasisDeformations.ScalarMeshCategory.identityRelations {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (D : Set V) (X Y : ScalarMeshCategory k Q c) : Set (X ⟶ Y)

The relations killing the identities of the objects in a set D (the manuscript's Σ).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.ObjectQuotient {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (D : Set V) : Type v

The object quotient C/[D]: the quotient by the ideal of morphisms that factor through finite sums of objects of D.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.ScalarMeshCategory.ObjectQuotient.obj {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (D : Set V) (x : V) : ObjectQuotient c D

The image of a vertex in an object quotient.

def MultiplicativeBasisDeformations.ScalarMeshCategory.BrickHypothesis {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) : Prop

The brick hypothesis: every object quotient with a nonzero object has an object whose endomorphism ring is k.