Right and left almost split morphisms #
A morphism f : X ⟶ Y is right almost split when it is not a split epimorphism and every
morphism Z ⟶ Y that is not a split epimorphism factors through it. Dually f is left almost
split when it is not a split monomorphism and every morphism X ⟶ Z that is not a split
monomorphism factors through it. So a right almost split morphism into Y is a single map that
absorbs all the "inessential" maps into Y at once, and a left almost split morphism out of X
absorbs all the inessential maps out of X.
These are the two lifting properties an almost-split (Auslander-Reiten) sequence
0 → τM → E → M → 0 carries: E ⟶ M is right almost split and τM ⟶ E is left almost split.
This file builds them as conditions on a single morphism of an arbitrary category, so that the
sequence-level notion can be assembled from them — it is, as
CategoryTheory.ShortComplex.IsAlmostSplit in TauCeti/CategoryTheory/AlmostSplit/Sequence.lean —
and proves the two facts that make the indecomposability clauses in the definition of an
almost-split sequence redundant: the target of a right almost split morphism is indecomposable,
and dually the source of a left almost split morphism is indecomposable. Neither end of an
almost-split sequence has to be assumed indecomposable — the lifting properties already force
it.
The connection to TauCeti.IsIrreducibleMorphism is the sharpened factorization
TauCeti.IsRightAlmostSplit.exists_isSplitMono_of_isIrreducibleMorphism: an irreducible morphism
into Y not only factors through a right almost split f : X ⟶ Y, it factors through it by a
split monomorphism, exhibiting its source as a retract of X. This is what makes the middle
term of an almost-split sequence the receptacle of the irreducible morphisms into M, and hence
what ties the sequence to the arrows of the Auslander-Reiten quiver.
Main results #
TauCeti.IsRightAlmostSplitandTauCeti.IsLeftAlmostSplit: the definitions, withTauCeti.isRightAlmostSplit_iffandTauCeti.isLeftAlmostSplit_iffas the introduction rules and the projectionsnot_isSplitEpi/not_isSplitMonoandfactors.TauCeti.isRightAlmostSplit_op_iffandTauCeti.isLeftAlmostSplit_op_iff: the two notions are exchanged by passage to the opposite category, so every result about one transports to the other.TauCeti.IsRightAlmostSplit.indecomposable: the target of a right almost split morphism is indecomposable, andTauCeti.IsLeftAlmostSplit.indecomposable: the source of a left almost split morphism is indecomposable.TauCeti.IsRightAlmostSplit.exists_isSplitMono_of_isIrreducibleMorphismandTauCeti.IsLeftAlmostSplit.exists_isSplitEpi_of_isIrreducibleMorphism: an irreducible morphism factors through an almost split morphism by a split mono, resp. a split epi.TauCeti.IsRightAlmostSplit.epi_of_epiandTauCeti.IsLeftAlmostSplit.mono_of_mono: a right almost split morphism is an epimorphism as soon as some non-split-epi into its target is one.TauCeti.IsRightAlmostSplit.not_projectiveandTauCeti.IsLeftAlmostSplit.not_injective: the target of an epimorphic right almost split morphism is not projective, and dually the source of a monomorphic left almost split morphism is not injective.TauCeti.IsRightAlmostSplit.not_isSplitMono,.not_monoand.ne_zeroand their left-hand duals: an epimorphic right almost split morphism is neither a split monomorphism nor — in a balanced category — a monomorphism, and it is nonzero.- Invariance under isomorphisms of the source and the target,
TauCeti.isRightAlmostSplit_comp_iso_iff,TauCeti.isRightAlmostSplit_iso_comp_iffand their left-hand analogues, so the notions descend to a skeleton.
Implementation notes #
The definitions are conjunctions rather than structures, matching the shape of
TauCeti.IsIrreducibleMorphism; their bodies are not exposed outside this module, so
TauCeti.isRightAlmostSplit_iff and TauCeti.isLeftAlmostSplit_iff are the introduction rules.
Both predicates are stated for f : X ⟶ Y in the same category, the right-hand notion being a
condition at the target Y and the left-hand one a condition at the source X. The lifting
quantifiers range over all objects of the ambient category. For the Auslander-Reiten theory of a
finite-dimensional algebra that is the intended reading: the ambient category there is the
finite-dimensional one, as it already is for TauCeti.IsIrreducibleMorphism. The distinction is
not cosmetic — quantifying an almost-split sequence's lifting properties over a category of
representations with no finiteness restriction states a strictly stronger condition, and the
existence theorem for such sequences is false in that form (Paquette, A non-existence theorem for
almost split sequences, arXiv:1104.1195, exhibits infinite-dimensional indecomposable
representations of the Kronecker quiver that end no almost-split sequence). Instantiating C at
the finite-dimensional subcategory is what recovers the intended notion.
A right almost split morphism may well be zero: over a field, the map 0 ⟶ k is right almost
split, every non-split-epi into the simple projective k being zero. So there is no unconditional
analogue here of TauCeti.IsIrreducibleMorphism.ne_zero, and this is not an oversight — it is the
boundary case of a projective target, where the almost split morphism is the inclusion of the
radical. TauCeti.IsRightAlmostSplit.ne_zero therefore assumes [Epi f], which is exactly what
that boundary case fails.
Indecomposability of the target is proved directly from the definition rather than through
endomorphism rings, so it needs no additivity, no finiteness and no field: given Y ≅ A ⊞ B with
both summands nonzero, neither inclusion A ⟶ Y nor B ⟶ Y is a split epimorphism (a section of
one of them retracts A ⊞ B onto that summand along its inclusion, and the two complementary
structure maps then compose to 0, collapsing the other summand), so both factor through f, and
CategoryTheory.Limits.biprod.desc assembles the two factorizations into a section of f.
References #
- M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, CUP (1995), V.1.
- I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, LMS Student Texts 65, CUP (2006), IV.1.
- C. Paquette, A non-existence theorem for almost split sequences, arXiv:1104.1195 (2011).
The definitions #
A right almost split morphism: one that is not a split epimorphism, and through which every morphism to its target that is not a split epimorphism factors.
The negative clause is what makes the notion nonvacuous: without it every split epimorphism would
qualify, the identity among them. With it, a right almost split morphism is in particular not an
isomorphism (TauCeti.IsRightAlmostSplit.not_isIso) and its target is indecomposable
(TauCeti.IsRightAlmostSplit.indecomposable).
Equations
- TauCeti.IsRightAlmostSplit f = (¬CategoryTheory.IsSplitEpi f ∧ ∀ (Z : C) (g : Z ⟶ Y), ¬CategoryTheory.IsSplitEpi g → ∃ (h : Z ⟶ X), CategoryTheory.CategoryStruct.comp h f = g)
Instances For
A left almost split morphism: one that is not a split monomorphism, and through which
every morphism out of its source that is not a split monomorphism factors. This is the condition
of TauCeti.IsRightAlmostSplit read in the opposite category
(TauCeti.isRightAlmostSplit_op_iff).
Equations
- TauCeti.IsLeftAlmostSplit f = (¬CategoryTheory.IsSplitMono f ∧ ∀ (Z : C) (g : X ⟶ Z), ¬CategoryTheory.IsSplitMono g → ∃ (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = g)
Instances For
The two clauses of being right almost split, spelled out. This is both the introduction
rule — the body of TauCeti.IsRightAlmostSplit is not exposed outside this module — and the
elimination rule; the components are also available as
TauCeti.IsRightAlmostSplit.not_isSplitEpi and TauCeti.IsRightAlmostSplit.factors.
The two clauses of being left almost split, spelled out; the introduction and elimination
rule for TauCeti.IsLeftAlmostSplit.
A right almost split morphism is not a split epimorphism.
The factorization property: every morphism to the target of a right almost split morphism that is not itself a split epimorphism factors through it.
A left almost split morphism is not a split monomorphism.
The factorization property: every morphism out of the source of a left almost split morphism that is not itself a split monomorphism factors through it.
A right almost split morphism is not an isomorphism, an isomorphism being a split epi.
A left almost split morphism is not an isomorphism, an isomorphism being a split mono.
An identity is not right almost split.
An identity is not left almost split.
Duality #
The opposite of a left almost split morphism is right almost split, and conversely: the two notions are exchanged by passage to the opposite category.
The opposite of a right almost split morphism is left almost split, and conversely.
Invariance under isomorphisms of the source and the target #
Postcomposing a right almost split morphism with an isomorphism keeps it right almost split.
Precomposing a right almost split morphism with an isomorphism keeps it right almost split.
Precomposing a left almost split morphism with an isomorphism keeps it left almost split.
Postcomposing a left almost split morphism with an isomorphism keeps it left almost split.
Being right almost split is invariant under an isomorphism of the target.
Being right almost split is invariant under an isomorphism of the source.
Being left almost split is invariant under an isomorphism of the source.
Being left almost split is invariant under an isomorphism of the target.
Interaction with epimorphisms, monomorphisms, and irreducible morphisms #
A right almost split morphism is an epimorphism as soon as some non-split epimorphism into its target is one. For a module category this is how the almost split morphism onto a non-projective module is seen to be surjective: a projective cover of it is an epimorphism and, the module being non-projective, not a split one.
A left almost split morphism is a monomorphism as soon as some non-split monomorphism out of its source is one.
An epimorphic right almost split morphism is not a split monomorphism: a splitting on that side would make it an isomorphism.
A monomorphic left almost split morphism is not a split epimorphism, dually to
TauCeti.IsRightAlmostSplit.not_isSplitMono.
In a balanced category an epimorphic right almost split morphism is not a monomorphism: it would otherwise be an isomorphism.
In a balanced category a monomorphic left almost split morphism is not an epimorphism, dually
to TauCeti.IsRightAlmostSplit.not_mono.
An epimorphic right almost split morphism is nonzero. A zero epimorphism forces its target to be a zero object, and the zero morphism into a zero object is a split epimorphism.
A monomorphic left almost split morphism is nonzero, dually to
TauCeti.IsRightAlmostSplit.ne_zero.
An irreducible morphism into the target of a right almost split morphism factors through it by a split monomorphism, so its source is a retract of the source of the almost split morphism.
This is why the middle term of an almost-split sequence receives all the irreducible morphisms into its right-hand end.
An irreducible morphism out of the source of a left almost split morphism factors through it by a split epimorphism, so its target is a retract of the target of the almost split morphism.
Projectivity and injectivity of the almost split end #
The target of an epimorphic right almost split morphism is not projective. Were it
projective, its identity would factor through the epimorphism f, which is exactly a section of
f, and f is not a split epimorphism.
The source of a monomorphic left almost split morphism is not injective, dually to
TauCeti.IsRightAlmostSplit.not_projective: its identity would factor through the monomorphism
f, retracting it.
Indecomposability of the almost split end #
The target of a right almost split morphism is indecomposable. So the indecomposability of the right-hand end of an almost-split sequence is a consequence of its lifting property rather than a hypothesis on it.
The source of a left almost split morphism is indecomposable, dually to
TauCeti.IsRightAlmostSplit.indecomposable.