Restricted Yoneda as a boundary diagram

The manuscript treats modules over the category of tau-projective boundary objects as contravariant diagrams on the augmented incidence poset. This file makes that identification literal for the restricted Yoneda objects of the primitive factor.

At a boundary point q, the diagram has value Hom(P_q,X). Along q ≤ r, its structure map is precomposition with the normalized incidence morphism P_q ⟶ P_r. The resulting diagram is naturally isomorphic to the boundary diagram of the concrete represented poset space. In particular, its maps into the root are injective and it has no nonzero subdiagram supported away from the root.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceRestrictedYonedaDiagram {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (X : S.FactorCategory K) : CategoryTheory.Functor (PosetSpace.BoundaryIndex T)ᵒᵖ (ModuleCat k)

The boundary-category form of restricted Yoneda at a factor object.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceRestrictedYonedaDiagramMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) {X Y : S.FactorCategory K} (f : X ⟶ Y) : R.incidenceRestrictedYonedaDiagram X ⟶ R.incidenceRestrictedYonedaDiagram Y

Postcomposition gives the morphism of restricted-Yoneda boundary diagrams induced by a factor morphism.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceRestrictedYonedaDiagramFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) : CategoryTheory.Functor (S.FactorCategory K) (CategoryTheory.Functor (PosetSpace.BoundaryIndex T)ᵒᵖ (ModuleCat k))

Restricted Yoneda on the boundary category is functorial in the factor object.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedBoundaryLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (X : S.FactorCategory K) (t : T) : (R.projective t ⟶ X) ≃ₗ[k] ↥(R.representableData.precomposition t X).range

Precomposition with P ⟶ P_t identifies Hom(P_t,X) with its range inside Hom(P,X).

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceRestrictedYonedaDiagramComponentIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (X : S.FactorCategory K) (q : (PosetSpace.BoundaryIndex T)ᵒᵖ) : (R.incidenceRestrictedYonedaDiagram X).obj q ≅ (PosetSpace.boundaryDiagram k T (R.representableData.obj X)).obj q

Componentwise identification of boundary restricted Yoneda with the boundary diagram of the represented poset space.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceRestrictedYonedaDiagramIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (X : S.FactorCategory K) : R.incidenceRestrictedYonedaDiagram X ≅ PosetSpace.boundaryDiagram k T (R.representableData.obj X)

The boundary-category restricted Yoneda diagram is the same diagram as the one obtained from the concrete represented poset space.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceRestrictedYonedaDiagramNatIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) : R.incidenceRestrictedYonedaDiagramFunctor ≅ R.representableData.functor.comp (PosetSpace.boundaryDiagramFunctor k T)

The preceding objectwise isomorphisms are natural in the represented factor object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceRestrictedYonedaDiagram_isFiniteInjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (X : S.FactorCategory K) : PosetSpace.IsFiniteInjectiveBoundaryDiagram k T (R.incidenceRestrictedYonedaDiagram X)

Every restricted-Yoneda boundary diagram has finite values and injective maps into the root.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceRestrictedYonedaDiagram_no_supportedAwaySubdiagram {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] (R : S.PrimitiveProjectivePosetData D T) (X : S.FactorCategory K) (N : PosetSpace.BoundarySubdiagram k T (R.incidenceRestrictedYonedaDiagram X)) (hN : N.SupportedAwayFromRoot) : N.IsZero

Equivalently, a restricted-Yoneda boundary diagram has no nonzero subdiagram supported away from the root.