Decomposition by the final categorical arrow

Every morphism in a mesh category is a scalar diagonal term plus a finite sum of morphisms followed by one arrow into its target. This is the path-algebra decomposition used in Ringel's induction for fullness and faithfulness.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.IncomingArrow {Q : Type v} [Quiver Q] (z : Q) : Type (max v w)

The finite family of reversed quiver arrows whose represented categorical maps end at z.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingArrowHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) {z : Q} (a : IncomingArrow z) : obj T a.fst ⟶ obj T z

The mesh-category morphism represented by one arrow into z.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.IncomingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) (x z : Q) : Type (max (max w v) (max u v) w)

One coefficient morphism for each arrow into the target.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.incomingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) {x z : Q} (c : T.IncomingCoefficient x z) : obj T x ⟶ obj T z

Compose a family of coefficients with all arrows into the target.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.singleIncomingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) {x z : Q} (a₀ : IncomingArrow z) (f : obj T x ⟶ obj T a₀.fst) : T.IncomingCoefficient x z

A coefficient family supported at one incoming arrow.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.incomingSum_single {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) {x z : Q} (a₀ : IncomingArrow z) (f : obj T x ⟶ obj T a₀.fst) : T.incomingSum (T.singleIncomingCoefficient a₀ f) = CategoryTheory.CategoryStruct.comp f (T.incomingArrowHom a₀)

Summing a coefficient family supported at one arrow recovers the one displayed composite.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.diagonalScalar {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) (x z : Q) (c : k) : obj T x ⟶ obj T z

The scalar identity term when the source and target labels coincide, and zero otherwise.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.diagonalScalar_self {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) (x : Q) (c : k) : T.diagonalScalar x x c = c • CategoryTheory.CategoryStruct.id (obj T x)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.exists_eq_diagonalScalar_add_incomingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) {x z : Q} (f : obj T x ⟶ obj T z) : ∃ (c : k) (h : T.IncomingCoefficient x z), f = T.diagonalScalar x z c + T.incomingSum h

Every mesh-category morphism is a scalar diagonal term plus a sum of morphisms followed by one incoming arrow.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.RawIncomingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) (X : RawCategory T) (z : Q) : Type (max (max w v) (max u v) w)

One coefficient morphism for each arrow into a target, with an arbitrary raw mesh-category object as source.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.rawIncomingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) {X : RawCategory T} {z : Q} (c : T.RawIncomingCoefficient X z) : X ⟶ obj T z

Compose raw-source coefficients with all arrows into the target.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.rawDiagonalScalar {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) (X : RawCategory T) (z : Q) (c : k) : X ⟶ obj T z

The scalar identity term for an arbitrary raw source object, and zero unless that source is the displayed target vertex.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.exists_eq_rawDiagonalScalar_add_rawIncomingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) {X : RawCategory T} {z : Q} (f : X ⟶ obj T z) : ∃ (c : k) (h : T.RawIncomingCoefficient X z), f = T.rawDiagonalScalar X z c + T.rawIncomingSum h

Decomposition by the final arrow for an arbitrary raw source object. This wrapper internalizes the harmless object transport between a quotient object and the vertex represented by its underlying path-category object.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.OutgoingArrow {Q : Type v} [Quiver Q] (x : Q) : Type (max v w)

The finite family of reversed quiver arrows whose represented categorical maps start at x.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.outgoingArrowHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) {x : Q} (a : OutgoingArrow x) : obj T x ⟶ obj T a.fst

The mesh-category morphism represented by one arrow out of x.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.outgoingArrowHom_cast_source {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) [(x : Q) → Fintype (OutgoingArrow x)] {x x' : Q} (h : x = x') (a : OutgoingArrow x) : T.outgoingArrowHom ⟨a.fst, Quiver.Hom.cast ⋯ h a.snd⟩ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (T.outgoingArrowHom a)

Transporting the source of an outgoing arrow is realized by the corresponding object equality before the original mesh morphism.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.OutgoingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) (x z : Q) : Type (max (max w v) (max u v) w)

One coefficient morphism after each arrow out of the source.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.outgoingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) [(x : Q) → Fintype (OutgoingArrow x)] {x z : Q} (c : T.OutgoingCoefficient x z) : obj T x ⟶ obj T z

Compose all arrows out of a source with their coefficient family.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.singleOutgoingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) {x z : Q} (a₀ : OutgoingArrow x) (f : obj T a₀.fst ⟶ obj T z) : T.OutgoingCoefficient x z

A coefficient family supported after one outgoing arrow.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.outgoingSum_single {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) [(x : Q) → Fintype (OutgoingArrow x)] {x z : Q} (a₀ : OutgoingArrow x) (f : obj T a₀.fst ⟶ obj T z) : T.outgoingSum (T.singleOutgoingCoefficient a₀ f) = CategoryTheory.CategoryStruct.comp (T.outgoingArrowHom a₀) f

Summing a coefficient family supported after one arrow recovers the one displayed composite.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.exists_eq_diagonalScalar_add_outgoingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) [(x : Q) → Fintype (OutgoingArrow x)] {x z : Q} (f : obj T x ⟶ obj T z) : ∃ (c : k) (h : T.OutgoingCoefficient x z), f = T.diagonalScalar x z c + T.outgoingSum h

Every mesh-category morphism is a scalar diagonal term plus a sum of one outgoing arrow followed by a coefficient morphism.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.RawOutgoingCoefficient {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) (x : Q) (Z : RawCategory T) : Type (max (max w v) (max u v) w)

One coefficient morphism after each arrow out of the source, with an arbitrary raw mesh-category object as target.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.rawOutgoingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) [(x : Q) → Fintype (OutgoingArrow x)] {x : Q} {Z : RawCategory T} (c : T.RawOutgoingCoefficient x Z) : obj T x ⟶ Z

Compose all arrows out of a source with raw-target coefficients.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.targetRawDiagonalScalar {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) (x : Q) (Z : RawCategory T) (c : k) : obj T x ⟶ Z

The scalar identity term for an arbitrary raw target object, and zero unless that target is the displayed source vertex.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.exists_eq_targetRawDiagonalScalar_add_rawOutgoingSum {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(z : Q) → Fintype ((y : Q) × (z ⟶ y))] (T : RightMeshData Q) [(x : Q) → Fintype (OutgoingArrow x)] {x : Q} {Z : RawCategory T} (f : obj T x ⟶ Z) : ∃ (c : k) (h : T.RawOutgoingCoefficient x Z), f = T.targetRawDiagonalScalar x Z c + T.rawOutgoingSum h

Decomposition by the first arrow for an arbitrary raw target object. This is the target-side counterpart of exists_eq_rawDiagonalScalar_add_rawIncomingSum.