Relative injectives in an exact category #
This file develops injectivity relative to a Quillen exact structure. An object is injective when maps into it extend across the inflations of the chosen structure. Thus the notion depends on the exact structure: every object is injective for the split structure, while the canonical structure on an abelian category recovers Mathlib's ordinary injective objects.
Relative injectivity is the formal dual of relative projectivity. The equivalence is made explicit
by TauCeti.ExactStructure.isInjective_iff_isProjective_op, so results about projectives can be
transported through the opposite exact structure without maintaining parallel hypotheses.
The splitting API is also dual. A conflation whose first term is injective splits because its inflation has a retraction.
The bundled TauCeti.ExactStructure.InjectivePresentation records a conflation into a relatively
injective object, and TauCeti.ExactStructure.EnoughInjectives says that every object admits one.
A morphism of the presented objects extends to the injective middle terms and hence induces a
morphism of the cokernel terms; both are recorded as
TauCeti.ExactStructure.InjectivePresentation.middleMap and
TauCeti.ExactStructure.InjectivePresentation.cokernelMap. They depend on a choice of extension,
which only the stable quotient removes.
References #
- Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1–69, https://arxiv.org/abs/0811.1480, Sections 11–12.
- Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.
The objects injective relative to E: maps into such an object extend across every inflation
of the exact structure.
Equations
- E.isInjective I = ∀ ⦃X Y : C⦄ {i : X ⟶ Y}, E.IsInflation i → ∀ (f : X ⟶ I), ∃ (g : Y ⟶ I), CategoryTheory.CategoryStruct.comp i g = f
Instances For
The defining extension property for relative injectivity.
The chosen extension of f : X ⟶ I across an inflation i : X ⟶ Y.
Equations
- hI.factorThru hi f = ⋯.choose
Instances For
Relative injectives are closed under retracts.
A zero object is injective relative to every exact structure.
A binary direct sum of relatively injective objects is relatively injective.
Relative injectives are closed under binary products; in a preadditive category these are biproducts.
A conflation with injective first term splits. The retraction of its inflation is the extension of the identity of that term.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every object is injective for the split exact structure.
For the canonical exact structure of an abelian category, relative injectivity is Mathlib's ordinary categorical injectivity.
An injective presentation of X relative to E is a conflation X → I → K whose
middle term is E-injective.
- I : C
The relatively injective middle term.
- K : C
The cokernel term of the presentation.
The inflation from the presented object.
The deflation from the injective term.
The two presentation maps form a short complex.
- conflation : E.Conflation { X₁ := X, X₂ := self.I, X₃ := self.K, f := self.i, g := self.p, zero := ⋯ }
The presentation is a conflation of
E. - isInjective : E.isInjective self.I
The middle term is injective relative to
E.
Instances For
An exact structure has enough injectives if every object admits a relative injective presentation.
- presentation (X : C) : Nonempty (E.InjectivePresentation X)
Instances For
The tautological injective presentation in the split exact structure.
Equations
- TauCeti.ExactStructure.InjectivePresentation.split X = { I := X, K := 0, i := CategoryTheory.CategoryStruct.id X, p := 0, zero := ⋯, conflation := ⋯, isInjective := ⋯ }
Instances For
Mathlib's injective presentation gives a relative injective presentation for the canonical exact structure of an abelian category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The extension of f : X ⟶ Y to the injective middle terms of relative injective
presentations P of X and Q of Y, chosen by relative injectivity of Q.I.
Equations
- P.middleMap Q f = ⋯.factorThru ⋯ (CategoryTheory.CategoryStruct.comp f Q.i)
Instances For
The chosen extension of f does extend f across the two inflations.
The chosen extension of f does extend f across the two inflations.
The morphism induced by f : X ⟶ Y on the cokernel terms of relative injective
presentations, through the chosen extension TauCeti.ExactStructure.InjectivePresentation.middleMap
of the injective middle terms.
Equations
- P.cokernelMap Q f = ⋯.desc (CategoryTheory.CategoryStruct.comp (P.middleMap Q f) Q.p) ⋯
Instances For
The induced morphism on cokernel terms makes the square on the two deflations commute.
The induced morphism on cokernel terms makes the square on the two deflations commute.
The split exact structure has enough relative injectives.
Enough ordinary injectives give enough relative injectives for the canonical exact structure on an abelian category.
Choose a relative injective presentation from enough relative injectives.
Equations
- h.injectivePresentation X = ⋯.some
Instances For
Relative injectivity in C is relative projectivity in the opposite exact category.
Relative projectivity in C is relative injectivity in the opposite exact category.
An injective presentation in C is a projective presentation in Cᵒᵖ.
Equations
Instances For
Unopposing an injective presentation gives a projective presentation.
Equations
Instances For
A projective presentation in C is an injective presentation in Cᵒᵖ.
Equations
Instances For
The middle term of the opposite presentation is the opposite projective term.
The cokernel term of the opposite presentation is the opposite kernel term.
After identifying the middle term, the opposite presentation starts with the opposite deflation.
After identifying the middle and cokernel terms, the opposite presentation ends with the opposite inflation.
Unopposing a projective presentation gives an injective presentation.
Equations
Instances For
Enough relative injectives in C are equivalent to enough relative projectives in Cᵒᵖ.
Enough relative projectives in C are equivalent to enough relative injectives in Cᵒᵖ.