Contravariant module duality from Riedtmann condition (c)

Coefficient-dualizing condition (c) identifies the injective D Hom(p,-) in the contravariant mesh-module category with the contravariant representable Hom(-,j). This is the orientation used in the Bongartz--Gabriel injective-resolution argument.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.oppositeVertex {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (X : T.VertexCategoryᵒᵖ) : Q

Recover the underlying mesh vertex from an object of the opposite strict vertex category.

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

The coefficient-dual form of the perfect pairing in condition (c).

theorem MagnitudeConjecture.MeshCategory.RightMeshData.riedtmannProjectiveCoefficientDualityLinearEquiv_evaluation {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hfinite : ∀ (x y : Q), FiniteDimensional k (obj T x ⟶ obj T y)) {p : Q} (D : T.RiedtmannProjectiveDualityData p) (x : Q) (phi : Module.Dual k (obj T p ⟶ obj T x)) (ell : Module.Dual k (obj T x ⟶ obj T D.dualVertex)) : ell ((T.riedtmannProjectiveCoefficientDualityLinearEquiv hfinite D x) phi) = phi ((T.riedtmannProjectiveDualityLinearEquiv D x).symm ell)

Evaluation characterizes the coefficient-dual form of condition (c).

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.riedtmannProjectiveContravariantLinearEquiv {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hfinite : ∀ (x y : Q), FiniteDimensional k (obj T x ⟶ obj T y)) {p : Q} (D : T.RiedtmannProjectiveDualityData p) (X : T.VertexCategoryᵒᵖ) : Module.Dual k (X ⟶ Opposite.op p) ≃ₗ[k] Opposite.unop X ⟶ D.dualVertex

The objectwise coefficient-dual condition-(c) equivalence in the strict vertex model and the opposite-category convention for contravariant modules.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.riedtmannProjectiveContravariantLinearEquiv_evaluation {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hfinite : ∀ (x y : Q), FiniteDimensional k (obj T x ⟶ obj T y)) {p : Q} (D : T.RiedtmannProjectiveDualityData p) (X : T.VertexCategoryᵒᵖ) (phi : Module.Dual k (X ⟶ Opposite.op p)) (ell : Module.Dual k (obj T (T.oppositeVertex X) ⟶ obj T D.dualVertex)) : ell ((T.riedtmannProjectiveContravariantLinearEquiv hfinite D X) phi).hom = phi (CategoryTheory.InducedCategory.homMk ((T.riedtmannProjectiveDualityLinearEquiv D (T.oppositeVertex X)).symm ell)).op

Evaluation formula for the strict-vertex coefficient-dual condition-(c) equivalence.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.riedtmannProjectiveContravariantLinearModuleIso {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hfinite : ∀ (x y : Q), FiniteDimensional k (obj T x ⟶ obj T y)) {p : Q} (D : T.RiedtmannProjectiveDualityData p) : CoveringHom.dualLinearYonedaLinearModule (Opposite.op p) ≅ T.contravariantRepresentableLinearModule D.dualVertex

Coefficient-dualizing condition (c) identifies the injective D Hom(p,-) with the contravariant representable Hom(-,j).

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.riedtmannProjectiveContravariantFiniteModuleIso {k : Type u} [Field k] {Q : Type} [Quiver Q] [Fintype Q] [(x y : Q) → Fintype (x ⟶ y)] (T : RightMeshData Q) (hfinite : ∀ (x y : Q), FiniteDimensional k (obj T x ⟶ obj T y)) (hP : T.FiniteContravariantRepresentables) {p : Q} (D : T.RiedtmannProjectiveDualityData p) (hI : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.dualLinearYonedaLinearModule (Opposite.op p))) : CoveringHom.finiteDimensionalDualLinearYoneda (Opposite.op p) hI ≅ T.contravariantRepresentableFiniteModule hP D.dualVertex

Finite-module form of the coefficient-dual condition-(c) isomorphism.