An abstract almost-split interface for the forward cofinite-two criterion #
This file isolates the Auslander--Reiten input needed for the forward half of the manuscript's mixed cofinite-two criterion. It proves the usual correspondence between the indecomposable summands of a minimal almost-split middle term and irreducible morphisms. It also proves that a supplied finite-length almost-split map can be replaced by a minimal one. Existence of ordinary almost-split maps is still left as a separate input.
A morphism f : E ⟶ Z is right almost split when it is not a split
epimorphism and every morphism into Z which is not a split epimorphism
factors through it.
Here "non-split epimorphism" is used in the standard AR sense of a morphism which is not a retraction; the morphism being factored need not itself be categorically epic.
- not_isSplitEpi : ¬CategoryTheory.IsSplitEpi f
- factors {X : C} (g : X ⟶ Z) : ¬CategoryTheory.IsSplitEpi g → ∃ (h : X ⟶ E), CategoryTheory.CategoryStruct.comp h f = g
Instances For
The dual notion of a left almost-split morphism.
- not_isSplitMono : ¬CategoryTheory.IsSplitMono f
- factors {X : C} (g : Z ⟶ X) : ¬CategoryTheory.IsSplitMono g → ∃ (h : E ⟶ X), CategoryTheory.CategoryStruct.comp f h = g
Instances For
Existence of an irreducible morphism between two objects.
Instances For
The no-loop input used for an almost-split middle term: there is no
irreducible endomorphism of X.
Instances For
A finite-length finitely generated module has no irreducible endomorphism.
The canonical epi--mono image factorization of a hypothetical irreducible endomorphism would make one factor split. The split factor is then an isomorphism, making the original endomorphism monic or epic; finite length makes it an isomorphism, contradicting irreducibility.
A right almost-split map is epic as soon as its target admits one categorically epic map which is not split.
Dually, a left almost-split map is monic as soon as its source admits one categorical monomorphism which is not split.
Each chosen skeleton representative has no irreducible endomorphism. Only its recorded finite length is needed.
To prove that a map into a chosen indecomposable is right almost split, it suffices to establish the factorization property on the chosen indecomposable representatives. The skeleton decomposition then handles an arbitrary source one component at a time.
The left-dual reduction: factorization on the chosen indecomposable representatives implies the full left almost-split property.
A split monomorphism between chosen indecomposables is also split epic. The splitting exhibits the source as a retract of the target, so the duplicate-free skeleton identifies their labels; finite length then upgrades the resulting monic endomorphism to an isomorphism.
Dually, a split epimorphism between chosen indecomposables is also split monic.
A chosen finite indecomposable decomposition of the middle object of a
minimal right almost-split map ending at σ.obj z.
- middle : FGModuleCat R
- finiteLength : IsFiniteLength R ↑self.middle
- rightAlmostSplit : IsRightAlmostSplit self.map
- rightMinimal : IsRightMinimal self.map
- index : FintypeCat
- label : self.index.obj → ι
Instances For
A chosen finite indecomposable decomposition of the middle object of a
minimal left almost-split map starting at σ.obj z.
- middle : FGModuleCat R
- finiteLength : IsFiniteLength R ↑self.middle
- leftAlmostSplit : IsLeftAlmostSplit self.map
- leftMinimal : IsLeftMinimal self.map
- index : FintypeCat
- label : self.index.obj → ι
Instances For
Bundle any supplied minimal right almost-split map with a decomposition provided by the existing skeleton.
Instances For
Any right almost-split morphism with finite-length middle term can be replaced by a minimal one. Choose an almost-split middle term of least finite length; if an endomorphism fixing its map were noninvertible, its categorical image would give a strictly shorter right almost-split middle term.
Bundle any supplied minimal left almost-split map with a decomposition provided by the existing skeleton.
Instances For
Any left almost-split morphism with finite-length middle term can be
replaced by a minimal one. This is the dual least-length image argument to
exists_of_rightAlmostSplit_of_finiteLength.
A legal mixed quotient-side two-point deletion: p is top
split-projective, z is not, the labels are distinct, and their complement
is quotient-closed.
- ne : p ≠ z
- projective : σ.IsRelativeSplitProjective Set.univ p
- not_projective : ¬σ.IsRelativeSplitProjective Set.univ z
- closed : σ.qClosure.IsClosed {p, z}ᶜ
Instances For
The dual notion of a legal mixed submodule-side deletion.
- ne : z ≠ i
- not_injective : ¬σ.IsRelativeSplitInjective Set.univ z
- injective : σ.IsRelativeSplitInjective Set.univ i
- closed : σ.sClosure.IsClosed {z, i}ᶜ
Instances For
The existence-level AR correspondence for a chosen right almost-split middle decomposition: a label occurs in the middle exactly when there is an irreducible map from that indecomposable to the end term.
Instances For
The dual existence-level AR correspondence for a chosen left almost-split middle decomposition.
Instances For
The indecomposable summands of a minimal right almost-split middle term are exactly the sources of irreducible morphisms to its endpoint.
For an occurring summand, right minimality is applied to the rank-one perturbation which replaces that coordinate by a supplied factorization. Conversely, right almost-splitness factors an irreducible morphism through the middle; irreducibility makes the first factor split monic, and retract support detects the corresponding label.
Coordinate-free form of the right almost-split summand correspondence: an indecomposable is a retract of the middle term exactly when it is the source of an irreducible morphism to the endpoint.
Non-top-projectivity of the end term supplies the nonsplit epimorphism needed to show that a right almost-split map is categorically epic.
The indecomposable summands of a minimal left almost-split middle term are exactly the targets of irreducible morphisms from its endpoint.
Non-top-injectivity of the start term supplies the nonsplit monomorphism needed to show that a left almost-split map is categorically monic.
Core quotient-side forcing lemma. For a legal mixed deletion, if the
end label z does not occur in the chosen right almost-split middle, then
the deleted projective label p must occur there.
Minimality is recorded in A; this elementary forcing step uses only its
right almost-split field.
Core dual forcing lemma.
With the standard existence-level AR correspondence and the finite-length no-loop theorem above, a legal mixed quotient deletion forces the projective label to occur in the minimal right almost-split middle.
Dual middle-term forcing theorem under the left AR correspondence and the finite-length no-loop theorem.
Forward quotient criterion with target-absence stated directly. This separates the elementary closure argument from the later no-loop input.
Dual forward criterion with start-label absence stated directly.
Forward mixed quotient criterion for a minimal right almost-split map.
Finite length excludes z from the middle; closedness then forces p into
the middle, and the proved correspondence produces an irreducible map
p ⟶ z.
Dual forward mixed criterion for a minimal left almost-split map.
A minimal right almost-split decomposition and the elementary converse give the full mixed criterion.
Dual full mixed criterion under a minimal left almost-split decomposition.