The vertex injective is the injective envelope of the vertex simple

For a vertex i of a quiver Q, the embedding Sᵢ ↪ Iᵢ of TauCeti.RepresentationTheory.Quiver.Representation.Comparison places the vertex simple inside the vertex injective. This file proves that when the trivial path is the only path i → i, this embedding is an injective envelope: it is an essential monomorphism into an injective object.

The local hypothesis is sharp. For the one-loop quiver, (Iᵢ)ᵢ is the full dual of k[X], while the image of Sᵢ is only the functional reading the constant coefficient; it is not an essential subobject. Acyclicity of the whole quiver is a sufficient uniform hypothesis, but cycles away from i play no role.

The result gives the strong form of essentiality: a morphism out of Iᵢ which remains monic on Sᵢ is a split monomorphism. Consequently, the general essential-monomorphism API identifies Iᵢ as the minimal injective object containing Sᵢ and makes it unique up to isomorphism under Sᵢ.

Main results

• TauCeti.isSplitMono_of_mono_simpleRepToIndecInjRep_comp: a map out of Iᵢ which is monic on Sᵢ is a split monomorphism.
• TauCeti.isEssentialMono_simpleRepToIndecInjRep: Sᵢ ↪ Iᵢ is an essential monomorphism.

References

The construction is dual to TauCeti/RepresentationTheory/Quiver/Representation/Projective/Cover.lean.

See I. Assem, D. Simson and A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, I.5 and III.2.

theorem TauCeti.eq_smul_simpleRepToIndecInjRep_app_generator (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] {i : Q} (h : ∀ (p : Quiver.Path i i), p = Quiver.Path.nil) (x : ↑((indecInjRep k Q i).obj ((CategoryTheory.Paths.of Q).obj i))) : x = x Quiver.Path.nil • (CategoryTheory.ConcreteCategory.hom ((simpleRepToIndecInjRep k i).app ((CategoryTheory.Paths.of Q).obj i))) (simpleRepGenerator k i)

With no nontrivial path i → i, the value of the vertex injective at i is the line spanned by the image of the generator of the vertex simple.

theorem TauCeti.isSplitMono_of_mono_simpleRepToIndecInjRep_comp (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] {i : Q} (h : ∀ (p : Quiver.Path i i), p = Quiver.Path.nil) {X : QuiverRep k Q} (g : indecInjRep k Q i ⟶ X) (hg : CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp (simpleRepToIndecInjRep k i) g)) : CategoryTheory.IsSplitMono g

Sᵢ ↪ Iᵢ is an essential monomorphism, in the strong split form: with no nontrivial path i → i, a morphism out of Iᵢ which remains monic after restriction to Sᵢ is already a split monomorphism.

theorem TauCeti.isEssentialMono_simpleRepToIndecInjRep (k : Type (max v w)) {Q : Type v} [Field k] [Quiver Q] {i : Q} (h : ∀ (p : Quiver.Path i i), p = Quiver.Path.nil) : IsEssentialMono (simpleRepToIndecInjRep k i)

The vertex injective is the injective envelope of the vertex simple. If the trivial path is the only path i → i, the canonical embedding Sᵢ ↪ Iᵢ is an essential monomorphism; together with TauCeti.injective_indecInjRep, this characterizes Iᵢ as the injective envelope.