Poset-space realization data for a primitive factor

This file specializes the concrete representable poset-space functor to the literal primitive factor category. The primitive multiplicity package already supplies finite-dimensional represented Hom spaces and faithfulness of Hom(P, -). Consequently the only remaining realization input is the manuscript's projective-poset presentation together with Iyama fullness and essential surjectivity.

The repaired manuscript derives the concrete T-space model from Iyama's minimal realization: restricted Yoneda lands in modules over the boundary projective incidence category, and the projective-socle condition identifies its image with subspace representations. The structures below isolate the remaining fullness and object-realization part of that derivation. They are not hypotheses of the eventual public magnitude theorem.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FactorProjectiveLabel {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)) : Type

The finite type of tau-projective surviving labels in a literal factor.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FactorInjectiveLabel {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)) : Type

The finite type of tau-injective surviving labels in a literal factor.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.sourceProjectiveLabel {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) : S.FactorProjectiveLabel K

Primitive multiplicity data makes the distinguished source a literal tau-projective label of the factor.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.sinkInjectiveLabel {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) : S.FactorInjectiveLabel K

Primitive multiplicity data makes the distinguished sink a literal tau-injective label of the factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.factorHomFrom_finrank_eq_multiplicity {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) (x : S.SurvivingLabel K) : Module.finrank k (S.factorObject K D.source ⟶ S.factorObject K x) = D.multiplicity ↑x

Finrank form of the primitive multiplicity identity in the literal factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.factorHomTo_finrank_eq_multiplicity {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) (x : S.SurvivingLabel K) : Module.finrank k (S.factorObject K x ⟶ S.factorObject K D.sink) = D.multiplicity ↑x

Dual finrank form of the primitive multiplicity identity in the literal factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.exists_factorHomFrom_ne_zero {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) (x : S.SurvivingLabel K) : ∃ (h : S.factorObject K D.source ⟶ S.factorObject K x), h ≠ 0

Every surviving factor label receives a nonzero map from the primitive source.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.sourcePostcomposition {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) {X Y : S.FactorCategory K} (f : X ⟶ Y) : (S.factorObject K D.source ⟶ X) →ₗ[k] S.factorObject K D.source ⟶ Y

Postcomposition on the represented factor Hom space.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.sourcePostcomposition_injective {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) {x y : S.SurvivingLabel K} (hx : D.multiplicity ↑x = 1) (hy : D.multiplicity ↑y = 1) (f : S.factorObject K x ⟶ S.factorObject K y) (hf : f ≠ 0) : Function.Injective ⇑(sourcePostcomposition S D f)

Between multiplicity-one objects, every nonzero factor morphism induces an injective map on represented Hom.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveMultiplicityInput.comp_ne_zero_of_multiplicity_eq_one {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) {x y z : S.SurvivingLabel K} (hx : D.multiplicity ↑x = 1) (hy : D.multiplicity ↑y = 1) (hz : D.multiplicity ↑z = 1) (f : S.factorObject K x ⟶ S.factorObject K y) (hf : f ≠ 0) (g : S.factorObject K y ⟶ S.factorObject K z) (hg : g ≠ 0) : CategoryTheory.CategoryStruct.comp f g ≠ 0

The composite of nonzero maps between multiplicity-one factor objects is nonzero. This is the paper's faithfulness-plus-nonzero-scalars argument.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.NonSourceFactorProjectiveLabel {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) : Type

Tau-projective labels other than the distinguished root.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData {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) : Prop

The exact directed boundary input preceding the poset-space realization in the frozen manuscript.

• acyclic : S.HasAcyclicNonzeroNonisomorphisms
• projective_multiplicity_eq_one (p : S.FactorProjectiveLabel K) : D.multiplicity ↑↑p = 1
• injective_multiplicity_eq_one (i : S.FactorInjectiveLabel K) : D.multiplicity ↑↑i = 1

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.ProjectivePoset {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} (B : S.PrimitiveDirectedBoundaryData D) : Type u

The non-root projective labels, tagged by the boundary data that proves their Hom relation is an order.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.projectivePosetFintype {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} (B : S.PrimitiveDirectedBoundaryData D) : Fintype B.ProjectivePoset

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.projectiveLE {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} (B : S.PrimitiveDirectedBoundaryData D) (s t : B.ProjectivePoset) : Prop

Reverse nonzero-Hom reachability on the non-root projectives.

@[reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.projectivePartialOrder {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} (B : S.PrimitiveDirectedBoundaryData D) : PartialOrder B.ProjectivePoset

The literal Hom relation is a partial order on the non-root tau-projectives.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.projectivePosetPartialOrder {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} (B : S.PrimitiveDirectedBoundaryData D) : PartialOrder B.ProjectivePoset

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData {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] : Type u

The manuscript's presentation of all tau-projectives as the root P together with the projectives P_t, indexed by a finite poset T.

The field order_iff_nonzero is the literal order s ≤ t ↔ Q(P_t,P_s) ≠ 0. The chosen nonzero maps unit t : P ⟶ P_t and their factorization property are precisely the data used by the concrete representable functor.

• projectiveEquiv : S.FactorProjectiveLabel K ≃ Option T
• source_eq_none : self.projectiveEquiv (PrimitiveMultiplicityInput.sourceProjectiveLabel S D) = none
• projective_multiplicity_eq_one (p : S.FactorProjectiveLabel K) : D.multiplicity ↑↑p = 1
• order_iff_nonzero (s t : T) : s ≤ t ↔ ∃ (f : S.factorObject K ↑(self.projectiveEquiv.symm (some t)) ⟶ S.factorObject K ↑(self.projectiveEquiv.symm (some s))), f ≠ 0
• unit (t : T) : S.factorObject K D.source ⟶ S.factorObject K ↑(self.projectiveEquiv.symm (some t))
• unit_ne_zero (t : T) : self.unit t ≠ 0
• factor {s t : T} : s ≤ t → ∃ (v : S.factorObject K ↑(self.projectiveEquiv.symm (some t)) ⟶ S.factorObject K ↑(self.projectiveEquiv.symm (some s))), CategoryTheory.CategoryStruct.comp (self.unit t) v = self.unit s

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.projectiveEquiv {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} (B : S.PrimitiveDirectedBoundaryData D) : S.FactorProjectiveLabel K ≃ Option B.ProjectivePoset

The canonical enumeration of all projectives by the root plus the non-root projective poset.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.projectiveEquiv_source {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} (B : S.PrimitiveDirectedBoundaryData D) : B.projectiveEquiv (PrimitiveMultiplicityInput.sourceProjectiveLabel S D) = none

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.projectiveEquiv_symm_some {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} (B : S.PrimitiveDirectedBoundaryData D) (t : B.ProjectivePoset) : B.projectiveEquiv.symm (some t) = ↑t.down

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.unit {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} (B : S.PrimitiveDirectedBoundaryData D) (t : B.ProjectivePoset) : S.factorObject K D.source ⟶ S.factorObject K ↑↑t.down

A chosen nonzero map P ⟶ P_t, obtained from positivity of the primitive multiplicity.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.unit_ne_zero {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} (B : S.PrimitiveDirectedBoundaryData D) (t : B.ProjectivePoset) : B.unit t ≠ 0

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.exists_unit_factor {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} (B : S.PrimitiveDirectedBoundaryData D) {s t : B.ProjectivePoset} (hst : s ≤ t) : ∃ (v : S.factorObject K ↑↑t.down ⟶ S.factorObject K ↑↑s.down), CategoryTheory.CategoryStruct.comp (B.unit t) v = B.unit s

In the one-dimensional represented Hom space, the nonzero composite P ⟶ P_t ⟶ P_s is a scalar multiple of the chosen P ⟶ P_s; rescaling the second map gives the required literal factorization.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.projectivePosetData {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} (B : S.PrimitiveDirectedBoundaryData D) : S.PrimitiveProjectivePosetData D B.ProjectivePoset

Directedness and boundary multiplicity one construct the complete projective-poset presentation used by the representable functor.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.label {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) (t : T) : S.SurvivingLabel K

The selected surviving label underlying P_t.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.projective {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) (t : T) : S.FactorCategory K

The P_t indexed by the projective poset.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.card_factorProjectiveLabel {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) : Fintype.card (S.FactorProjectiveLabel K) = Fintype.card T + 1

The projective enumeration proves the manuscript's count p = |T| + 1.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representableData {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) : PosetSpace.RepresentableData k T (S.FactorCategory K)

The projective-poset presentation instantiates the manuscript's concrete representable T-space data on the literal factor category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representable_faithful {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.representableData.functor.Faithful

The represented Hom functor of a primitive factor is faithful; no faithfulness field remains in the Iyama realization input below.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.exists_smul_unit_eq {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) (t : T) (h : S.factorObject K D.source ⟶ S.factorObject K (R.label t)) : ∃ (c : k), c • R.unit t = h

The chosen boundary map P ⟶ P_t spans the one-dimensional represented Hom space.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.precomposition_injective {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) (t : T) (X : S.FactorCategory K) : Function.Injective ⇑(R.representableData.precomposition t X)

Precomposition with P ⟶ P_t is injective. This is the manuscript's faithfulness argument, with the scalar spanning step made explicit.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.finrank_subspace_eq_projectiveHom {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) (t : T) (X : S.FactorCategory K) : Module.finrank k ↥((R.representableData.obj X).subspace t) = Module.finrank k (R.projective t ⟶ X)

The represented subspace at t has the same dimension as Hom(P_t,X), because its defining precomposition map is injective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.projectiveHom_finrank_le_one {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) (s t : T) : Module.finrank k (R.projective t ⟶ R.projective s) ≤ 1

Every Hom space between two non-root projectives has dimension at most one. It injects into the one-dimensional represented Hom space of its target.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceMap {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) {s t : T} (hst : s ≤ t) : R.projective t ⟶ R.projective s

The normalized incidence morphism P_t ⟶ P_s for s ≤ t.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.unit_comp_incidenceMap {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) {s t : T} (hst : s ≤ t) : CategoryTheory.CategoryStruct.comp (R.unit t) (R.incidenceMap hst) = R.unit s

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.unit_comp_incidenceMap_assoc {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) {s t : T} (hst : s ≤ t) {Z : S.FactorCategory K} (h : R.projective s ⟶ Z) : CategoryTheory.CategoryStruct.comp (R.unit t) (CategoryTheory.CategoryStruct.comp (R.incidenceMap hst) h) = CategoryTheory.CategoryStruct.comp (R.unit s) h

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceMap_ne_zero {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) {s t : T} (hst : s ≤ t) : R.incidenceMap hst ≠ 0

A normalized incidence morphism is nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceMap_unique {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) {s t : T} (hst : s ≤ t) (f : R.projective t ⟶ R.projective s) (hf : CategoryTheory.CategoryStruct.comp (R.unit t) f = R.unit s) : f = R.incidenceMap hst

Normalization by the chosen maps from P determines an incidence morphism uniquely.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.incidenceMap_comp {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 s t : T} (hrs : r ≤ s) (hst : s ≤ t) : CategoryTheory.CategoryStruct.comp (R.incidenceMap hst) (R.incidenceMap hrs) = R.incidenceMap ⋯

The normalized incidence maps have literal incidence composition.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.exists_smul_incidenceMap_eq {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) {s t : T} (hst : s ≤ t) (f : R.projective t ⟶ R.projective s) : ∃ (c : k), c • R.incidenceMap hst = f

Every morphism along an incidence relation is a scalar multiple of the normalized incidence morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.eq_zero_of_projectiveHom_of_not_le {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) {s t : T} (hst : ¬s ≤ t) (f : R.projective t ⟶ R.projective s) : f = 0

Off the incidence order there are no morphisms between the corresponding projectives.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.unitScalarLinearMap {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) (t : T) : k →ₗ[k] S.factorObject K D.source ⟶ S.factorObject K (R.label t)

Scalar multiplication of the chosen P ⟶ P_t map, as a linear map from the coefficient field.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.unitCoordinateEquiv {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) (t : T) : (S.factorObject K D.source ⟶ S.factorObject K (R.label t)) ≃ₗ[k] k

The chosen boundary map identifies Hom(P,P_t) with the coefficient field.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.unitCoordinateEquiv_symm_apply {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) (t : T) (c : k) : (R.unitCoordinateEquiv t).symm c = c • R.unit t

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedProjectiveCoordinateEquiv {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) (t : T) : (R.representableData.obj (R.projective t)).carrier ≃ₗ[k] k

The same coordinate equivalence with the carrier of the represented poset space exposed in its statement.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedProjectiveCoordinateEquiv_symm_apply {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) (t : T) (c : k) : (R.representedProjectiveCoordinateEquiv t).symm c = c • R.unit t

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.projectiveObjIsoLine {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) (s : T) : R.representableData.obj (R.projective s) ≅ PosetSpace.line k T (Set.Ici s) ⋯

The represented image of P_s is the one-dimensional poset space on the principal filter generated by s.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sourceProjectiveLabel_ne_projective {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) (t : T) : PrimitiveMultiplicityInput.sourceProjectiveLabel S D ≠ R.projectiveEquiv.symm (some t)

The distinguished source projective is different from every projective indexed by T.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.eq_zero_of_projectiveHom_to_source {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) (H : S.HasAcyclicNonzeroNonisomorphisms) (t : T) (f : R.projective t ⟶ R.representableData.source) : f = 0

Directedness rules out a morphism from a non-root projective back to the distinguished source.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sourceIdScalarLinearMap {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) : k →ₗ[k] R.representableData.source ⟶ R.representableData.source

Scalar multiplication of the identity of the distinguished source.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sourceCoordinateEquiv {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.representableData.source ⟶ R.representableData.source) ≃ₗ[k] k

The identity gives a coordinate on the one-dimensional represented Hom space of the distinguished source.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sourceCoordinateEquiv_symm_apply {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) (c : k) : R.sourceCoordinateEquiv.symm c = c • CategoryTheory.CategoryStruct.id R.representableData.source

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedSourceCoordinateEquiv {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.representableData.obj R.representableData.source).carrier ≃ₗ[k] k

The source coordinate with the carrier of its represented poset space exposed.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sourceObjIsoEmptyLine {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) (H : S.HasAcyclicNonzeroNonisomorphisms) : R.representableData.obj R.representableData.source ≅ PosetSpace.line k T ∅ ⋯

Restricted Yoneda sends the distinguished source to the line with empty support.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sinkUnit {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.representableData.source ⟶ S.factorObject K D.sink

A chosen nonzero element of the one-dimensional represented Hom space of the distinguished sink.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sinkUnit_ne_zero {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.sinkUnit ≠ 0

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sinkUnitScalarLinearMap {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) : k →ₗ[k] R.representableData.source ⟶ S.factorObject K D.sink

Scalar multiplication of the chosen source-to-sink map.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sinkCoordinateEquiv {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) (hsink : D.multiplicity ↑D.sink = 1) : (R.representableData.source ⟶ S.factorObject K D.sink) ≃ₗ[k] k

A multiplicity-one sink has its represented Hom space canonically coordinatized by the chosen source-to-sink map.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.precomposition_surjective_to_sink {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) (hsink : D.multiplicity ↑D.sink = 1) (t : T) : Function.Surjective ⇑(R.representableData.precomposition t (S.factorObject K D.sink))

Precomposition from every non-root projective onto a multiplicity-one sink is surjective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representedSinkCoordinateEquiv {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) (hsink : D.multiplicity ↑D.sink = 1) : (R.representableData.obj (S.factorObject K D.sink)).carrier ≃ₗ[k] k

The sink coordinate with the represented carrier exposed.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.sinkObjIsoFullLine {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) (hsink : D.multiplicity ↑D.sink = 1) : R.representableData.obj (S.factorObject K D.sink) ≅ PosetSpace.line k T Set.univ ⋯

Restricted Yoneda sends a multiplicity-one distinguished sink to the line with full support.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.finrank_obj_factorObject {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.SurvivingLabel K) : Module.finrank k (R.representableData.obj (S.factorObject K x)).carrier = D.multiplicity ↑x

The total dimension of the realized selected indecomposable is exactly the ambient primitive multiplicity d_X.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.exists_source_hom_ne_zero {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.SurvivingLabel K) : ∃ (h : R.representableData.source ⟶ S.factorObject K x), h ≠ 0

Every surviving selected indecomposable has a nonzero map from the distinguished source, because its primitive multiplicity is positive.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.sourceObjIsoEmptyLine {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} (B : S.PrimitiveDirectedBoundaryData D) : B.projectivePosetData.representableData.obj B.projectivePosetData.representableData.source ≅ PosetSpace.line k B.ProjectivePoset ∅ ⋯

The concrete primitive boundary sends its distinguished source to the empty-support line.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.sinkObjIsoFullLine {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} (B : S.PrimitiveDirectedBoundaryData D) : B.projectivePosetData.representableData.obj (S.factorObject K D.sink) ≅ PosetSpace.line k B.ProjectivePoset Set.univ ⋯

The concrete primitive boundary sends its distinguished sink to the full-support line.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.card_factorProjectiveLabel {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} (B : S.PrimitiveDirectedBoundaryData D) : Fintype.card (S.FactorProjectiveLabel K) = Fintype.card B.ProjectivePoset + 1

The directed boundary package gives the manuscript's exact projective count p = |T| + 1.