Irreducible maps and the converse cofinite-two criterion #
This file formalizes the elementary (non-Auslander--Reiten) half of
the manuscript's mixed cofinite-two criterion. If P is projective and
there is an irreducible map P ⟶ Z, then deleting the labels of P and Z
leaves a quotient-closed support. The dual injective statement is included
as well.
The definition of irreducibility is categorical: the map itself is neither a split monomorphism nor a split epimorphism, and in every factorization the first factor is a split monomorphism or the second is a split epimorphism.
A morphism is irreducible if it is not split in either direction and every factorization has a split-monomorphic first factor or a split-epimorphic second factor.
- not_isSplitMono : ¬CategoryTheory.IsSplitMono f
- not_isSplitEpi : ¬CategoryTheory.IsSplitEpi f
- factorization {M : C} (g : X ⟶ M) (h : M ⟶ Y) : CategoryTheory.CategoryStruct.comp g h = f → CategoryTheory.IsSplitMono g ∨ CategoryTheory.IsSplitEpi h
Instances For
A categorical projective is split-projective relative to the top support in the existing explicit-presentation sense.
Conversely, top relative split-projectivity is categorical
projectivity. The pullback of an epimorphism along a map out of P gives
an epimorphism onto P; the skeleton decomposition turns its source into
one of the explicit presentations tested by the relative predicate.
Categorical projectivity and the package's top relative split-projectivity agree on the chosen indecomposable objects.
A categorical injective is split-injective relative to the top support in the existing explicit-presentation sense.
Conversely, top relative split-injectivity is categorical injectivity, by the dual pushout argument.
Categorical injectivity and top relative split-injectivity agree on the chosen indecomposable objects.
Converse half of the mixed quotient cofinite-two criterion: an irreducible map from a projective indecomposable forces the two-point complement to be quotient-closed.
The same converse criterion with the manuscript's top split-projectivity hypothesis.
Combined formulation matching the manuscript terminology: the projective label is top split-projective, and deleting it together with the target of an irreducible map gives a quotient-closed support.
Dual converse half: an irreducible map into an injective indecomposable forces the two-point complement to be submodule-closed.
The dual criterion with the manuscript's top split-injectivity hypothesis.
Dual combined formulation.