Linear realizations of mesh categories

An assignment of objects and reversed arrow representatives determines a linear functor from the free path category. If the displayed mesh relations evaluate to zero, that functor descends to the mesh quotient. This file also isolates the exact kernel statement which makes the descended realization faithful.

structure MagnitudeConjecture.MeshCategory.Realization {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (T : RightMeshData Q) (F₀ : Q → C) : Type (max (max u_1 v) w)

A realization of the arrows of a right translation quiver in a linear category for which every ordinary mesh relation evaluates to zero.

• arrowMap {i j : Q} : (i ⟶ j) → (F₀ j ⟶ F₀ i)
• map_meshRelation (x : { x : Q // x ∉ T.projective }) : (LinearPathCategory.lift F₀ fun {i j : Q} => self.arrowMap).map (T.meshRelation x) = 0

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.MeshCategory.Realization.freeFunctor {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) : CategoryTheory.Functor (LinearPathCategory.Category k Q) C

The free linear path realization determined by the arrow assignment.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.MeshCategory.Realization.meshIdeal {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (_R : Realization T F₀) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal (LinearPathCategory.Category k Q)

The Hom ideal generated by the ordinary mesh relations.

theorem MagnitudeConjecture.MeshCategory.Realization.meshIdeal_isKilledBy {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) : R.meshIdeal.IsKilledBy R.freeFunctor

Vanishing of the mesh generators implies vanishing of their whole two-sided linear Hom ideal.

noncomputable def MagnitudeConjecture.MeshCategory.Realization.functor {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) : CategoryTheory.Functor (RawCategory T) C

The induced realization of the ordinary mesh quotient.

instance MagnitudeConjecture.MeshCategory.Realization.functor_additive {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) : R.functor.Additive

instance MagnitudeConjecture.MeshCategory.Realization.functor_linear {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) : CategoryTheory.Functor.Linear k R.functor

instance MagnitudeConjecture.MeshCategory.Realization.functor_full {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) [R.freeFunctor.Full] : R.functor.Full

@[simp]

theorem MagnitudeConjecture.MeshCategory.Realization.functor_map_quotient_map {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) {X Y : LinearPathCategory.Category k Q} (f : X ⟶ Y) : R.functor.map ((quotientFunctor T).map f) = R.freeFunctor.map f

def MagnitudeConjecture.MeshCategory.Realization.KernelGeneratedByMesh {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) : Prop

The residual standardness statement upstairs: every relation killed by the free-path realization lies in the ideal generated by the meshes.

theorem MagnitudeConjecture.MeshCategory.Realization.functor_faithful {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) (hker : R.KernelGeneratedByMesh) : R.functor.Faithful

Kernel generation by meshes makes the quotient realization faithful.

noncomputable def MagnitudeConjecture.MeshCategory.Realization.homLinearEquivOfInjective {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) [R.functor.Full] (x y : Q) (hinjective : Function.Injective fun (f : obj T x ⟶ obj T y) => R.functor.map f) : (obj T x ⟶ obj T y) ≃ₗ[k] F₀ x ⟶ F₀ y

A full mesh realization which is injective on one displayed Hom space gives a linear equivalence on that Hom space.

noncomputable def MagnitudeConjecture.MeshCategory.Realization.homLinearEquiv {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) [R.functor.Full] [R.functor.Faithful] (x y : Q) : (obj T x ⟶ obj T y) ≃ₗ[k] F₀ x ⟶ F₀ y

A full and faithful mesh realization gives a linear equivalence on each Hom space.

@[simp]

theorem MagnitudeConjecture.MeshCategory.Realization.homLinearEquivOfInjective_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) [R.functor.Full] (x y : Q) (hinjective : Function.Injective fun (f : obj T x ⟶ obj T y) => R.functor.map f) (f : obj T x ⟶ obj T y) : (R.homLinearEquivOfInjective x y hinjective) f = R.functor.map f

@[simp]

theorem MagnitudeConjecture.MeshCategory.Realization.homLinearEquiv_apply {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] {C : Type z} [CategoryTheory.Category.{u_1, z} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {T : RightMeshData Q} {F₀ : Q → C} (R : Realization T F₀) [R.functor.Full] [R.functor.Faithful] (x y : Q) (f : obj T x ⟶ obj T y) : (R.homLinearEquiv x y) f = R.functor.map f