Gabriel's direct comparison of the two beta bounds

This file develops the local module argument excluding the injective D4 boundary fork forced by a failure of the opposite beta bound. The first step identifies the chosen minimal left almost-split middle term out of the injective center with its socle quotient. The three arms of the fork then force that quotient to have at least three indecomposable summands.

theorem MagnitudeConjecture.indecomposable_of_epi_from_simpleTop {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (P Y : RightModule.FinitelyGeneratedCategory A) (hPtop : IsSimpleModule Aᵐᵒᵖ (↑P ⧸ Module.jacobson Aᵐᵒᵖ ↑P)) (hY : ¬CategoryTheory.Limits.IsZero Y) (f : P ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Indecomposable Y

A nonzero quotient of a finite module with simple top is indecomposable.

theorem MagnitudeConjecture.simple_kernel_of_irreducible_epi_from_simpleTop {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (P Y : RightModule.FinitelyGeneratedCategory A) (hPtop : IsSimpleModule Aᵐᵒᵖ (↑P ⧸ Module.jacobson Aᵐᵒᵖ ↑P)) (hY : CategoryTheory.Indecomposable Y) (f : P ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) [CategoryTheory.Epi f] : IsSimpleModule Aᵐᵒᵖ ↥(ModuleCat.Hom.hom f.hom).ker

An irreducible epimorphism from a finite module with simple top has simple kernel. This is the elementary local-module lemma in Gabriel's boundary argument.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.leftMiddleIsoSocleQuotient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (F : S.InjectiveNonprojectiveD4Fork) : (S.minimalLeftAlmostSplitAt ↑F.center).middle ≅ moduleSocleQuotientFGObj (S.fgObj ↑F.center)

The chosen minimal left almost-split middle term out of the injective center of a boundary fork is its canonical socle quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.leftMiddleIsoSocleQuotient_hom {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) : CategoryTheory.CategoryStruct.comp (S.minimalLeftAlmostSplitAt ↑F.center).map (leftMiddleIsoSocleQuotient S F).hom = moduleSocleQuotientProjection (S.fgObj ↑F.center)

The comparison isomorphism intertwines the chosen minimal left almost-split map with the canonical socle-quotient projection.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.outgoingSocleFactor {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) : moduleSocleQuotientFGObj (S.fgObj ↑F.center) ⟶ S.fgObj ↑(F.target j)

The factor of a fork arm through the canonical quotient by the injective center's socle.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.projection_comp_outgoingSocleFactor {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.CategoryStruct.comp (moduleSocleQuotientProjection (S.fgObj ↑F.center)) (outgoingSocleFactor S F j) = outgoingMap S F j

Factoring a fork arm through the socle quotient recovers that arm.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.outgoingSocleFactor_isSplitEpi {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.IsSplitEpi (outgoingSocleFactor S F j)

The factor of an irreducible fork arm through the socle quotient is a split epimorphism.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.minimalLeftMiddleDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : CategoryTheory.FiniteIndecomposableDecomposition (S.minimalLeftAlmostSplitAt i).middle

The displayed decomposition of the chosen minimal left almost-split middle term, reindexed by a finite ordinal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmOccurrence {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.StandardFormOccurrence ↑(F.target j) ↑F.center

The finite right-mesh occurrence represented by a fork arm.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmIndex {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 (FiniteTauMatrix.rightMiddleArity S.finiteTauCategoryData.toFiniteRightTauCategoryData ↑(F.target j))

The underlying middle index of a fork arm.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmLabel {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) : FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑(F.target j)) (rightArmIndex S F j) = ↑F.center

The selected middle occurrence has the center label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmMiddleObj_eq_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.finiteTauCategoryData.obj (FiniteTauMatrix.rightMiddleLabel S.finiteTauCategoryData.toFiniteRightTauCategoryData (↑(F.target j)) (rightArmIndex S F j)) = S.fgObj ↑F.center

The selected finite-tau middle object is the skeletal center object.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.targetNonprojectiveVertex {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) : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }

A fork target, viewed as a nonprojective standard-form vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.standardFormTau_target {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.standardFormTau (targetNonprojectiveVertex S F j) = translatedTarget S F j

The standard-form translate of a fork target is its translated target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSourceObj_eq_tauPlus {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.fgObj (translatedTarget S F j) = S.finiteTauCategoryData.obj (S.finiteTauCategoryData.tauPlus (S.standardFormFiniteTauNonprojective (targetNonprojectiveVertex S F j)))

The skeletal translated target is the finite-tau source object of the right mesh ending at the fork target.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmComplement {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) : FinitelyGeneratedCategory A

The direct sum of all right-mesh occurrences except the selected fork arm.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmMiddleSplitIso {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.finiteTauCategoryData.rightMesh (S.fgObj ↑(F.target j))).X₂ ≅ rightArmComplement S F j ⊞ S.fgObj ↑F.center

Split the selected injective-center occurrence from its right almost-split middle term.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource {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.fgObj (translatedTarget S F j) ⟶ rightArmComplement S F j ⊞ S.fgObj ↑F.center

The right-mesh source after splitting off the selected arm.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSink {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) : rightArmComplement S F j ⊞ S.fgObj ↑F.center ⟶ S.fgObj ↑(F.target j)

The right-mesh sink after splitting off the selected arm.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmMiddleSplitIso_inr_inv {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.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (rightArmMiddleSplitIso S F j).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (FiniteTauMatrix.rightMiddleInclusion S.finiteTauCategoryData (↑(F.target j)) (rightArmIndex S F j))

The selected right component of the split mesh is the fork arm.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmMiddleSplitIso_hom_snd {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.CategoryStruct.comp (rightArmMiddleSplitIso S F j).hom CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp (FiniteTauMatrix.rightMiddleProjection S.finiteTauCategoryData (↑(F.target j)) (rightArmIndex S F j)) (CategoryTheory.eqToHom ⋯)

Projection to the selected arm after splitting is the old middle projection followed by the label identification.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSink_inr {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.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (rightArmSink S F j) = outgoingMap S F j

The selected right component of the split mesh is the fork arm.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_snd {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.CategoryStruct.comp (rightArmSource S F j) CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (FiniteTauMatrix.rightMiddleSourceComponent S.finiteTauCategoryData (S.standardFormFiniteTauNonprojective (targetNonprojectiveVertex S F j)) (rightArmIndex S F j)) (CategoryTheory.eqToHom ⋯))

The selected component of the split source is the finite-tau source component, up to the displayed source and center identifications.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_snd_irreducible {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) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp (rightArmSource S F j) CategoryTheory.Limits.biprod.snd)

The selected left component of the split mesh is irreducible.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_comp_sink {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.CategoryStruct.comp (rightArmSource S F j) (rightArmSink S F j) = 0

The split right-mesh source and sink have zero composite.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_comp_sink_assoc {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) {Z : FinitelyGeneratedCategory A} (h : S.fgObj ↑(F.target j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (rightArmSource S F j) (CategoryTheory.CategoryStruct.comp (rightArmSink S F j) h) = CategoryTheory.CategoryStruct.comp 0 h

The split right-mesh source and sink have zero composite.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_mono {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.Mono (rightArmSource S F j)

The split right-mesh source remains monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_isLeftAlmostSplit {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) : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit (rightArmSource S F j)

The split right-mesh source remains left almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_isLeftMinimal {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) : QuotientSubmoduleEquidistribution.IsLeftMinimal (rightArmSource S F j)

The split right-mesh source remains left minimal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSink_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 (rightArmSink S F j)

The split right-mesh sink remains epic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_factors_of_comp_sink_eq_zero {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) {X : FinitelyGeneratedCategory A} (q : X ⟶ rightArmComplement S F j ⊞ S.fgObj ↑F.center) (hq : CategoryTheory.CategoryStruct.comp q (rightArmSink S F j) = 0) : ∃ (t : X ⟶ S.fgObj (translatedTarget S F j)), CategoryTheory.CategoryStruct.comp t (rightArmSource S F j) = q

The split right-mesh source retains the weak-kernel factorization property.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArm_functionExact {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) : Function.Exact ⇑(ModuleCat.Hom.hom (rightArmSource S F j).hom) ⇑(ModuleCat.Hom.hom (rightArmSink S F j).hom)

Exactness of the split right mesh on underlying module elements.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_fst_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 (CategoryTheory.CategoryStruct.comp (rightArmSource S F j) CategoryTheory.Limits.biprod.fst)

Exactness and epicity of the selected outgoing arm force the complementary source component to be epic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmSource_fst_irreducible {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) (hC : ¬CategoryTheory.Limits.IsZero (rightArmComplement S F j)) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (CategoryTheory.CategoryStruct.comp (rightArmSource S F j) CategoryTheory.Limits.biprod.fst)

If the complementary middle object is nonzero, its source component is irreducible.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArm_component_relation {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.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (rightArmSource S F j) CategoryTheory.Limits.biprod.fst) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (rightArmSink S F j)) + CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (rightArmSource S F j) CategoryTheory.Limits.biprod.snd) (outgoingMap S F j) = 0

The two split components of the right-mesh relation.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmComplementaryKernelObj {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) : FinitelyGeneratedCategory A

The literal kernel of the complementary source component.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmComplementaryKernelInclusion {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) : rightArmComplementaryKernelObj S F j ⟶ S.fgObj (translatedTarget S F j)

The literal complementary-kernel submodule inclusion.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmComplementaryKernelInclusion_comp {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.CategoryStruct.comp (rightArmComplementaryKernelInclusion S F j) (CategoryTheory.CategoryStruct.comp (rightArmSource S F j) CategoryTheory.Limits.biprod.fst) = 0

The complementary-kernel inclusion is killed by the complementary source component.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.rightArmComplementaryKernelInclusion_comp_assoc {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) {Z : FinitelyGeneratedCategory A} (h : rightArmComplement S F j ⟶ Z) : CategoryTheory.CategoryStruct.comp (rightArmComplementaryKernelInclusion S F j) (CategoryTheory.CategoryStruct.comp (rightArmSource S F j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h)) = CategoryTheory.CategoryStruct.comp 0 h

The complementary-kernel inclusion is killed by the complementary source component.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.complementaryKernelToSocleFactorKernel {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) : rightArmComplementaryKernelObj S F j ⟶ CategoryTheory.Limits.kernel (outgoingSocleFactor S F j)

Exactness sends the kernel of the complementary source component to the kernel left after splitting the chosen arm off the socle quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.complementaryKernelToSocleFactorKernel_comp_ι {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.CategoryStruct.comp (complementaryKernelToSocleFactorKernel S F j) (CategoryTheory.Limits.kernel.ι (outgoingSocleFactor S F j)) = CategoryTheory.CategoryStruct.comp (rightArmComplementaryKernelInclusion S F j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (rightArmSource S F j) CategoryTheory.Limits.biprod.snd) (moduleSocleQuotientProjection (S.fgObj ↑F.center)))

The kernel lift is characterized by its composite with the canonical kernel inclusion.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.complementaryKernelToSocleFactorKernel_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 (complementaryKernelToSocleFactorKernel S F j)

The exact right mesh makes the complementary-kernel map onto the remaining socle-quotient kernel surjective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.complementaryKernel_simpleTop_of_projective {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) (hp : CategoryTheory.Projective (S.fgObj (translatedTarget S F j))) : IsSimpleModule Aᵐᵒᵖ (↑(rightArmComplementaryKernelObj S F j) ⧸ Module.jacobson Aᵐᵒᵖ ↑(rightArmComplementaryKernelObj S F j))

If the translated arm is projective, the kernel of the complementary source component has simple top. For a zero complement it is the whole projective; for a nonzero complement it is the simple kernel of an irreducible epimorphism.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.leftMiddleOccurrence {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.minimalLeftAlmostSplitAt ↑F.center).index.obj

The three fork arms inject into the summand occurrences of the chosen minimal left almost-split middle term.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.leftMiddleOccurrence_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 (leftMiddleOccurrence S F)

Distinct fork arms give distinct summand occurrences.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.three_le_leftMiddle_card {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) : 3 ≤ Fintype.card (S.minimalLeftAlmostSplitAt ↑F.center).index.obj

The chosen minimal left almost-split middle term out of the fork center has at least three indecomposable summand occurrences.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.socleQuotient_not_indecomposable {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) : ¬CategoryTheory.Indecomposable (moduleSocleQuotientFGObj (S.fgObj ↑F.center))

The socle quotient of the injective center of a D4 boundary fork is not indecomposable. This is the only decomposition consequence of the fork needed in Gabriel's local argument.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.outgoingSocleFactorKernelSplitIso {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) : moduleSocleQuotientFGObj (S.fgObj ↑F.center) ≅ CategoryTheory.Limits.kernel (outgoingSocleFactor S F j) ⊞ S.fgObj ↑(F.target j)

A split fork-arm factor displays the socle quotient as the direct sum of its kernel and the arm target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.two_le_outgoingSocleFactorKernel_n {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) (dK : CategoryTheory.FiniteIndecomposableDecomposition (CategoryTheory.Limits.kernel (outgoingSocleFactor S F j))) : 2 ≤ dK.n

Removing any one fork arm leaves at least two indecomposable occurrences in the kernel of the corresponding split factor from the socle quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.outgoingSocleFactorKernel_nonzero_and_not_indecomposable {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.Limits.IsZero (CategoryTheory.Limits.kernel (outgoingSocleFactor S F j)) ∧ ¬CategoryTheory.Indecomposable (CategoryTheory.Limits.kernel (outgoingSocleFactor S F j))

The kernel left after splitting off one fork arm is nonzero and is not indecomposable: it contains at least the other two indecomposable occurrences.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.InjectiveNonprojectiveD4Fork.translatedTarget_not_projective {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.Projective (S.fgObj (translatedTarget S F j))

No translated arm of an injective D4 boundary fork can be projective. The complementary kernel would otherwise be a simple-top source surjecting onto an object with at least two indecomposable occurrences.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.not_nonempty_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) : ¬Nonempty S.InjectiveNonprojectiveD4Fork

A right beta bound of two excludes the injective D4 boundary fork.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.leftBeta_le_two_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) : S.leftBeta ≤ 2

Gabriel's direct comparison: the right beta bound ≤ 2 forces the opposite (left) beta bound ≤ 2.