Documentation

TauCeti.CategoryTheory.Projective.Cover

Essential epimorphisms and the uniqueness of a projective cover #

A projective cover of an object M is an epimorphism π : P ⟶ M from a projective object which is minimal, in the sense of being an essential epimorphism: a morphism g into P is an epimorphism as soon as g ≫ π is one. That epimorphism condition is the definition used here — TauCeti.IsEssentialEpi — and nothing beyond [Category C] is assumed for it. It is what makes "the" projective cover well defined: two projective covers of the same object are isomorphic over it.

The familiar reading of minimality, that no proper subobject of P already maps onto M, is intuition rather than a restatement, and the two are not interchangeable. In a balanced category, where a morphism that is both a monomorphism and an epimorphism is an isomorphism, essentiality implies subobject-minimality: a subobject m : P' ⟶ P with m ≫ π an epimorphism is an epimorphism by essentiality, hence an isomorphism. The converse needs more than balancedness — an epimorphism–monomorphism factorization, to reduce an arbitrary g : X ⟶ P to its image before applying minimality to that subobject — which module and representation categories do have, so there the two conditions agree. In an arbitrary category they need not, and it is the epimorphism condition, not the subobject one, that the results below use.

Mathlib has projective objects (CategoryTheory.Projective) and projective presentations (CategoryTheory.ProjectivePresentation, an epimorphism from a projective with no minimality demanded), but neither essential epimorphisms nor projective covers. The module-level notion is TauCeti.IsProjectiveCover in TauCeti.Algebra.Module.ProjectiveCover.Basic, phrased through the superfluousness of the kernel; TauCeti.isProjectiveCover_iff_forall_surjective shows that over an additive group it is exactly the condition used here, so this file is the categorical reading of the same notion, available in categories with no ambient kernel or subobject theory.

The uniqueness argument is short and needs no additivity, exactness, or subobjects — only the lifting property of projectives and the fact that a split epimorphism whose section is an epimorphism is an isomorphism (CategoryTheory.IsIso.of_epi_section'). Given two covers π : P ⟶ M and π' : P' ⟶ M, lift π through π' to h : P ⟶ P'. Essentiality of π' makes h an epimorphism, so projectivity of P' splits it: there is σ : P' ⟶ P with σ ≫ h = 𝟙. That section satisfies σ ≫ π = π', so essentiality of π makes σ an epimorphism too, and a split epimorphism whose section is an epimorphism is an isomorphism.

Main definitions #

Main results #

Implementation notes #

Nothing here uses a preadditive structure — every declaration assumes only [Category C], with projectivity entering as a hypothesis on individual objects — so the file is placed under TauCeti.CategoryTheory.Projective rather than beside its import Mathlib.CategoryTheory.Preadditive.Projective.Basic.

IsEssentialEpi carries Epi π as a field rather than as an instance argument, so that the predicate is a single self-contained hypothesis that can be produced and consumed as a term. Its second field takes the epimorphism hypothesis on the composite as an explicit argument for the same reason.

References #

This supplies the "unique up to isomorphism" clause of the "projective covers and injective envelopes" bullet of Layer 3 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, in the categorical form the representation category needs.

source
structure TauCeti.IsEssentialEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {P M : C} (π : P ⟶ M) :
Prop

An essential epimorphism is an epimorphism π : P ⟶ M such that a morphism g into P is an epimorphism as soon as g ≫ π is one. In a balanced category it implies that nothing smaller than P already covers M; the converse implication needs in addition an epimorphism–monomorphism factorization, as a module or representation category has. No subobject theory is assumed here.

An essential epimorphism from a projective object is a projective cover. Over a module category this is exactly TauCeti.IsProjectiveCover, by TauCeti.isProjectiveCover_iff_forall_surjective.

Instances For
    source
    theorem TauCeti.isEssentialEpi_of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {P M : C} (f : P ⟶ M) [CategoryTheory.IsIso f] :
    IsEssentialEpi f

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

    source
    theorem TauCeti.IsEssentialEpi.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {P M N : C} {π : P ⟶ M} {τ : M ⟶ N} (hπ : IsEssentialEpi π) (hτ : IsEssentialEpi τ) :
    IsEssentialEpi (CategoryTheory.CategoryStruct.comp π τ)

    Essential epimorphisms are closed under composition: if π and τ are both essential then a morphism whose composite with π ≫ τ is an epimorphism is caught first by τ, then by π.

    source
    theorem TauCeti.IsEssentialEpi.isIso_of_comp_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' M : C} [CategoryTheory.Projective P'] {π : P ⟶ M} {π' : P' ⟶ M} (hπ : IsEssentialEpi π) (hπ' : IsEssentialEpi π') {h : P ⟶ P'} (hh : CategoryTheory.CategoryStruct.comp h π' = π) :
    CategoryTheory.IsIso h

    Rigidity of a projective cover. If π : P ⟶ M and π' : P' ⟶ M are essential epimorphisms with P' projective, then any h : P ⟶ P' over M is an isomorphism. Note that only the target P' is required to be projective; taking π' = π this says that an endomorphism of the source of a projective cover commuting with the cover is automatically an isomorphism.

    source
    theorem TauCeti.IsEssentialEpi.exists_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' M : C} [CategoryTheory.Projective P] [CategoryTheory.Projective P'] {π : P ⟶ M} {π' : P' ⟶ M} (hπ : IsEssentialEpi π) (hπ' : IsEssentialEpi π') :
    ∃ (e : P ≅ P'), CategoryTheory.CategoryStruct.comp e.hom π' = π

    The projective cover is unique. Two essential epimorphisms onto M from projective objects are related by an isomorphism of their sources commuting with them, so "the" projective cover of M is well defined up to isomorphism over M.

    source
    theorem TauCeti.IsEssentialEpi.exists_comp_eq_and_isSplitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {P M : C} [CategoryTheory.Projective P] {π : P ⟶ M} (hπ : IsEssentialEpi π) {X : C} [CategoryTheory.Projective X] {f : X ⟶ M} (hf : CategoryTheory.Epi f) :
    ∃ (g : X ⟶ P), CategoryTheory.CategoryStruct.comp g π = f ∧ CategoryTheory.IsSplitEpi g

    The projective cover is minimal. Every epimorphism onto M from a projective object factors through a projective cover of M by a split epimorphism, so the cover is a retract of every projective presentation of M. (In an additive category a retract is a direct summand, but nothing here needs additivity.)

    source
    theorem TauCeti.IsEssentialEpi.isIso_of_isSplitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {P M : C} {π : P ⟶ M} (hπ : IsEssentialEpi π) [CategoryTheory.IsSplitEpi π] :
    CategoryTheory.IsIso π

    An essential epimorphism that splits is an isomorphism. Its composite with its section is the identity, so essentiality makes that section an epimorphism, and a split epimorphism whose section is an epimorphism is an isomorphism.

    source
    theorem TauCeti.IsEssentialEpi.isIso_of_projective_target {C : Type u} [CategoryTheory.Category.{v, u} C] {P M : C} [CategoryTheory.Projective M] {π : P ⟶ M} (hπ : IsEssentialEpi π) :
    CategoryTheory.IsIso π

    A projective object is its own projective cover. An essential epimorphism onto a projective object splits, hence is an isomorphism.