Direct arrow and mesh partitions for primitive deletion

This file formalizes the finite partitions used in the live manuscript's direct count. Every ambient arrow occurrence is internal to the killed subcategory, internal to its complement, or crosses the boundary. Every ambient nonprojective mesh likewise has both translation endpoints killed, both surviving, or on opposite sides.

theorem QuotientSubmoduleEquidistribution.IsRightAlmostSplit.fullSubcategory {C : Type v} [CategoryTheory.Category.{w, v} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (f : X ⟶ Y) (hf : IsRightAlmostSplit f.hom) : IsRightAlmostSplit f

A right almost-split morphism remains right almost split after restricting both endpoints to a full subcategory.

@[instance_reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveDirectCountQuotientFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Fintype (S.PrimitiveQuotientLabel D)

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.AmbientArrowOccurrence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Type

All ambient Auslander--Reiten arrow occurrences, with parallel arrows retained.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveKilledInternalArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Type

Ambient arrows with both endpoints in the primitive quotient subcategory mod (A/AeA).

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveKilledInternalArrowEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : S.PrimitiveKilledInternalArrow D ≃ (target : S.PrimitiveQuotientLabel D) × (source : S.PrimitiveQuotientLabel D) × S.MeshArrow ↑target ↑source

Internal ambient arrow occurrences, reindexed by the literal quotient labels at their two endpoints.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.arrowMultiplicity_eq_card_meshArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source target : Fin S.n) : FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData source target = Nat.card (S.MeshArrow target source)

The official ambient arrow multiplicity is the cardinality of the chosen ambient mesh-arrow occurrence type.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientIrreducibleArrowMultiplicity_eq_card_meshArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (source target : S.PrimitiveQuotientLabel D) : S.ambientIrreducibleArrowMultiplicity D source target = Nat.card (S.MeshArrow ↑target ↑source)

For surviving labels, the ambient intrinsic irreducible-arrow multiplicity is the cardinality of the chosen ambient mesh-arrow type.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_primitiveKilledInternalArrow_eq_sum_ambientMultiplicity {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : Nat.card (S.PrimitiveKilledInternalArrow D) = ∑ source : S.PrimitiveQuotientLabel D, ∑ target : S.PrimitiveQuotientLabel D, S.ambientIrreducibleArrowMultiplicity D source target

The ambient-arrow count internal to mod (A/AeA) is the sum of the ambient intrinsic arrow multiplicities over surviving endpoints.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientArrowCount_eq_card_ambientArrowOccurrence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ARCount.arrowCount (FiniteTauMatrix.arrowMultiplicity S.finiteTauCategoryData.toFiniteRightTauCategoryData) = ↑(Nat.card S.AmbientArrowOccurrence)

The official total ambient arrow count is the cardinality of all chosen ambient mesh-arrow occurrences, with parallel arrows retained.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveSurvivingInternalArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Type

Ambient arrows with both endpoints in the strict factor.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveSurvivingInternalArrowEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : S.PrimitiveSurvivingInternalArrow D ≃ (target : S.SurvivingLabel (S.primitiveKilledLabels D)) × (source : S.SurvivingLabel (S.primitiveKilledLabels D)) × S.MeshArrow ↑target ↑source

Internal strict-factor arrow occurrences, reindexed by their surviving endpoint labels.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorMiddleSurvivingIndexEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (target : S.SurvivingLabel (S.primitiveKilledLabels D)) : { i : (S.meshRightAlmostSplitAt ↑target).index.obj // (S.meshRightAlmostSplitAt ↑target).label i ∉ S.primitiveKilledLabels D } ≃ (source : S.SurvivingLabel (S.primitiveKilledLabels D)) × S.MeshArrow ↑target ↑source

The surviving summand indices in the ambient right-mesh middle term are exactly its arrow occurrences whose source also survives.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightMiddleSurvivingDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (target : S.SurvivingLabel (S.primitiveKilledLabels D)) : CategoryTheory.FiniteIndecomposableDecomposition ((S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).rightMesh ((S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).obj target)).X₂

The strict factor's right-mesh middle term, decomposed by the surviving summands of the corresponding ambient right-mesh middle term.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorRightMiddleArity_eq_card_survivingMeshArrows {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (target : S.SurvivingLabel (S.primitiveKilledLabels D)) : FiniteTauMatrix.rightMiddleArity (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).toFiniteRightTauCategoryData target = Nat.card ((source : S.SurvivingLabel (S.primitiveKilledLabels D)) × S.MeshArrow ↑target ↑source)

The total incoming multiplicity at a strict-factor vertex is the number of surviving ambient arrow occurrences entering it.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorArrowCount_eq_card_primitiveSurvivingInternalArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : ARCount.arrowCount (FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).toFiniteRightTauCategoryData) = ↑(Nat.card (S.PrimitiveSurvivingInternalArrow D))

The strict factor's official total arrow count is the cardinality of the ambient arrow occurrences internal to the strict factor.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientArrowRegionEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : S.AmbientArrowOccurrence ≃ S.PrimitiveKilledInternalArrow D ⊕ S.PrimitiveSurvivingInternalArrow D ⊕ S.PrimitiveCrossingArrow D

The manuscript's three-region partition of ambient arrows.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_ambientArrowOccurrence_eq_internal_add_crossing {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Nat.card S.AmbientArrowOccurrence = Nat.card (S.PrimitiveKilledInternalArrow D) + Nat.card (S.PrimitiveSurvivingInternalArrow D) + Nat.card (S.PrimitiveCrossingArrow D)

The ambient arrow count is a₀ + a_H + z.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjective_of_ambient_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x : S.SurvivingLabel (S.primitiveKilledLabels D)) (hx : CategoryTheory.Projective (S.fgObj ↑x)) : (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).IsProjective x

An ambient projective label remains tau-projective in the strict factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjective_of_translation_killed {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x : S.SurvivingLabel (S.primitiveKilledLabels D)) (hx : ¬CategoryTheory.Projective (S.fgObj ↑x)) (htranslate : S.rightTranslationLabel ⟨↑x, hx⟩ ∈ S.primitiveKilledLabels D) : (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).IsProjective x

If the ambient translate of a surviving nonprojective label is killed, that label is tau-projective in the strict factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorProjective_iff_ambient_projective_or_translation_killed {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x : S.SurvivingLabel (S.primitiveKilledLabels D)) : (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).IsProjective x ↔ CategoryTheory.Projective (S.fgObj ↑x) ∨ ∃ (hx : ¬CategoryTheory.Projective (S.fgObj ↑x)), S.rightTranslationLabel ⟨↑x, hx⟩ ∈ S.primitiveKilledLabels D

A strict-factor label is tau-projective exactly at the ambient projective boundary or when its ambient translate is killed.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveSurvivingInternalMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Type

Ambient nonprojective meshes whose two translation endpoints lie in the strict factor.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.factorNonprojectiveEquivPrimitiveSurvivingInternalMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : { x : S.SurvivingLabel (S.primitiveKilledLabels D) // ¬(S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).IsProjective x } ≃ S.PrimitiveSurvivingInternalMesh D

Nonprojective strict-factor labels are precisely ambient meshes whose two translation endpoints survive.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_factorNonprojective_eq_card_primitiveSurvivingInternalMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Nat.card { x : S.SurvivingLabel (S.primitiveKilledLabels D) // ¬(S.factorFiniteTauCategoryData (S.primitiveKilledLabels D)).IsProjective x } = Nat.card (S.PrimitiveSurvivingInternalMesh D)

The q-p meshes of the strict primitive factor are exactly the ambient meshes internal to the surviving region.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveKilledInternalMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Type

Ambient nonprojective meshes whose two translation endpoints lie in the primitive quotient subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientLabelObj_projective_of_ambient_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x : S.PrimitiveQuotientLabel D) (hx : CategoryTheory.Projective (S.fgObj ↑x)) : CategoryTheory.Projective (S.primitiveQuotientLabelObj D x)

An ambient-projective quotient label remains projective in the exact full subcategory of modules annihilated by AeA.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientLabelObj_not_projective_of_internalMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (z : S.PrimitiveKilledInternalMesh D) : ¬CategoryTheory.Projective (S.primitiveQuotientLabelObj D ⟨↑↑z, ⋯⟩)

An ambient mesh with both translation endpoints in mod (A/AeA) remains a right almost-split mesh there, so its endpoint is nonprojective in the literal quotient subcategory.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveQuotientNonprojectiveMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Type

The nonprojective mesh endpoints of the literal primitive quotient.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientNonprojectiveMeshEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : S.PrimitiveQuotientNonprojectiveMesh D ≃ S.PrimitiveKilledInternalMesh D ⊕ S.PrimitiveNewRightMeshEndpoint D

Every quotient mesh is either inherited from an ambient mesh with both translation endpoints killed, or is new; the two cases are disjoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_primitiveQuotientNonprojectiveMesh_eq_internal_add_new {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Nat.card (S.PrimitiveQuotientNonprojectiveMesh D) = Nat.card (S.PrimitiveKilledInternalMesh D) + Nat.card (S.PrimitiveNewRightMeshEndpoint D)

The quotient mesh count is the number of inherited internal meshes plus the number of genuinely new meshes.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ambientMeshRegionEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) } ≃ S.PrimitiveKilledInternalMesh D ⊕ S.PrimitiveSurvivingInternalMesh D ⊕ S.PrimitiveBoundaryMesh D

The manuscript's three-region partition of ambient meshes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_ambientNonprojective_eq_internalMesh_add_boundary {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Nat.card { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) } = Nat.card (S.PrimitiveKilledInternalMesh D) + Nat.card (S.PrimitiveSurvivingInternalMesh D) + Nat.card (S.PrimitiveBoundaryMesh D)

The ambient mesh count is the sum of the two internal regions and the boundary meshes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_ambientVertex_eq_quotient_add_factor {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Nat.card (Fin S.n) = Nat.card (S.PrimitiveQuotientLabel D) + Nat.card (S.SurvivingLabel (S.primitiveKilledLabels D))

The ambient labels split into the literal quotient labels and the strict-factor labels.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_ambientVertex_eq_projective_add_nonprojective {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Nat.card (Fin S.n) = Nat.card { x : Fin S.n // CategoryTheory.Projective (S.fgObj x) } + Nat.card { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }

Ambient vertices split into projective vertices and mesh endpoints.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_primitiveQuotientVertex_eq_projective_add_nonprojective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Nat.card (S.PrimitiveQuotientLabel D) = Nat.card { x : S.PrimitiveQuotientLabel D // CategoryTheory.Projective (S.primitiveQuotientLabelObj D x) } + Nat.card (S.PrimitiveQuotientNonprojectiveMesh D)

Literal quotient vertices split into projective vertices and mesh endpoints.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_factorVertex_eq_projective_add_internalMesh {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) : Nat.card (S.SurvivingLabel (S.primitiveKilledLabels D)) = Nat.card (S.FactorProjectiveLabel (S.primitiveKilledLabels D)) + Nat.card (S.PrimitiveSurvivingInternalMesh D)

Strict-factor vertices split into tau-projectives and ambient meshes internal to the surviving region.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_primitiveNewRightMeshEndpoint_eq_crossing_sub_projectiveRemainder {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (H : S.HasAcyclicNonzeroNonisomorphisms) : ↑(Nat.card (S.PrimitiveNewRightMeshEndpoint ⋯)) = ↑(Nat.card (S.PrimitiveCrossingArrow ⋯)) - (↑(Nat.card (S.FactorProjectiveLabel (S.primitiveKilledLabels ⋯))) - 1)

The complete primitive-projective presentation and the finite mesh partitions give the manuscript's exact formula r = z - (p - 1).