The first Kupisch comparison for ordinary-quiver forks #
The two nonzero composites in a right-continuation fork lie in the principal right ideal generated by the coordinate of their common first arrow. Uniseriality compares those two elements. Projecting the resulting scalar to the appropriate primitive-idempotent corner and transporting it back through the selected-projective coordinate equivalence gives exactly one of the two factorizations used in the Skowroński--Waschbüsch correction.
@[instance_reducible]
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instQuiverProjectiveLabel
{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.instFintypeHomProjectiveLabel
{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
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.eq_of_codomainHom_uniserial
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(D : OrdinaryArrowRepresentatives)
{x y : S.ProjectiveLabel}
(huni :
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj x))
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x))
(a b : S.OrdinaryArrow x y)
:
a = b
If the Hom-space between two selected projectives is uniserial under postcomposition by endomorphisms of its codomain, then the corresponding ordinary-quiver vertices support at most one arrow. Indeed, comparability would make one arrow representative a postcomposition multiple of the other; the scalar part survives modulo the radical square while the radical part does not, contradicting linear independence of distinct arrow classes.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.eq_of_domainHom_uniserial
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(D : OrdinaryArrowRepresentatives)
{x y : S.ProjectiveLabel}
(huni :
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj y))ᵐᵒᵖ
(S.ordinaryProjectiveObj y ⟶ S.ordinaryProjectiveObj x))
(a b : S.OrdinaryArrow x y)
:
a = b
The domain-endomorphism analogue of
eq_of_codomainHom_uniserial. Uniseriality for precomposition by the
opposite endomorphism ring also forces uniqueness of an ordinary arrow
between fixed vertices.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.RightContinuationFork.followingTarget_ne_of_uniserialAlternative
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(D : OrdinaryArrowRepresentatives)
(F : D.RightContinuationFork)
(huni :
∀ (z : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))
(S.ordinaryProjectiveObj z ⟶ S.ordinaryProjectiveObj F.middleVertex) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj z))ᵐᵒᵖ
(S.ordinaryProjectiveObj z ⟶ S.ordinaryProjectiveObj F.middleVertex))
:
(↑F.following₁).fst ≠ (↑F.following₂).fst
The two continuation targets are also distinct under Kupisch's literal left-or-right uniserial alternative.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_rightFork_secondComparison
{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)
(connector : S.ordinaryProjectiveObj (↑F.following₂).fst ⟶ S.ordinaryProjectiveObj (↑F.following₁).fst)
(hconnector :
connector ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj (↑F.following₂).fst)
(S.ordinaryProjectiveObj (↑F.following₁).fst))
(huni :
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))
(S.ordinaryProjectiveObj (↑F.following₂).fst ⟶ S.ordinaryProjectiveObj F.middleVertex))
:
∃
e ∈
S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj F.middleVertex)
(S.ordinaryProjectiveObj F.middleVertex),
CategoryTheory.CategoryStruct.comp connector (D.hom (↑F.following₁).snd) = CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) e
Once the first Kupisch comparison has produced a radical connector, a second uniserial comparison produces the radical endomorphism used in the SW correction. The opposite comparison order is impossible: it would express an ordinary-arrow representative as a radical-square morphism.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.false_of_rightFork_firstComparison_of_domainHom_uniserial
{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)
(connector : S.ordinaryProjectiveObj (↑F.following₂).fst ⟶ S.ordinaryProjectiveObj (↑F.following₁).fst)
(hconnector :
connector ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj (↑F.following₂).fst)
(S.ordinaryProjectiveObj (↑F.following₁).fst))
(hfirst :
CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) (D.hom F.first) = CategoryTheory.CategoryStruct.comp connector
(CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₁).snd) (D.hom F.first)))
(huni :
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj (↑F.following₂).fst))ᵐᵒᵖ
(S.ordinaryProjectiveObj (↑F.following₂).fst ⟶ S.ordinaryProjectiveObj F.middleVertex))
:
False
The domain-uniserial alternative in Kupisch condition (K)(2) is incompatible with the already obtained first comparison. Comparability would either put an ordinary arrow in the radical square, or make the original nonzero two-arrow composite fixed by a radical endomorphism. The latter is impossible because one minus a nilpotent is invertible.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_rightFork_secondComparison_of_uniserialAlternative
{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)
(connector : S.ordinaryProjectiveObj (↑F.following₂).fst ⟶ S.ordinaryProjectiveObj (↑F.following₁).fst)
(hconnector :
connector ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj (↑F.following₂).fst)
(S.ordinaryProjectiveObj (↑F.following₁).fst))
(hfirst :
CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) (D.hom F.first) = CategoryTheory.CategoryStruct.comp connector
(CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₁).snd) (D.hom F.first)))
(huni :
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))
(S.ordinaryProjectiveObj (↑F.following₂).fst ⟶ S.ordinaryProjectiveObj F.middleVertex) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj (↑F.following₂).fst))ᵐᵒᵖ
(S.ordinaryProjectiveObj (↑F.following₂).fst ⟶ S.ordinaryProjectiveObj F.middleVertex))
:
∃
e ∈
S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj F.middleVertex)
(S.ordinaryProjectiveObj F.middleVertex),
CategoryTheory.CategoryStruct.comp connector (D.hom (↑F.following₁).snd) = CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) e
Kupisch's literal left-or-right alternative gives the radical corner comparison: the codomain-uniserial branch constructs it, while the domain-uniserial branch is excluded by the first comparison and nilpotence.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.LeftContinuationFork.precedingSource_ne_of_uniserialAlternative
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(D : OrdinaryArrowRepresentatives)
(F : D.LeftContinuationFork)
(huni :
∀ (z : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj z))
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj z) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))ᵐᵒᵖ
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj z))
:
(↑F.preceding₁).fst ≠ (↑F.preceding₂).fst
The two predecessor sources in a left fork are distinct under Kupisch's literal left-or-right uniserial alternative.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_leftFork_secondComparison
{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)
(connector : S.ordinaryProjectiveObj (↑F.preceding₁).fst ⟶ S.ordinaryProjectiveObj (↑F.preceding₂).fst)
(hconnector :
connector ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj (↑F.preceding₁).fst)
(S.ordinaryProjectiveObj (↑F.preceding₂).fst))
(huni :
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))ᵐᵒᵖ
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj (↑F.preceding₂).fst))
:
∃
e ∈
S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj F.middleVertex)
(S.ordinaryProjectiveObj F.middleVertex),
CategoryTheory.CategoryStruct.comp (D.hom (↑F.preceding₁).snd) connector = CategoryTheory.CategoryStruct.comp e (D.hom (↑F.preceding₂).snd)
Once the first left Kupisch comparison has produced a radical connector, domain-Hom uniseriality produces the radical middle endomorphism used in the symmetric SW correction.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.false_of_leftFork_firstComparison_of_codomainHom_uniserial
{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)
(connector : S.ordinaryProjectiveObj (↑F.preceding₁).fst ⟶ S.ordinaryProjectiveObj (↑F.preceding₂).fst)
(hconnector :
connector ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj (↑F.preceding₁).fst)
(S.ordinaryProjectiveObj (↑F.preceding₂).fst))
(hfirst :
CategoryTheory.CategoryStruct.comp (D.hom F.second) (D.hom (↑F.preceding₂).snd) = CategoryTheory.CategoryStruct.comp (D.hom F.second)
(CategoryTheory.CategoryStruct.comp (D.hom (↑F.preceding₁).snd) connector))
(huni :
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj (↑F.preceding₂).fst))
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj (↑F.preceding₂).fst))
:
False
The codomain-uniserial alternative in Kupisch condition (K)(2) is incompatible with an already obtained first left comparison.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_leftFork_secondComparison_of_uniserialAlternative
{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)
(connector : S.ordinaryProjectiveObj (↑F.preceding₁).fst ⟶ S.ordinaryProjectiveObj (↑F.preceding₂).fst)
(hconnector :
connector ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj (↑F.preceding₁).fst)
(S.ordinaryProjectiveObj (↑F.preceding₂).fst))
(hfirst :
CategoryTheory.CategoryStruct.comp (D.hom F.second) (D.hom (↑F.preceding₂).snd) = CategoryTheory.CategoryStruct.comp (D.hom F.second)
(CategoryTheory.CategoryStruct.comp (D.hom (↑F.preceding₁).snd) connector))
(huni :
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj (↑F.preceding₂).fst))
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj (↑F.preceding₂).fst) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))ᵐᵒᵖ
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj (↑F.preceding₂).fst))
:
∃
e ∈
S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj F.middleVertex)
(S.ordinaryProjectiveObj F.middleVertex),
CategoryTheory.CategoryStruct.comp (D.hom (↑F.preceding₁).snd) connector = CategoryTheory.CategoryStruct.comp e (D.hom (↑F.preceding₂).snd)
Kupisch's literal alternative gives the radical middle endomorphism for the left correction: the domain branch constructs it, while the codomain branch is excluded by the first comparison and nilpotence.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_eq_outgoing_sum_of_mem_projectiveRadical
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(D : OrdinaryArrowRepresentatives)
(x : S.ProjectiveLabel)
(e : S.ordinaryProjectiveObj x ⟶ S.ordinaryProjectiveObj x)
(he : e ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj x) (S.ordinaryProjectiveObj x))
:
∃ (h : (a : Quiver.Costar x) → S.ordinaryProjectiveObj a.fst ⟶ S.ordinaryProjectiveObj x),
e = ∑ a : Quiver.Costar x, CategoryTheory.CategoryStruct.comp (D.hom a.snd) (h a)
Every radical endomorphism of a selected projective is a finite sum of maps which first follow an ordinary arrow out of that projective. Fullness gives a free-path preimage; the only possible length-zero term is a scalar identity, and nilpotence of the projective radical forces that scalar to vanish.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.OrdinaryArrowRepresentatives.exists_eq_incoming_sum_of_mem_projectiveRadical
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(D : OrdinaryArrowRepresentatives)
(x : S.ProjectiveLabel)
(e : S.ordinaryProjectiveObj x ⟶ S.ordinaryProjectiveObj x)
(he : e ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj x) (S.ordinaryProjectiveObj x))
:
∃ (h : (a : Quiver.Star x) → S.ordinaryProjectiveObj x ⟶ S.ordinaryProjectiveObj a.fst),
e = ∑ a : Quiver.Star x, CategoryTheory.CategoryStruct.comp (h a) (D.hom a.snd)
Dually, every radical endomorphism of a selected projective is a finite sum of maps which end with an ordinary arrow into that projective.
structure
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.RightKupischComparisonData
{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 two source-faithful Kupisch comparisons attached to one chosen ordering of a right fork. This is the algebraic core of the local SW correction, before extracting the second incoming arrow required by the zero-monotonicity argument.
- connector : S.ordinaryProjectiveObj (↑F.following₂).fst ⟶ S.ordinaryProjectiveObj (↑F.following₁).fst
- connector_mem_radical : self.connector ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj (↑F.following₂).fst) (S.ordinaryProjectiveObj (↑F.following₁).fst)
- firstComparison : CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) (D.hom F.first) = CategoryTheory.CategoryStruct.comp self.connector (CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₁).snd) (D.hom F.first))
- 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)
- secondComparison : CategoryTheory.CategoryStruct.comp self.connector (D.hom (↑F.following₁).snd) = CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) self.cornerEndomorphism
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.RightKupischComparisonData.kills
{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 : RightKupischComparisonData D F)
:
(D.perturbAt F.changedArrow (D.codomainCorrection F.changedArrow C.cornerEndomorphism ⋯)).twoStepComposite
F.killedTwoStep = 0
The codomain correction supplied by the two Kupisch comparisons kills the selected composite. The proof also covers the loop case in which the changed continuation is itself the common first arrow, so both occurrences are perturbed.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.RightKupischComparisonData.exists_secondPredecessor
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
{D : OrdinaryArrowRepresentatives}
{F : D.RightContinuationFork}
(C : RightKupischComparisonData D F)
:
∃ (d : Quiver.Costar F.middleVertex),
F.firstPredecessor ≠ d ∧ CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) (D.hom d.snd) ≠ 0
The radical corner endomorphism in the Kupisch comparison must contain a second incoming ordinary-arrow branch on which the changed continuation is nonzero. Otherwise its outgoing-arrow decomposition would make the original nonzero composite fixed by a radical endomorphism; nilpotence then gives the Nakayama contradiction.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.RightKupischComparisonData.toRightSWCorrectionData
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
{D : OrdinaryArrowRepresentatives}
{F : D.RightContinuationFork}
(C : RightKupischComparisonData D F)
:
Package the extracted predecessor and the already proved correction as the exact local datum consumed by the finite SW minimization.
Instances For
structure
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.LeftKupischComparisonData
{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 two source-faithful Kupisch comparisons attached to one chosen ordering of a left fork.
- connector : S.ordinaryProjectiveObj (↑F.preceding₁).fst ⟶ S.ordinaryProjectiveObj (↑F.preceding₂).fst
- connector_mem_radical : self.connector ∈ S.projectiveNilpotentRadicalData.ideal.hom (S.ordinaryProjectiveObj (↑F.preceding₁).fst) (S.ordinaryProjectiveObj (↑F.preceding₂).fst)
- firstComparison : CategoryTheory.CategoryStruct.comp (D.hom F.second) (D.hom (↑F.preceding₂).snd) = CategoryTheory.CategoryStruct.comp (D.hom F.second) (CategoryTheory.CategoryStruct.comp (D.hom (↑F.preceding₁).snd) self.connector)
- 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)
- secondComparison : CategoryTheory.CategoryStruct.comp (D.hom (↑F.preceding₁).snd) self.connector = CategoryTheory.CategoryStruct.comp self.cornerEndomorphism (D.hom (↑F.preceding₂).snd)
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.LeftKupischComparisonData.kills
{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 : LeftKupischComparisonData D F)
:
(D.perturbAt F.changedArrow (D.domainCorrection F.changedArrow C.cornerEndomorphism ⋯)).twoStepComposite
F.killedTwoStep = 0
The domain correction supplied by the two left Kupisch comparisons kills the selected composite, including the possible loop case.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.LeftKupischComparisonData.exists_secondFollowing
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
{D : OrdinaryArrowRepresentatives}
{F : D.LeftContinuationFork}
(C : LeftKupischComparisonData D F)
:
∃ (d : Quiver.Star F.middleVertex),
F.firstFollowing ≠ d ∧ CategoryTheory.CategoryStruct.comp (D.hom d.snd) (D.hom (↑F.preceding₂).snd) ≠ 0
The radical middle endomorphism in a left Kupisch comparison contains a second outgoing branch on which the changed predecessor is nonzero.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.LeftKupischComparisonData.toLeftSWCorrectionData
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
{D : OrdinaryArrowRepresentatives}
{F : D.LeftContinuationFork}
(C : LeftKupischComparisonData D F)
:
Package the left comparison and extracted following arrow as the exact local datum consumed by finite minimization.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.compositeInArrowRightIdeal
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
{x y z : S.ProjectiveLabel}
(a : S.OrdinaryArrow x y)
(b : S.OrdinaryArrow y z)
:
↥(rightIdeal (P.projectiveHomCoordinate (D.hom a)))
A two-arrow composite, bundled in the principal right ideal generated by the coordinate of its first arrow.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.compositeInArrowRightIdeal_coe
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
{x y z : S.ProjectiveLabel}
(a : S.OrdinaryArrow x y)
(b : S.OrdinaryArrow y z)
:
↑(P.compositeInArrowRightIdeal D a b) = P.projectiveHomCoordinate (CategoryTheory.CategoryStruct.comp (D.hom b) (D.hom a))
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_rightFork_firstComparison
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
(F : D.RightContinuationFork)
(huni : IsUniserialModule Aᵐᵒᵖ ↥(rightIdeal (P.projectiveHomCoordinate (D.hom F.first))))
:
(∃ (connector : S.ordinaryProjectiveObj (↑F.following₂).fst ⟶ S.ordinaryProjectiveObj (↑F.following₁).fst),
CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) (D.hom F.first) = CategoryTheory.CategoryStruct.comp connector
(CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₁).snd) (D.hom F.first))) ∨ ∃ (connector : S.ordinaryProjectiveObj (↑F.following₁).fst ⟶ S.ordinaryProjectiveObj (↑F.following₂).fst),
CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₁).snd) (D.hom F.first) = CategoryTheory.CategoryStruct.comp connector
(CategoryTheory.CategoryStruct.comp (D.hom (↑F.following₂).snd) (D.hom F.first))
Uniseriality of the principal right ideal generated by the common first arrow compares the two nonzero composites in one of the two source-faithful orders and converts the scalar into a corner-supported projective connector.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_rightKupischComparisonChoice
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
(F : D.RightContinuationFork)
(hprincipal : IsUniserialModule Aᵐᵒᵖ ↥(rightIdeal (P.projectiveHomCoordinate (D.hom F.first))))
(hcorner :
∀ (z : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))
(S.ordinaryProjectiveObj z ⟶ S.ordinaryProjectiveObj F.middleVertex) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj z))ᵐᵒᵖ
(S.ordinaryProjectiveObj z ⟶ S.ordinaryProjectiveObj F.middleVertex))
:
Nonempty (RightKupischComparisonData D F) ∨ Nonempty (RightKupischComparisonData D F.swap)
Under Kupisch's literal codomain-or-domain uniserial alternative, the two successive comparisons produce complete comparison data for one of the two orderings of the fork. The domain-uniserial branch is ruled out by nilpotence. The disjunction records the order selected by uniseriality rather than imposing a stronger predetermined orientation.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_rightSWCorrectionChoice
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
(F : D.RightContinuationFork)
(hprincipal : IsUniserialModule Aᵐᵒᵖ ↥(rightIdeal (P.projectiveHomCoordinate (D.hom F.first))))
(hcorner :
∀ (z : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))
(S.ordinaryProjectiveObj z ⟶ S.ordinaryProjectiveObj F.middleVertex) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj z))ᵐᵒᵖ
(S.ordinaryProjectiveObj z ⟶ S.ordinaryProjectiveObj F.middleVertex))
:
Kupisch's uniserial alternative supplies the exact unordered right-hand correction choice consumed by the finite adapted-representative construction.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.compositeInArrowLeftIdeal
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
{x y z : S.ProjectiveLabel}
(a : S.OrdinaryArrow x y)
(b : S.OrdinaryArrow y z)
:
↥(leftIdeal (P.projectiveHomCoordinate (D.hom b)))
A two-arrow composite bundled in the principal left ideal generated by the coordinate of its second arrow.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.compositeInArrowLeftIdeal_coe
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
{x y z : S.ProjectiveLabel}
(a : S.OrdinaryArrow x y)
(b : S.OrdinaryArrow y z)
:
↑(P.compositeInArrowLeftIdeal D a b) = P.projectiveHomCoordinate (CategoryTheory.CategoryStruct.comp (D.hom b) (D.hom a))
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_leftFork_firstComparison
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
(F : D.LeftContinuationFork)
(huni : IsUniserialModule A ↥(leftIdeal (P.projectiveHomCoordinate (D.hom F.second))))
:
(∃ (connector : S.ordinaryProjectiveObj (↑F.preceding₁).fst ⟶ S.ordinaryProjectiveObj (↑F.preceding₂).fst),
CategoryTheory.CategoryStruct.comp (D.hom F.second) (D.hom (↑F.preceding₂).snd) = CategoryTheory.CategoryStruct.comp (D.hom F.second)
(CategoryTheory.CategoryStruct.comp (D.hom (↑F.preceding₁).snd) connector)) ∨ ∃ (connector : S.ordinaryProjectiveObj (↑F.preceding₂).fst ⟶ S.ordinaryProjectiveObj (↑F.preceding₁).fst),
CategoryTheory.CategoryStruct.comp (D.hom F.second) (D.hom (↑F.preceding₁).snd) = CategoryTheory.CategoryStruct.comp (D.hom F.second)
(CategoryTheory.CategoryStruct.comp (D.hom (↑F.preceding₂).snd) connector)
Uniseriality of the principal left ideal generated by the common second arrow compares the two nonzero composites and turns the selected multiplier into a corner-supported connector.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_leftKupischComparisonChoice
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
(F : D.LeftContinuationFork)
(hprincipal : IsUniserialModule A ↥(leftIdeal (P.projectiveHomCoordinate (D.hom F.second))))
(hcorner :
∀ (z : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj z))
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj z) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))ᵐᵒᵖ
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj z))
:
Nonempty (LeftKupischComparisonData D F) ∨ Nonempty (LeftKupischComparisonData D F.swap)
The principal-left-ideal comparison and Kupisch's literal Hom-bimodule alternative give complete comparison data for one ordering of a left fork.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.exists_leftSWCorrectionChoice
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
[IsAlgClosed k]
(P : S.PrimitiveProjectivePresentation)
(D : OrdinaryArrowRepresentatives)
(F : D.LeftContinuationFork)
(hprincipal : IsUniserialModule A ↥(leftIdeal (P.projectiveHomCoordinate (D.hom F.second))))
(hcorner :
∀ (z : S.ProjectiveLabel),
IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj z))
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj z) ∨ IsUniserialModule (CategoryTheory.End (S.ordinaryProjectiveObj F.middleVertex))ᵐᵒᵖ
(S.ordinaryProjectiveObj F.middleVertex ⟶ S.ordinaryProjectiveObj z))
:
Kupisch's uniserial alternative supplies the exact unordered left-hand correction choice consumed by finite adapted-representative construction.