Essential monomorphisms and the uniqueness of an injective envelope

An injective envelope of an object M is a monomorphism ι : M ⟶ I into an injective object which is minimal, in the sense of being an essential monomorphism: a morphism g out of I is a monomorphism as soon as ι ≫ g is one. This file packages that condition as TauCeti.IsEssentialMono and proves the categorical uniqueness and minimality properties of an injective envelope.

The definition and results are dual to TauCeti.IsEssentialEpi in TauCeti/CategoryTheory/Projective/Cover.lean. They are stated directly in the original category, so users do not have to move an injective-envelope argument through the opposite category.

For module categories this is the categorical form of TauCeti.IsInjectiveEnvelope from TauCeti/Algebra/Module/Injective/Envelope/Basic.lean: the latter asks that the range be an essential submodule. Its TauCeti.isInjectiveEnvelope_iff_forall_injective theorem identifies that condition with the one used here. The categorical formulation also applies to functor categories, in particular to representations of a quiver.

Main definitions

• TauCeti.IsEssentialMono: ι is a monomorphism, and every morphism out of its target whose composite with ι is a monomorphism is already one.

Main results

• TauCeti.IsEssentialMono.isIso_of_comp_eq: a comparison morphism between injective envelopes which commutes with their structure maps is an isomorphism.
• TauCeti.IsEssentialMono.exists_iso: two injective envelopes of the same object are isomorphic under that object.
• TauCeti.IsEssentialMono.exists_comp_eq_and_isSplitMono: every embedding of the object into an injective object receives the envelope by a split monomorphism.
• TauCeti.IsEssentialMono.isIso_of_isSplitMono: a split essential monomorphism is an isomorphism.

References

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

structure TauCeti.IsEssentialMono {C : Type u} [CategoryTheory.Category.{v, u} C] {M I : C} (ι : M ⟶ I) : Prop

An essential monomorphism is a monomorphism ι : M ⟶ I such that a morphism out of I is a monomorphism as soon as its composite with ι is one. An essential monomorphism into an injective object is an injective envelope.

• mono : CategoryTheory.Mono ι

  An essential monomorphism is in particular a monomorphism.

• mono_of_comp_mono {X : C} (g : I ⟶ X) : CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp ι g) → CategoryTheory.Mono g

  A morphism out of the target is a monomorphism as soon as its composite with ι is one.

theorem TauCeti.isEssentialMono_of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {M I : C} (f : M ⟶ I) [CategoryTheory.IsIso f] : IsEssentialMono f

An isomorphism is an essential monomorphism: composing with it changes nothing.

theorem TauCeti.IsEssentialMono.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {M I J : C} {ι : M ⟶ I} {κ : I ⟶ J} (hι : IsEssentialMono ι) (hκ : IsEssentialMono κ) : IsEssentialMono (CategoryTheory.CategoryStruct.comp ι κ)

Essential monomorphisms are closed under composition.

theorem TauCeti.IsEssentialMono.isIso_of_comp_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {M I I' : C} [CategoryTheory.Injective I] {ι : M ⟶ I} {ι' : M ⟶ I'} (hι : IsEssentialMono ι) (hι' : IsEssentialMono ι') {h : I ⟶ I'} (hh : CategoryTheory.CategoryStruct.comp ι h = ι') : CategoryTheory.IsIso h

Rigidity of an injective envelope. If ι : M ⟶ I and ι' : M ⟶ I' are essential monomorphisms with I injective, then any h : I ⟶ I' under M is an isomorphism. Only the source of h has to be injective.

theorem TauCeti.IsEssentialMono.exists_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {M I I' : C} [CategoryTheory.Injective I] [CategoryTheory.Injective I'] {ι : M ⟶ I} {ι' : M ⟶ I'} (hι : IsEssentialMono ι) (hι' : IsEssentialMono ι') : ∃ (e : I ≅ I'), CategoryTheory.CategoryStruct.comp ι e.hom = ι'

The injective envelope is unique. Two essential monomorphisms out of M into injective objects are related by an isomorphism of their targets commuting with them.

theorem TauCeti.IsEssentialMono.exists_comp_eq_and_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] {M I : C} [CategoryTheory.Injective I] {ι : M ⟶ I} (hι : IsEssentialMono ι) {X : C} [CategoryTheory.Injective X] {f : M ⟶ X} (hf : CategoryTheory.Mono f) : ∃ (g : I ⟶ X), CategoryTheory.CategoryStruct.comp ι g = f ∧ CategoryTheory.IsSplitMono g

The injective envelope is minimal. Every monomorphism from M into an injective object extends along an injective envelope by a split monomorphism, so the envelope is a retract of every injective copresentation of M.

theorem TauCeti.IsEssentialMono.isIso_of_isSplitMono {C : Type u} [CategoryTheory.Category.{v, u} C] {M I : C} {ι : M ⟶ I} (hι : IsEssentialMono ι) [CategoryTheory.IsSplitMono ι] : CategoryTheory.IsIso ι

An essential monomorphism that splits is an isomorphism.

theorem TauCeti.IsEssentialMono.isIso_of_injective_source {C : Type u} [CategoryTheory.Category.{v, u} C] {M I : C} [CategoryTheory.Injective M] {ι : M ⟶ I} (hι : IsEssentialMono ι) : CategoryTheory.IsIso ι

An injective object is its own injective envelope. An essential monomorphism from an injective object splits, hence is an isomorphism.