Minimal injective copresentations

A minimal injective copresentation of a module M is an exact sequence

0 → M → Q₀ → Q₁

in which Q₀ and Q₁ are injective and both successive extensions are minimal. The first structure map is an injective envelope of M. Exactness makes the second map descend to an embedding Q₀ / range(i₀) → Q₁, and minimality says that this induced embedding is an injective envelope as well. Equivalently, the ranges of both displayed maps are essential submodules of their targets.

This file records both directions of that equivalence and proves uniqueness: two minimal injective copresentations of the same module are related by linear equivalences of both injective terms, commuting with both maps. Thus the first two terms of a minimal injective resolution are independent of the choices. The construction is dual to minimal projective presentations, and is the injective half of the presentation theory used to define the Auslander--Reiten translate and its inverse.

Main definitions and results

• TauCeti.IsMinimalInjectiveCopresentation: exactness, an injective envelope in degree zero, an injective module in degree one, and essential image in degree one.
• TauCeti.IsMinimalInjectiveCopresentation.cokernelMap: the induced map Q₀ / range(i₀) → Q₁.
• TauCeti.IsMinimalInjectiveCopresentation.isInjectiveEnvelope_cokernelMap: the induced map is the second injective envelope.
• TauCeti.IsInjectiveEnvelope.isMinimalInjectiveCopresentation: the converse constructor from two successive injective envelopes.
• TauCeti.IsMinimalInjectiveCopresentation.exists_linearEquiv: uniqueness as an isomorphism of the two copresentation diagrams.

References

This supplies the injective half of sublayer 6B, "minimal projective/injective presentations", of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md. That sublayer is an explicit prerequisite for the transpose, the Auslander--Reiten translate, and almost-split sequences.

See M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, CUP (1995), Chapter IV, and I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, CUP (2006), Section IV.2.

structure TauCeti.IsMinimalInjectiveCopresentation {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] (i₀ : M →ₗ[R] Q₀) (i₁ : Q₀ →ₗ[R] Q₁) : Prop

A minimal injective copresentation 0 → M → Q₀ → Q₁ consists of an injective envelope i₀ : M →ₗ[R] Q₀, an exact pair i₀, i₁, and an injective Q₁ in which the range of i₁ is essential. Exactness identifies Q₀ / range(i₀) with the source of the second embedding, so the last two fields say precisely that this induced embedding is another injective envelope.

• isInjectiveEnvelope : IsInjectiveEnvelope i₀

  The first map exhibits Q₀ as the injective envelope of M.

• exact : Function.Exact ⇑i₀ ⇑i₁

  The image of i₀ is the kernel of i₁.

• moduleInjective : Module.Injective R Q₁

  The second ambient module is injective.

• isEssential_range : IsEssential i₁.range

  The image of i₁, equivalently of the induced cokernel embedding, is essential in Q₁.

def TauCeti.IsMinimalInjectiveCopresentation.cokernelMap {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] {i₀ : M →ₗ[R] Q₀} {i₁ : Q₀ →ₗ[R] Q₁} (h : IsMinimalInjectiveCopresentation i₀ i₁) : Q₀ ⧸ i₀.range →ₗ[R] Q₁

The map Q₀ / range(i₀) → Q₁ induced by the second map of an injective copresentation.

Equations

• h.cokernelMap = i₀.range.liftQ i₁ ⋯

@[simp]

theorem TauCeti.IsMinimalInjectiveCopresentation.cokernelMap_mk {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] {i₀ : M →ₗ[R] Q₀} {i₁ : Q₀ →ₗ[R] Q₁} (h : IsMinimalInjectiveCopresentation i₀ i₁) (x : Q₀) : h.cokernelMap (Submodule.Quotient.mk x) = i₁ x

The induced cokernel map agrees with i₁ on representatives.

@[simp]

theorem TauCeti.IsMinimalInjectiveCopresentation.range_cokernelMap {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] {i₀ : M →ₗ[R] Q₀} {i₁ : Q₀ →ₗ[R] Q₁} (h : IsMinimalInjectiveCopresentation i₀ i₁) : h.cokernelMap.range = i₁.range

The induced cokernel map has the same range as the displayed second map.

theorem TauCeti.IsMinimalInjectiveCopresentation.isInjectiveEnvelope_cokernelMap {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] {i₀ : M →ₗ[R] Q₀} {i₁ : Q₀ →ₗ[R] Q₁} (h : IsMinimalInjectiveCopresentation i₀ i₁) : IsInjectiveEnvelope h.cokernelMap

The induced map Q₀ / range(i₀) → Q₁ is the second injective envelope in a minimal injective copresentation.

theorem TauCeti.IsInjectiveEnvelope.isMinimalInjectiveCopresentation {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] {i₀ : M →ₗ[R] Q₀} {i₁ : Q₀ →ₗ[R] Q₁} (h₀ : IsInjectiveEnvelope i₀) (hexact : Function.Exact ⇑i₀ ⇑i₁) (h₁ : IsInjectiveEnvelope (i₀.range.liftQ i₁ ⋯)) : IsMinimalInjectiveCopresentation i₀ i₁

Construct a minimal injective copresentation from an injective envelope of M, an exact continuation, and an injective envelope of the resulting cokernel.

theorem TauCeti.IsMinimalInjectiveCopresentation.i₀_bijective_of_moduleInjective {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] {i₀ : M →ₗ[R] Q₀} {i₁ : Q₀ →ₗ[R] Q₁} [Small.{w₀, u} R] [Small.{v, u} R] [Module.Injective R M] (h : IsMinimalInjectiveCopresentation i₀ i₁) : Function.Bijective ⇑i₀

If the module being copresented is already injective, then the first structure map is an isomorphism.

theorem TauCeti.IsMinimalInjectiveCopresentation.i₁_eq_zero_of_moduleInjective {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] {i₀ : M →ₗ[R] Q₀} {i₁ : Q₀ →ₗ[R] Q₁} [Small.{w₀, u} R] [Small.{v, u} R] [Module.Injective R M] (h : IsMinimalInjectiveCopresentation i₀ i₁) : i₁ = 0

A minimal injective copresentation of an injective module has zero second map.

theorem TauCeti.IsMinimalInjectiveCopresentation.subsingleton_Q₁_of_moduleInjective {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] {i₀ : M →ₗ[R] Q₀} {i₁ : Q₀ →ₗ[R] Q₁} [Small.{w₀, u} R] [Small.{v, u} R] [Module.Injective R M] (h : IsMinimalInjectiveCopresentation i₀ i₁) : Subsingleton Q₁

The second injective term of a minimal copresentation of an injective module is a zero module.

theorem TauCeti.IsMinimalInjectiveCopresentation.exists_linearEquiv {R : Type u} {M : Type v} {Q₀ : Type w₀} {Q₁ : Type w₁} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q₀] [Module R Q₀] [AddCommGroup Q₁] [Module R Q₁] {i₀ : M →ₗ[R] Q₀} {i₁ : Q₀ →ₗ[R] Q₁} {Q₀' : Type w₀'} {Q₁' : Type w₁'} [AddCommGroup Q₀'] [Module R Q₀'] [AddCommGroup Q₁'] [Module R Q₁'] {i₀' : M →ₗ[R] Q₀'} {i₁' : Q₀' →ₗ[R] Q₁'} [Small.{w₀, u} R] [Small.{w₀', u} R] [Small.{w₁, u} R] [Small.{w₁', u} R] (h : IsMinimalInjectiveCopresentation i₀ i₁) (h' : IsMinimalInjectiveCopresentation i₀' i₁') : ∃ (e₀ : Q₀ ≃ₗ[R] Q₀') (e₁ : Q₁ ≃ₗ[R] Q₁'), ↑e₀ ∘ₗ i₀ = i₀' ∧ ↑e₁ ∘ₗ i₁ = i₁' ∘ₗ ↑e₀

Uniqueness of minimal injective copresentations. Two copresentations of the same module are isomorphic in both injective degrees, by equivalences commuting with both structure maps.