Crossing arrows and ambient meshes for primitive deletion

This file formalizes the crossing-mesh lemma in the live manuscript. Its first layer records the exact primitive-coordinate equation on every ambient Auslander--Reiten sequence and the quotient/submodule closure which prevents a crossing arrow from starting at an injective killed object or ending at a projective killed object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sum_primitiveMultiplicity_minimalRightMiddle_eq {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 : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : ∑ i : (S.minimalRightAlmostSplitAt ↑z).index.obj, S.primitiveMultiplicity D ((S.minimalRightAlmostSplitAt ↑z).label i) = S.primitiveMultiplicity D (S.rightTranslationLabel z) + S.primitiveMultiplicity D ↑z

Applying the primitive projective coordinate to an ambient Auslander--Reiten sequence gives the manuscript's additive equation d_(tau z) + d_z = sum_y a(y,z)d_y, with displayed arrow occurrences on the right.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_primitiveKilledLabels_of_epi {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) {x y : Fin S.n} (hx : x ∈ S.primitiveKilledLabels D) (f : S.fgObj x ⟶ S.fgObj y) [CategoryTheory.Epi f] : y ∈ S.primitiveKilledLabels D

The AeA-annihilated labels are closed under epimorphic images.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_primitiveKilledLabels_of_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) {x y : Fin S.n} (hy : y ∈ S.primitiveKilledLabels D) (f : S.fgObj x ⟶ S.fgObj y) [CategoryTheory.Mono f] : x ∈ S.primitiveKilledLabels D

The AeA-annihilated labels are closed under subobjects.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.not_injective_of_irreducible_from_primitiveKilled {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) {x y : Fin S.n} (hx : x ∈ S.primitiveKilledLabels D) (hy : y ∉ S.primitiveKilledLabels D) (f : S.fgObj x ⟶ S.fgObj y) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : ¬CategoryTheory.Injective (S.fgObj x)

An irreducible arrow leaving the killed subcategory cannot start at an injective ambient module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.not_projective_of_irreducible_to_primitiveKilled {k A : Type u} [Field k] [Ring A] [Algebra k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) {x y : Fin S.n} (hx : x ∉ S.primitiveKilledLabels D) (hy : y ∈ S.primitiveKilledLabels D) (f : S.fgObj x ⟶ S.fgObj y) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : ¬CategoryTheory.Projective (S.fgObj y)

An irreducible arrow entering the killed subcategory cannot end at a projective ambient module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightTranslation_not_mem_of_meshArrow_to_primitiveKilled {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 : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) (y : Fin S.n) (hz : ↑z ∈ S.primitiveKilledLabels D) (hy : y ∉ S.primitiveKilledLabels D) (a : S.MeshArrow (↑z) y) : S.rightTranslationLabel z ∉ S.primitiveKilledLabels D

If an incoming mesh occurrence crosses from the non-killed side into a killed endpoint, then the ambient translate of that endpoint is non-killed. This is the first orientation of the manuscript's crossing-sum argument.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.inverseTranslation_not_mem_of_meshArrow_from_primitiveKilled {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) (x : { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }) (y : Fin S.n) (hx : ↑x ∈ S.primitiveKilledLabels D) (hy : y ∉ S.primitiveKilledLabels D) (a : S.MeshArrow y ↑x) : ↑(S.rightTranslationEquiv.symm x) ∉ S.primitiveKilledLabels D

If a mesh occurrence crosses out of a killed source, the inverse ambient translate of that source is non-killed. Pairing the two sides of an ambient mesh reduces this to the preceding crossing-sum orientation.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveIncomingCrossingArrow {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 arrow occurrences entering the primitive-quotient subcategory. The stored mesh arrow represents the irreducible map source ⟶ target.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveOutgoingCrossingArrow {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 arrow occurrences leaving the primitive-quotient subcategory.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveCrossingArrow {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

All ambient arrows crossing between the quotient labels and their complement, with parallel occurrences retained.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveIncomingBoundaryMesh {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 meshes whose right endpoint is killed while its translate is not killed.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveOutgoingBoundaryMesh {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 meshes whose right endpoint is not killed while its translate is killed.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveBoundaryMesh {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 meshes with translation endpoints on opposite sides of the primitive deletion.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveBoundaryMeshEndpoint {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.PrimitiveBoundaryMesh D) : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }

Forget the orientation tag of a boundary mesh.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.incomingCrossingArrowBoundaryMesh {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) (a : S.PrimitiveIncomingCrossingArrow D) : S.PrimitiveIncomingBoundaryMesh D

A crossing arrow entering the killed subcategory determines the ambient mesh ending at its target.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.outgoingCrossingArrowBoundaryMesh {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) (a : S.PrimitiveOutgoingCrossingArrow D) : S.PrimitiveOutgoingBoundaryMesh D

A crossing arrow leaving the killed subcategory determines the ambient mesh whose left translation endpoint is its source.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.crossingArrowBoundaryMesh {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) : S.PrimitiveCrossingArrow D → S.PrimitiveBoundaryMesh D

The manuscript's map from crossing arrows to meshes with opposite translation endpoints.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveNonKilledMiddleOccurrence {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 : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : Type

Displayed middle occurrences lying on the non-killed side of an ambient mesh.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveNonKilledMiddleIndexEquiv {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 : { x : Fin S.n // ¬CategoryTheory.Projective (S.fgObj x) }) : { i : (S.meshRightAlmostSplitAt ↑z).index.obj // (S.meshRightAlmostSplitAt ↑z).label i ∉ S.primitiveKilledLabels D } ≃ S.PrimitiveNonKilledMiddleOccurrence D z

The displayed-index and labelled-arrow descriptions of a surviving middle occurrence are equivalent, with parallel occurrences retained.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.incomingCrossingArrowEquivBoundaryOccurrence {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.PrimitiveIncomingCrossingArrow D ≃ (z : S.PrimitiveIncomingBoundaryMesh D) × S.PrimitiveNonKilledMiddleOccurrence D ↑z

Incoming crossing arrows are the surviving middle occurrences in the boundary meshes ending on the killed side.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.outgoingCrossingArrowBoundaryOccurrence {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) (a : S.PrimitiveOutgoingCrossingArrow D) : (z : S.PrimitiveOutgoingBoundaryMesh D) × S.PrimitiveNonKilledMiddleOccurrence D ↑z

Pair an outgoing crossing arrow across its ambient mesh and retain its middle occurrence on the non-killed side.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.outgoingBoundaryOccurrenceCrossingArrow {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) (zi : (z : S.PrimitiveOutgoingBoundaryMesh D) × S.PrimitiveNonKilledMiddleOccurrence D ↑z) : S.PrimitiveOutgoingCrossingArrow D

Reconstruct an outgoing crossing arrow from its paired middle occurrence.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sum_primitiveMultiplicity_incomingBoundaryMesh_eq_one {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) (z : S.PrimitiveIncomingBoundaryMesh D) : ∑ i : (S.minimalRightAlmostSplitAt ↑↑z).index.obj, S.primitiveMultiplicity D ((S.minimalRightAlmostSplitAt ↑↑z).label i) = 1

At a boundary mesh ending on the killed side, the full displayed primitive-coordinate sum is one.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.sum_primitiveMultiplicity_outgoingBoundaryMesh_eq_one {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) (z : S.PrimitiveOutgoingBoundaryMesh D) : ∑ i : (S.minimalRightAlmostSplitAt ↑↑z).index.obj, S.primitiveMultiplicity D ((S.minimalRightAlmostSplitAt ↑↑z).label i) = 1

At a boundary mesh ending on the non-killed side, the full displayed primitive-coordinate sum is also one.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_primitiveNonKilledMiddleOccurrence_eq_one {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) (z : S.PrimitiveBoundaryMesh D) : Nat.card (S.PrimitiveNonKilledMiddleOccurrence D (S.primitiveBoundaryMeshEndpoint D z)) = 1

Every ambient boundary mesh has exactly one displayed middle occurrence on the non-killed side.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.outgoingCrossingArrowEquivBoundaryOccurrence {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) : S.PrimitiveOutgoingCrossingArrow D ≃ (z : S.PrimitiveOutgoingBoundaryMesh D) × S.PrimitiveNonKilledMiddleOccurrence D ↑z

Outgoing crossing arrows, paired across their ambient mesh, are the surviving middle occurrences in the boundary meshes ending on the non-killed side. Uniqueness of the surviving occurrence makes the result independent of the proof transports used to recover the inverse translate.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.crossingArrowEquivBoundaryOccurrence {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) : S.PrimitiveCrossingArrow D ≃ (z : S.PrimitiveBoundaryMesh D) × S.PrimitiveNonKilledMiddleOccurrence D (S.primitiveBoundaryMeshEndpoint D z)

Both crossing orientations together are the disjoint union, over boundary meshes, of their surviving middle occurrences.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.card_primitiveCrossingArrow_eq_card_primitiveBoundaryMesh {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.PrimitiveCrossingArrow D) = Nat.card (S.PrimitiveBoundaryMesh D)

The number of ambient crossing-arrow occurrences is the number of ambient meshes whose translation endpoints lie on opposite sides of the primitive deletion.