Finite correction of ordinary-arrow representatives #
Skowroński--Waschbüsch construct special-biserial representatives by successively changing an arrow by a radical-square term. Each change retains every two-arrow composite which was already zero and makes at least one additional composite zero. This file makes the finite termination argument literal.
The remaining algebraic input is consequently local: whenever one of the two continuation bounds fails, produce one such zero-preserving correction. No induction or global compatibility is left in that input.
@[instance_reducible]
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryAdaptedQuiver
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
:
Quiver S.ProjectiveLabel
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryAdaptedArrowFintype
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(x y : S.ProjectiveLabel)
:
Fintype (x ⟶ y)
Instances For
@[reducible, inline]
abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryTwoStep
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
:
Type u
A composable pair of ordinary arrows, retaining its three vertices.
Instances For
@[reducible, inline]
abbrev
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowTotal
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
:
Type u
An ordinary arrow together with its source and target.
Instances For
@[instance_reducible]
noncomputable instance
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ordinaryTwoStepFintype
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
:
Fintype S.OrdinaryTwoStep
structure
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightContinuationFork
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
:
Type u
A literal failure witness for the right-continuation bound: two distinct arrows follow the same arrow with nonzero composites.
- startVertex : S.ProjectiveLabel
- middleVertex : S.ProjectiveLabel
- first : S.OrdinaryArrow self.startVertex self.middleVertex
- following₁ : { b : Quiver.Star self.middleVertex // CategoryTheory.CategoryStruct.comp (D.hom b.snd) (D.hom self.first) ≠ 0 }
- following₂ : { b : Quiver.Star self.middleVertex // CategoryTheory.CategoryStruct.comp (D.hom b.snd) (D.hom self.first) ≠ 0 }
- distinct : self.following₁ ≠ self.following₂
Instances For
structure
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftContinuationFork
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
:
Type u
A literal failure witness for the left-continuation bound: two distinct arrows precede the same arrow with nonzero composites.
- middleVertex : S.ProjectiveLabel
- targetVertex : S.ProjectiveLabel
- second : S.OrdinaryArrow self.middleVertex self.targetVertex
- preceding₁ : { c : Quiver.Costar self.middleVertex // CategoryTheory.CategoryStruct.comp (D.hom self.second) (D.hom c.snd) ≠ 0 }
- preceding₂ : { c : Quiver.Costar self.middleVertex // CategoryTheory.CategoryStruct.comp (D.hom self.second) (D.hom c.snd) ≠ 0 }
- distinct : self.preceding₁ ≠ self.preceding₂
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.arrowCorrectionSpace
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(a : S.OrdinaryArrowTotal)
:
Submodule k (S.ordinaryProjectiveObj a.snd.fst ⟶ S.ordinaryProjectiveObj a.fst)
The radical-square correction space belonging to a total ordinary arrow.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturbationAt
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(a : S.OrdinaryArrowTotal)
(r : ↥(arrowCorrectionSpace a))
{x y : S.ProjectiveLabel}
:
S.OrdinaryArrow x y → ↥(S.projectiveRadicalSquareSubmodule x y)
The radical-square perturbation supported at one total ordinary arrow.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturbAt
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
:
Change exactly one arrow representative by the supplied radical-square term.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.domainCorrection
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(x : S.ordinaryProjectiveObj a.snd.fst ⟶ S.ordinaryProjectiveObj a.snd.fst)
(hx :
x ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj a.snd.fst) (S.ordinaryProjectiveObj a.snd.fst))
:
↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst)
The radical-square correction -(x ≫ a) obtained from a radical
endomorphism of the domain of the arrow representative a.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.codomainCorrection
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(y : S.ordinaryProjectiveObj a.fst ⟶ S.ordinaryProjectiveObj a.fst)
(hy : y ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj a.fst) (S.ordinaryProjectiveObj a.fst))
:
↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst)
The radical-square correction -(a ≫ y) obtained from a radical
endomorphism of the codomain of the arrow representative a.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturbationAt_self
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
:
perturbationAt a r a.snd.snd = r
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturbAt_hom_self
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
:
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturbationAt_eq_zero_of_ne
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
{x y : S.ProjectiveLabel}
(b : S.OrdinaryArrow x y)
(hba : ⟨x, ⟨y, b⟩⟩ ≠ a)
:
perturbationAt a r b = 0
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturbAt_hom_eq_of_ne
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
{x y : S.ProjectiveLabel}
(b : S.OrdinaryArrow x y)
(hba : ⟨x, ⟨y, b⟩⟩ ≠ a)
:
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.twoStepComposite
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(q : S.OrdinaryTwoStep)
:
S.ordinaryProjectiveObj q.snd.snd.fst ⟶ S.ordinaryProjectiveObj q.fst
The selected-projective composite represented by a composable pair of ordinary arrows.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.OrdinaryTwoStep.firstArrow
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(q : S.OrdinaryTwoStep)
:
The first total arrow in a two-step path.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.OrdinaryTwoStep.secondArrow
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(q : S.OrdinaryTwoStep)
:
The second total arrow in a two-step path.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.OrdinaryTwoStep.UsesArrow
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(q : S.OrdinaryTwoStep)
(a : S.OrdinaryArrowTotal)
:
A two-step path is incident to an arrow if that arrow is one of its two steps.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturbAt_twoStepComposite_eq_of_not_uses
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
(q : S.OrdinaryTwoStep)
(hq : ¬OrdinaryTwoStep.UsesArrow q a)
:
(D.perturbAt a r).twoStepComposite q = D.twoStepComposite q
Perturbing one arrow leaves every nonincident two-step composite unchanged.
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.PreservesIncidentZeros
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
:
A one-arrow perturbation preserves the zero composites incident to its support. This is the precise local obligation in the SW replacement step.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.HasTwoSidedFactorization
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
:
The changed representative factors through the old one on both sides. This is a useful sufficient condition for preserving all old two-arrow zero relations; the actual asymmetric SW replacement below needs only one side.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.NoZeroWhenFirst
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
:
No zero two-step composite has a as its first arrow.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.NoZeroWhenSecond
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
:
No zero two-step composite has a as its second arrow.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.noZeroWhenSecond_of_costar_card_le_two
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
{y z : S.ProjectiveLabel}
(a : S.OrdinaryArrow y z)
(c₁ c₂ : Quiver.Costar y)
(hc : c₁ ≠ c₂)
(h₁ : CategoryTheory.CategoryStruct.comp (D.hom a) (D.hom c₁.snd) ≠ 0)
(h₂ : CategoryTheory.CategoryStruct.comp (D.hom a) (D.hom c₂.snd) ≠ 0)
(hcard : Nat.card (Quiver.Costar y) ≤ 2)
:
D.NoZeroWhenSecond ⟨y, ⟨z, a⟩⟩
If at most two arrows end at a vertex and two distinct such arrows have
nonzero composite with a, then no arrow preceding a has zero composite.
This is the finite-degree step in the asymmetric SW correction.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.noZeroWhenFirst_of_star_card_le_two
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
{x y : S.ProjectiveLabel}
(a : S.OrdinaryArrow x y)
(b₁ b₂ : Quiver.Star y)
(hb : b₁ ≠ b₂)
(h₁ : CategoryTheory.CategoryStruct.comp (D.hom b₁.snd) (D.hom a) ≠ 0)
(h₂ : CategoryTheory.CategoryStruct.comp (D.hom b₂.snd) (D.hom a) ≠ 0)
(hcard : Nat.card (Quiver.Star y) ≤ 2)
:
D.NoZeroWhenFirst ⟨x, ⟨y, a⟩⟩
The left-right symmetric finite-degree criterion: two distinct nonzero
arrows following a exhaust a star of cardinality at most two.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_rightContinuationFork_of_not_hasRightContinuationBound
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(hbad : ¬D.HasRightContinuationBound)
:
Nonempty D.RightContinuationFork
Failure of the right-continuation bound supplies two explicit distinct nonzero continuations.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_leftContinuationFork_of_not_hasLeftContinuationBound
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(hbad : ¬D.HasLeftContinuationBound)
:
Nonempty D.LeftContinuationFork
Failure of the left-continuation bound supplies two explicit distinct nonzero predecessors.
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightContinuationFork.swap
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.RightContinuationFork)
:
Exchange the two nonzero continuations in a right fork. The local uniserial comparison chooses one of these two orderings.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightContinuationFork.changedArrow
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.RightContinuationFork)
:
The second branch of a right fork, bundled as a total arrow.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightContinuationFork.killedTwoStep
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.RightContinuationFork)
:
The nonzero two-step path which the correction will kill.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightContinuationFork.firstPredecessor
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.RightContinuationFork)
:
Quiver.Costar F.middleVertex
The original first arrow, regarded as a predecessor of the changed second branch.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightContinuationFork.killedTwoStepComposite_ne_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.RightContinuationFork)
:
D.twoStepComposite F.killedTwoStep ≠ 0
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftContinuationFork.swap
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.LeftContinuationFork)
:
Exchange the two nonzero predecessors in a left fork. This is the left-right symmetric branch choice used by the local comparison.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftContinuationFork.changedArrow
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.LeftContinuationFork)
:
The second predecessor branch of a left fork, bundled as a total arrow.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftContinuationFork.killedTwoStep
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.LeftContinuationFork)
:
The nonzero two-step path which the symmetric correction will kill.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftContinuationFork.firstFollowing
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.LeftContinuationFork)
:
Quiver.Star F.middleVertex
The original second arrow, regarded as a continuation of the changed first branch.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftContinuationFork.killedTwoStepComposite_ne_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
(F : D.LeftContinuationFork)
:
D.twoStepComposite F.killedTwoStep ≠ 0
structure
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightSWCorrectionData
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(F : D.RightContinuationFork)
:
Type u
The exact categorical local output needed on the right-handed side of the SW correction. Besides the radical corner endomorphism, it records the second nonzero predecessor which proves that no old zero relation occurs on the unprotected side.
- secondPredecessor : Quiver.Costar F.middleVertex
- secondPredecessor_ne : F.firstPredecessor ≠ self.secondPredecessor
- secondPredecessor_composite_ne : CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) (D.hom self.secondPredecessor.snd) ≠ 0
- cornerEndomorphism : S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj F.middleVertex
- cornerEndomorphism_mem_radical : self.cornerEndomorphism ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj F.middleVertex) (S.ordinaryProjectiveObj F.middleVertex)
- kills : (D.perturbAt F.changedArrow (D.codomainCorrection F.changedArrow self.cornerEndomorphism ⋯)).twoStepComposite F.killedTwoStep = 0
Instances For
structure
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftSWCorrectionData
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(F : D.LeftContinuationFork)
:
Type u
The left-right symmetric local output of the Kupisch--Nakayama step.
- secondFollowing : Quiver.Star F.middleVertex
- secondFollowing_ne : F.firstFollowing ≠ self.secondFollowing
- secondFollowing_composite_ne : CategoryTheory.CategoryStruct.comp (D.hom self.secondFollowing.snd) (D.hom (↑F.preceding₂).snd) ≠ 0
- cornerEndomorphism : S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj F.middleVertex
- cornerEndomorphism_mem_radical : self.cornerEndomorphism ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj F.middleVertex) (S.ordinaryProjectiveObj F.middleVertex)
- kills : (D.perturbAt F.changedArrow (D.domainCorrection F.changedArrow self.cornerEndomorphism ⋯)).twoStepComposite F.killedTwoStep = 0
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightSWCorrectionChoice
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(F : D.RightContinuationFork)
:
The source's right-handed local comparison may select either ordering of the two displayed continuations. Requiring data for a predetermined ordering would be stronger than uniserial comparability.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftSWCorrectionChoice
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(F : D.LeftContinuationFork)
:
The left-right symmetric choice between the two predecessor orderings.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.HasDomainFactorization
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
:
Precomposition factorization of the changed representative through the old one.
Instances For
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.HasCodomainFactorization
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
:
Postcomposition factorization of the changed representative through the old one.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.domainCorrection_hasDomainFactorization
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(x : S.ordinaryProjectiveObj a.snd.fst ⟶ S.ordinaryProjectiveObj a.snd.fst)
(hx :
x ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj a.snd.fst) (S.ordinaryProjectiveObj a.snd.fst))
:
D.HasDomainFactorization a (D.domainCorrection a x hx)
A domain correction is literally precomposition by 1 - x.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.codomainCorrection_hasCodomainFactorization
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(y : S.ordinaryProjectiveObj a.fst ⟶ S.ordinaryProjectiveObj a.fst)
(hy : y ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj a.fst) (S.ordinaryProjectiveObj a.fst))
:
D.HasCodomainFactorization a (D.codomainCorrection a y hy)
A codomain correction is literally postcomposition by 1 - y.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.preservesIncidentZeros_of_domainFactorization_of_noZeroWhenFirst
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
(hfactor : D.HasDomainFactorization a r)
(hno : D.NoZeroWhenFirst a)
:
D.PreservesIncidentZeros a r
A domain-factor replacement preserves the zero composites in which the changed arrow occurs second. If no zero composite used it first, all incident zeros are therefore preserved.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.preservesIncidentZeros_of_codomainFactorization_of_noZeroWhenSecond
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
(hfactor : D.HasCodomainFactorization a r)
(hno : D.NoZeroWhenSecond a)
:
D.PreservesIncidentZeros a r
The left-right symmetric zero-preservation criterion for a codomain factor replacement.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.domainCorrection_hasTwoSidedFactorization_of_balanced
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(x : S.ordinaryProjectiveObj a.snd.fst ⟶ S.ordinaryProjectiveObj a.snd.fst)
(y : S.ordinaryProjectiveObj a.fst ⟶ S.ordinaryProjectiveObj a.fst)
(hx :
x ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj a.snd.fst) (S.ordinaryProjectiveObj a.snd.fst))
(hbalanced :
CategoryTheory.CategoryStruct.comp x (D.hom a.snd.snd) = CategoryTheory.CategoryStruct.comp (D.hom a.snd.snd) y)
:
D.HasTwoSidedFactorization a (D.domainCorrection a x hx)
If the radical endomorphisms on the two sides satisfy x ≫ a = a ≫ y,
then the balanced correction replaces a simultaneously by
(1 - x) ≫ a and by a ≫ (1 - y).
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.preservesIncidentZeros_of_twoSidedFactorization
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
(hfactor : D.HasTwoSidedFactorization a r)
:
D.PreservesIncidentZeros a r
A two-sided factor replacement preserves every incident two-arrow zero relation, including the square of a loop arrow.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.nonzeroTwoSteps
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
:
Finset S.OrdinaryTwoStep
The finite set of two-step paths whose representative composite is nonzero.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.mem_nonzeroTwoSteps_iff
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(q : S.OrdinaryTwoStep)
:
q ∈ D.nonzeroTwoSteps ↔ D.twoStepComposite q ≠ 0
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.TwoStepZeroMonotone
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D E : OrdinaryArrowRepresentatives)
:
A change of representatives is zero-monotone on two-step paths when it does not turn any existing zero composite into a nonzero composite.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.perturbAt_twoStepZeroMonotone
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(r : ↥(S.projectiveRadicalSquareSubmodule a.fst a.snd.fst))
(hlocal : D.PreservesIncidentZeros a r)
:
D.TwoStepZeroMonotone (D.perturbAt a r)
Local preservation at the changed arrow implies global two-step zero-monotonicity.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.domainCorrection_twoStepZeroMonotone_of_noZeroWhenFirst
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(x : S.ordinaryProjectiveObj a.snd.fst ⟶ S.ordinaryProjectiveObj a.snd.fst)
(hx :
x ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj a.snd.fst) (S.ordinaryProjectiveObj a.snd.fst))
(hno : D.NoZeroWhenFirst a)
:
D.TwoStepZeroMonotone (D.perturbAt a (D.domainCorrection a x hx))
A domain correction is globally zero-monotone provided the changed arrow did not occur first in an old zero composite.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.codomainCorrection_twoStepZeroMonotone_of_noZeroWhenSecond
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(a : S.OrdinaryArrowTotal)
(y : S.ordinaryProjectiveObj a.fst ⟶ S.ordinaryProjectiveObj a.fst)
(hy : y ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj a.fst) (S.ordinaryProjectiveObj a.fst))
(hno : D.NoZeroWhenSecond a)
:
D.TwoStepZeroMonotone (D.perturbAt a (D.codomainCorrection a y hy))
A codomain correction is globally zero-monotone provided the changed arrow did not occur second in an old zero composite.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.twoStepZeroMonotone_refl
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
:
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.TwoStepZeroMonotone.trans
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D E F : OrdinaryArrowRepresentatives}
(hDE : D.TwoStepZeroMonotone E)
(hEF : E.TwoStepZeroMonotone F)
:
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.nonzeroTwoSteps_subset_of_twoStepZeroMonotone
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D E : OrdinaryArrowRepresentatives}
(hDE : D.TwoStepZeroMonotone E)
:
A zero-monotone change can only decrease the finite set of nonzero two-step composites.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.card_nonzeroTwoSteps_lt_of_twoStepZeroMonotone_of_kills
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D E : OrdinaryArrowRepresentatives}
(hDE : D.TwoStepZeroMonotone E)
(q : S.OrdinaryTwoStep)
(hDq : D.twoStepComposite q ≠ 0)
(hEq : E.twoStepComposite q = 0)
:
E.nonzeroTwoSteps.card < D.nonzeroTwoSteps.card
If a zero-monotone change kills one previously nonzero two-step composite, the total number of nonzero two-step composites strictly drops.
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.HasTwoStepCorrection
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(q : S.OrdinaryTwoStep)
:
One local SW correction: retain every existing zero two-step relation and kill the specified nonzero two-step composite.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.hasTwoStepCorrection_of_domainCorrection
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(q : S.OrdinaryTwoStep)
(a : S.OrdinaryArrowTotal)
(x : S.ordinaryProjectiveObj a.snd.fst ⟶ S.ordinaryProjectiveObj a.snd.fst)
(hx :
x ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj a.snd.fst) (S.ordinaryProjectiveObj a.snd.fst))
(hq : D.twoStepComposite q ≠ 0)
(hno : D.NoZeroWhenFirst a)
(hkill : (D.perturbAt a (D.domainCorrection a x hx)).twoStepComposite q = 0)
:
Package a successful domain correction as the local correction consumed by the finite minimization argument.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.hasTwoStepCorrection_of_codomainCorrection
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(D : OrdinaryArrowRepresentatives)
(q : S.OrdinaryTwoStep)
(a : S.OrdinaryArrowTotal)
(y : S.ordinaryProjectiveObj a.fst ⟶ S.ordinaryProjectiveObj a.fst)
(hy : y ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj a.fst) (S.ordinaryProjectiveObj a.fst))
(hq : D.twoStepComposite q ≠ 0)
(hno : D.NoZeroWhenSecond a)
(hkill : (D.perturbAt a (D.codomainCorrection a y hy)).twoStepComposite q = 0)
:
Package a successful codomain correction as the local correction consumed by the finite minimization argument.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightSWCorrectionData.hasTwoStepCorrection
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
{F : D.RightContinuationFork}
(C : D.RightSWCorrectionData F)
(hcard : Nat.card (Quiver.Costar F.middleVertex) ≤ 2)
:
The right-handed SW local data gives a zero-monotone correction once the incoming degree at the middle vertex is at most two.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftSWCorrectionData.hasTwoStepCorrection
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
{F : D.LeftContinuationFork}
(C : D.LeftSWCorrectionData F)
(hcard : Nat.card (Quiver.Star F.middleVertex) ≤ 2)
:
The left-handed SW local data gives the symmetric zero-monotone correction once the outgoing degree at the middle vertex is at most two.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_hasTwoStepCorrection_of_rightSWCorrectionChoice
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
{F : D.RightContinuationFork}
(C : D.RightSWCorrectionChoice F)
(hcard : Nat.card (Quiver.Costar F.middleVertex) ≤ 2)
:
∃ (q : S.OrdinaryTwoStep), D.HasTwoStepCorrection q
Either ordering selected by the right-handed local comparison supplies a usable correction of one of the two original nonzero paths.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_hasTwoStepCorrection_of_leftSWCorrectionChoice
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{D : OrdinaryArrowRepresentatives}
{F : D.LeftContinuationFork}
(C : D.LeftSWCorrectionChoice F)
(hcard : Nat.card (Quiver.Star F.middleVertex) ≤ 2)
:
∃ (q : S.OrdinaryTwoStep), D.HasTwoStepCorrection q
Either ordering selected by the left-handed local comparison supplies the symmetric usable correction.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_minimal_nonzeroTwoSteps
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
:
∃ (D : OrdinaryArrowRepresentatives),
∀ (E : OrdinaryArrowRepresentatives), D.nonzeroTwoSteps.card ≤ E.nonzeroTwoSteps.card
There is a representative system minimizing the finite number of nonzero two-step composites.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_adapted_of_exists_twoStepCorrection
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(hCorrection :
∀ (D : OrdinaryArrowRepresentatives),
¬(D.HasRightContinuationBound ∧ D.HasLeftContinuationBound) → ∃ (q : S.OrdinaryTwoStep), D.HasTwoStepCorrection q)
:
The source-faithful finite correction principle. Once every failure of the two continuation conditions supplies one local zero-monotone correction, a globally adapted representative system exists.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_adapted_of_swCorrectionData
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(hStar : ∀ (x : S.ProjectiveLabel), Nat.card (Quiver.Star x) ≤ 2)
(hCostar : ∀ (x : S.ProjectiveLabel), Nat.card (Quiver.Costar x) ≤ 2)
(hRight : ∀ (D : OrdinaryArrowRepresentatives) (F : D.RightContinuationFork), D.RightSWCorrectionChoice F)
(hLeft : ∀ (D : OrdinaryArrowRepresentatives) (F : D.LeftContinuationFork), D.LeftSWCorrectionChoice F)
:
The exact SW assembly theorem after separating its local Kupisch--Nakayama output from the finite correction argument.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_adapted_of_isBiserial_of_swCorrectionData
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsNoetherianRing A]
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(hP : P.IsBiserial)
(hRight : ∀ (D : OrdinaryArrowRepresentatives) (F : D.RightContinuationFork), D.RightSWCorrectionChoice F)
(hLeft : ∀ (D : OrdinaryArrowRepresentatives) (F : D.LeftContinuationFork), D.LeftSWCorrectionChoice F)
:
For a biserial primitive-projective presentation, the already proved ordinary-quiver degree bounds discharge the two finite-degree hypotheses in the SW assembly. Only the local Kupisch--Nakayama correction data remains.