The D4 boundary forced by one-sided beta failure

Translation removes every interior obstruction to comparing the two beta invariants. If right beta is at most two but left beta is not, the remaining injective boundary vertex has three distinct nonprojective successors. This file packages those successors as literal reversed-AR-quiver arrows, retaining the occurrence data needed by the subsequent sectional or module argument.

@[reducible, inline]

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

Literal outgoing AR occurrences from source whose target is nonprojective. The standard-form arrow is reversed, so an element over target represents an irreducible module map source ⟶ target.

@[reducible, inline]

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

Literal incoming AR occurrences at target whose source is nonprojective. In the reversed standard-form quiver these are arrows from target to the displayed source.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.natCard_nonprojectiveOutgoingOccurrence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (source : Fin S.n) : Nat.card (S.NonprojectiveOutgoingOccurrence source) = S.nonprojectiveOutgoingAt source

The occurrence type has the cardinality recorded by the numerical nonprojective outgoing count.

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

The incoming occurrence type has cardinality betaAt.

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

A literal three-armed boundary fork. Its arrows point from the center to the three targets in the module AR quiver (and hence from each target to the center in the standard-form quiver).

• center : { i : Fin S.n // ¬CategoryTheory.Projective (S.fgObj i) }
• center_injective : CategoryTheory.Injective (S.fgObj ↑self.center)
• target : Fin 3 → { i : Fin S.n // ¬CategoryTheory.Projective (S.fgObj i) }
• arrow (j : Fin 3) : S.StandardFormArrow ↑(self.target j) ↑self.center
• target_injective : Function.Injective self.target

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.outgoingMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.InjectiveNonprojectiveD4Fork) (j : Fin 3) : S.fgObj ↑F.center ⟶ S.fgObj ↑(F.target j)

The actual irreducible quotient map represented by one fork arm.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.outgoingMap_epi {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.InjectiveNonprojectiveD4Fork) (j : Fin 3) : CategoryTheory.Epi (outgoingMap S F j)

Every fork arm is an epimorphism: a monic irreducible map out of the injective center would split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.target_objectFinrank_lt_center {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.InjectiveNonprojectiveD4Fork) (j : Fin 3) : S.objectFinrank ↑(F.target j) < S.objectFinrank ↑F.center

Every target of the injective boundary fork has strictly smaller coefficient-field dimension than its center.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.translatedTarget {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.InjectiveNonprojectiveD4Fork) (j : Fin 3) : Fin S.n

The source paired to one arm by the mesh polarization.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.translatedTarget_not_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.InjectiveNonprojectiveD4Fork) (j : Fin 3) : ¬CategoryTheory.Injective (S.fgObj (translatedTarget S F j))

A translated fork target is noninjective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.translatedArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.InjectiveNonprojectiveD4Fork) (j : Fin 3) : S.StandardFormArrow (↑F.center) (translatedTarget S F j)

Polarizing an outgoing fork arrow gives an incoming arrow from its translated target to the center.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.translatedTarget_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.InjectiveNonprojectiveD4Fork) : Function.Injective (translatedTarget S F)

Distinct fork arms have distinct translated targets.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.exists_projective_translatedTarget {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.InjectiveNonprojectiveD4Fork) (hbeta : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ 2) : ∃ (j : Fin 3), CategoryTheory.Projective (S.fgObj (translatedTarget S F j))

If right beta is at most two, a three-armed boundary fork has a projective translated arm. Otherwise polarization would inject its three arms into the nonprojective incoming occurrences at the center.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_injectiveNonprojectiveD4Fork_of_boundary {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { i : Fin S.n // ¬CategoryTheory.Projective (S.fgObj i) }) (hzInjective : CategoryTheory.Injective (S.fgObj ↑z)) (hz : 3 ≤ S.nonprojectiveOutgoingAt ↑z) : Nonempty S.InjectiveNonprojectiveD4Fork

Three distinct outgoing occurrences determine a literal D4 boundary fork. Representation-finite square-freeness is what makes their target labels distinct rather than merely their occurrence indices.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_injectiveNonprojectiveD4Fork_of_beta_le_two {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hbeta : FiniteTauMatrix.beta S.finiteTauCategoryData.toFiniteRightTauCategoryData ≤ 2) (hleft : ¬S.leftBeta ≤ 2) : Nonempty S.InjectiveNonprojectiveD4Fork

Under beta ≤ 2, failure of the opposite beta bound yields the canonical three-armed injective boundary fork.