Magnitude conjecture

MagnitudeConjecture.CategoryTheory.MeshRiedtmannDuality

Perfect pairings from Riedtmann condition (c) #

This file packages the objectwise perfect composition pairing supplied by Riedtmann condition (c). The contravariant finite-module orientation used by the recovery proof is built separately in MeshRiedtmannContravariantDuality.

source
noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.riedtmannProjectiveDualityLinearEquiv {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {p : Q} (D : T.RiedtmannProjectiveDualityData p) (x : Q) :
(obj T p ⟶ obj T x) ≃ₗ[k] Module.Dual k (obj T x ⟶ obj T D.dualVertex)

The objectwise perfect composition pairing supplied by Riedtmann condition (c).

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.MeshCategory.RightMeshData.riedtmannProjectiveDualityLinearEquiv_apply_apply {k : Type u} [Field k] {Q : Type} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {p : Q} (D : T.RiedtmannProjectiveDualityData p) (x : Q) (f : obj T p ⟶ obj T x) (g : obj T x ⟶ obj T D.dualVertex) :
    ((T.riedtmannProjectiveDualityLinearEquiv D x) f) g = D.epsilon (CategoryTheory.CategoryStruct.comp f g)