Projective-injective coordinates over the standard mesh

Every indecomposable projective-injective finite contravariant module over the standard mesh is the dual corepresentable based at a projective mesh vertex. Finite Krull--Schmidt decomposition then gives literal finite coordinates for every projective-injective object.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : Fintype (x ⟶ y)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposable_projectiveInjective_iso_standardFormProjectiveDual {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (N : S.StandardFormFiniteContravariantModuleCategory) [CategoryTheory.Projective N] [CategoryTheory.Injective N] (hN : CategoryTheory.Indecomposable N) : ∃ (p : S.StandardFormProjectiveVertex), Nonempty (CoveringHom.finiteDimensionalDualLinearYoneda (S.standardFormOppositeVertex ↑p) ⋯ ≅ N)

An indecomposable projective-injective standard-mesh module is the dual corepresentable based at a projective mesh vertex.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardFormProjectiveInjectiveCoordinates {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (M : S.StandardFormFiniteContravariantModuleCategory) : Type u

Literal finite coordinates on a projective-injective standard-mesh module by dual corepresentables based at projective vertices.

• n : ℕ
• p : Fin self.n → S.StandardFormProjectiveVertex
• isoSource : (⨁ fun (i : Fin self.n) => CoveringHom.finiteDimensionalDualLinearYoneda (S.standardFormOppositeVertex ↑(self.p i)) ⋯) ≅ M

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveCoordinates_nonempty {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (M : S.StandardFormFiniteContravariantModuleCategory) [CategoryTheory.Projective M] [CategoryTheory.Injective M] : Nonempty (S.StandardFormProjectiveInjectiveCoordinates M)

Every projective-injective finite standard-mesh module has finite projective-vertex dual-corepresentable coordinates.