Intrinsic irreducible quotients compute arrow multiplicities

Borrowed from formalization/magnitude_conjecture (commit 52fbbfa2b): meshProjectiveBoundaryMap, meshRightAlmostSplitAt and its equation lemmas, and labelRightMesh_X₂ from Algebra/RightModuleStandardMesh.lean; the multiplicity lemmas indecomposableMultiplicity* from Algebra/RightModulePrimitiveDeletion.lean; and intrinsicIrreducible_finrank_eq_arrowMultiplicity from Algebra/RightModuleIntrinsicArrowMultiplicity.lean. Statements and proofs are unchanged apart from the namespace rename. The rest of those files is not needed and is not copied.

def MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.meshProjectiveBoundaryMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : S.projectiveBoundaryRadical z ⟶ S.almostSplitSkeleton.obj z

The projective radical inclusion written in the selected skeleton's object vocabulary.

noncomputable def MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.meshRightAlmostSplitAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : S.almostSplitSkeleton.MinimalRightAlmostSplitDecomposition z

A minimal right almost-split decomposition at every vertex, using the radical inclusion at a projective vertex and the chosen AR decomposition at a nonprojective vertex.

@[simp]

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.meshRightAlmostSplitAt_eq_of_not_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : ¬CategoryTheory.Projective (S.fgObj z)) : S.meshRightAlmostSplitAt z = S.minimalRightAlmostSplitAt z

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.meshRightAlmostSplitAt_eq_of_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : CategoryTheory.Projective (S.fgObj z)) : S.meshRightAlmostSplitAt z = QSE.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.ofMap S.almostSplitSkeleton (S.meshProjectiveBoundaryMap z) ⋯ ⋯ ⋯

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.labelRightMesh_X₂ {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : (S.labelRightMesh z).X₂ = (S.meshRightAlmostSplitAt z).middle

The middle term of the unified label mesh is the displayed middle term of the corresponding minimal right almost-split decomposition.

noncomputable def MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (M : FinitelyGeneratedCategory A) : ℕ

Multiplicity of one ambient skeleton label in the fixed displayed Krull--Schmidt decomposition of a finitely generated module.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_eq_of_decomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (M : FinitelyGeneratedCategory A) {n : ℕ} {label : Fin n → Fin S.n} (d : M ≅ ⨁ fun (i : Fin n) => S.fgObj (label i)) : S.indecomposableMultiplicity p M = ∑ i : Fin n, if label i = p then 1 else 0

The fixed multiplicity agrees with the occurrence count in any other displayed decomposition into the same ambient skeleton.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_eq_of_fintype_decomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (M : FinitelyGeneratedCategory A) {I : Type} [Fintype I] [Finite I] {label : I → Fin S.n} (d : M ≅ ⨁ fun (i : I) => S.fgObj (label i)) : S.indecomposableMultiplicity p M = ∑ i : I, if label i = p then 1 else 0

The fixed multiplicity agrees with a decomposition indexed by any finite type. This is the index-neutral form used by almost-split decompositions, whose index is stored as a FintypeCat.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.indecomposableMultiplicity_meshRightMiddle {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p z : Fin S.n) : S.indecomposableMultiplicity p (S.meshRightAlmostSplitAt z).middle = FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData p z

At every ambient endpoint, including the projective boundary, the fixed object multiplicity of the standard right-mesh middle term is exactly the ambient arrow multiplicity.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.intrinsicIrreducible_finrank_eq_arrowMultiplicity {k A : Type u'} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source target : Fin S.n) : Module.finrank k (CategoricalIrreducible.Space k (S.fgObj source) (S.fgObj target)) = FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData source target

Over an algebraically closed field the dimension of the intrinsic categorical irreducible quotient is the literal finite-tau arrow multiplicity, including arrows into projective vertices.