Projective covers

A projective cover of a module M is a surjection f : P →ₗ[R] M from a projective module whose kernel is superfluous in P (TauCeti.IsSuperfluous). Mathlib has projective objects but no projective covers; this file supplies the predicate and the two facts everything downstream rests on.

Both rest on the minimality packaged in TauCeti.IsSuperfluous.surjective_of_surjective_comp: over a covering module that is an additive group, a map into the source of a cover whose composite with the cover is onto is itself onto, the kernel of a cover being too small for the image of such a map to miss it. This is the sense in which the superfluous-kernel condition makes a cover minimal, and read backwards it is TauCeti.isProjectiveCover_iff_forall_surjective: over an additive group the covers of M are exactly the essential epimorphisms onto M from a projective module. Both directions need differences, so neither is available for a covering module that is only a monoid.

The first fact is that a projective cover receives every projective presentation: if Q is projective and g : Q →ₗ[R] M is surjective, then g factors as f ∘ₗ h with h : Q →ₗ[R] P surjective (TauCeti.IsProjectiveCover.exists_surjective); taking for Q the finite free module on a generating family, this reads off that a cover of a finitely generated module is itself finitely generated (TauCeti.IsProjectiveCover.finite). The second is that a projective cover is unique: any two projective covers of M differ by a linear equivalence commuting with the covering maps (TauCeti.IsProjectiveCover.exists_linearEquiv). Uniqueness is what makes "the" projective cover a well-defined object, and hence what makes the Cartan matrix Cᵢⱼ = [Pᵢ : Sⱼ] of a finite-dimensional algebra well defined.

Existence of projective covers is a separate matter: over a semiperfect ring every finitely generated module has one, while existence for arbitrary modules is a strictly stronger condition on the ring, met for instance by a semiprimary ring — a finite-dimensional algebra among them. Nothing here proves or assumes it; every statement below is conditional on a cover being given, and TauCeti/Algebra/Module/ProjectiveCover/Existence.lean supplies covers over a semiprimary ring.

Main definitions

• TauCeti.IsProjectiveCover: f : P →ₗ[R] M is surjective, P is projective, and ker f is superfluous.

Main results

• TauCeti.isProjectiveCover_id: a projective module is its own projective cover.
• TauCeti.isProjectiveCover_iff_forall_surjective: a surjection from a projective module that is an additive group is a projective cover exactly when it is an essential epimorphism.
• TauCeti.IsProjectiveCover.exists_surjective: every surjection onto M from a projective module factors through a projective cover by a surjection.
• TauCeti.IsProjectiveCover.finite: a projective cover of a finitely generated module is finitely generated.
• TauCeti.IsProjectiveCover.bijective_of_comp_eq and TauCeti.IsProjectiveCover.exists_linearEquiv: uniqueness, first as bijectivity of any comparison map between two covers and then as the existence of an isomorphism over M.
• TauCeti.IsProjectiveCover.nonempty_linearEquiv_ker: uniqueness read on the kernels — the syzygy cut out by a projective cover of M is independent of the cover.
• TauCeti.IsProjectiveCover.comp: composing a projective cover with a surjection that itself has superfluous kernel again gives a projective cover.
• TauCeti.IsProjectiveCover.ker_le_jacobson: the kernel of a projective cover lies in the radical of the covering module.
• TauCeti.isProjectiveCover_mkQ_iff: the concrete family of covers, P ↠ P ⧸ N is a projective cover of a projective P exactly when N is superfluous; over a coatomic submodule lattice TauCeti.isProjectiveCover_mkQ_iff_le_jacobson reads this off the radical, so that R ↠ R ⧸ I is a projective cover exactly when I ≤ Ring.jacobson R. For a nilpotent ideal I, TauCeti.isProjectiveCover_mkQ_smul_top_of_isNilpotent covers the top P ⧸ I • P by P.
• TauCeti.IsProjectiveCover.exists_comp_eq: every map from a covering module into a semisimple module factors through the cover, and TauCeti.IsProjectiveCover.homEquivOfIsSemisimpleModule: precomposition with a projective cover f : P →ₗ[R] M is an isomorphism Hom_R(M, T) ≃ₗ[k] Hom_R(P, T) for every semisimple T.

References

Uniqueness, proved here, is what makes "the" projective cover of a module a well-defined object; that a cover exists at all is a condition on the ring, established for a semiprimary ring — a finite-dimensional algebra among them — in TauCeti/Algebra/Module/ProjectiveCover/Existence.lean. The dual notion, an injective envelope, is an essential monomorphism into an injective module; nothing here is used for it.

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

structure TauCeti.IsProjectiveCover {R : Type u} {M : Type v} {P : Type w} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid P] [Module R P] (f : P →ₗ[R] M) : Prop

A projective cover of M: a surjection from a projective module whose kernel is superfluous. The superfluous kernel is the minimality of the cover: when P is an additive group it says exactly that no proper submodule of P still surjects onto M, equivalently that every map into P whose composite with f is onto is onto already (TauCeti.isProjectiveCover_iff_forall_surjective).

• projective : Module.Projective R P

  The covering module is projective.

• surjective : Function.Surjective ⇑f

  The covering map is onto.

• isSuperfluous_ker : IsSuperfluous f.ker

  Minimality: the kernel is superfluous, so the cover cannot be shrunk.

theorem TauCeti.isProjectiveCover_id {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Projective R M] : IsProjectiveCover LinearMap.id

A projective module is its own projective cover, along the identity.

theorem TauCeti.isProjectiveCover_iff_forall_surjective {R : Type u} {M : Type v} {P : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] [Module.Projective R P] {f : P →ₗ[R] M} (hf : Function.Surjective ⇑f) : IsProjectiveCover f ↔ ∀ {P' : Type w} [inst : AddCommMonoid P'] [inst_1 : Module R P'] (h : P' →ₗ[R] P), Function.Surjective ⇑(f ∘ₗ h) → Function.Surjective ⇑h

Projective covers are the essential epimorphisms from a projective module. A surjection f : P →ₗ[R] M from a projective module is a projective cover exactly when every map into P whose composite with f is onto is itself onto.

theorem TauCeti.IsProjectiveCover.exists_surjective {R : Type u} {M : Type v} {P : Type w} {Q : Type w'} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] [AddCommMonoid Q] [Module R Q] [Module.Projective R Q] {f : P →ₗ[R] M} (hf : IsProjectiveCover f) {g : Q →ₗ[R] M} (hg : Function.Surjective ⇑g) : ∃ (h : Q →ₗ[R] P), f ∘ₗ h = g ∧ Function.Surjective ⇑h

A projective cover receives every projective presentation. A surjection onto M from a projective module factors through a projective cover of M, by a surjection.

theorem TauCeti.IsProjectiveCover.finite {R : Type u} {M : Type v} {P : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] [Module.Finite R M] {f : P →ₗ[R] M} (hf : IsProjectiveCover f) : Module.Finite R P

A projective cover of a finitely generated module is finitely generated. If M is finitely generated, then so is the source of any projective cover of M. This holds over a semiring when the covering and covered modules are additive groups; no finiteness hypothesis beyond Module.Finite R M is needed.

theorem TauCeti.IsProjectiveCover.bijective_of_comp_eq {R : Type u} {M : Type v} {P : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {P' : Type u_1} [AddCommGroup P'] [Module R P'] {f : P →ₗ[R] M} {f' : P' →ₗ[R] M} (hf : IsProjectiveCover f) (hf' : IsProjectiveCover f') {h : P →ₗ[R] P'} (hcomp : f' ∘ₗ h = f) : Function.Bijective ⇑h

Uniqueness of the projective cover, in comparison-map form. A map between the sources of two projective covers of M that commutes with the covering maps is automatically an isomorphism.

theorem TauCeti.IsProjectiveCover.exists_linearEquiv {R : Type u} {M : Type v} {P : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {P' : Type u_1} [AddCommGroup P'] [Module R P'] {f : P →ₗ[R] M} {f' : P' →ₗ[R] M} (hf : IsProjectiveCover f) (hf' : IsProjectiveCover f') : ∃ (e : P ≃ₗ[R] P'), f' ∘ₗ ↑e = f

Uniqueness of the projective cover. Two projective covers of the same module are related by a linear equivalence commuting with the covering maps; in particular the covering module of a projective cover is well defined up to isomorphism.

theorem TauCeti.IsProjectiveCover.nonempty_linearEquiv_ker {R : Type u} {M : Type v} {P : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {P' : Type u_1} [AddCommGroup P'] [Module R P'] {f : P →ₗ[R] M} {f' : P' →ₗ[R] M} (hf : IsProjectiveCover f) (hf' : IsProjectiveCover f') : Nonempty (↥f.ker ≃ₗ[R] ↥f'.ker)

The kernel of a projective cover is well defined. The equivalence of covering modules of TauCeti.IsProjectiveCover.exists_linearEquiv carries the kernel of one cover onto the kernel of the other, so the syzygy that a projective cover of M cuts out does not depend on the cover.

theorem TauCeti.IsProjectiveCover.comp {R : Type u} {M : Type v} {P : Type w} [Semiring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {N : Type u_1} [AddCommMonoid N] [Module R N] {f : P →ₗ[R] M} (hf : IsProjectiveCover f) {g : M →ₗ[R] N} (hg : Function.Surjective ⇑g) (hgker : IsSuperfluous g.ker) : IsProjectiveCover (g ∘ₗ f)

Composing a projective cover with a surjection whose kernel is superfluous again gives a projective cover.

theorem TauCeti.IsProjectiveCover.ker_le_jacobson {R : Type u} {M : Type v} {P : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {f : P →ₗ[R] M} (hf : IsProjectiveCover f) : f.ker ≤ Module.jacobson R P

The kernel of a projective cover lies in the radical of the covering module, being superfluous.

Quotients

The quotient maps of a projective module are the source of concrete projective covers. Since R is free, hence projective, R ⧸ I is covered by R exactly when the left ideal I is small in R, that is contained in the Jacobson radical; over a local ring this covers the residue field by R.

@[simp]

theorem TauCeti.isProjectiveCover_mkQ_iff {R : Type u} {P : Type w} [Ring R] [AddCommGroup P] [Module R P] [Module.Projective R P] {N : Submodule R P} : IsProjectiveCover N.mkQ ↔ IsSuperfluous N

When the quotient map of a projective module is a projective cover. The quotient map P →ₗ[R] P ⧸ N of a projective module is a projective cover precisely when N is superfluous.

theorem TauCeti.isProjectiveCover_mkQ_iff_le_jacobson {R : Type u} {P : Type w} [Ring R] [AddCommGroup P] [Module R P] [Module.Projective R P] [IsCoatomic (Submodule R P)] {N : Submodule R P} : IsProjectiveCover N.mkQ ↔ N ≤ Module.jacobson R P

Over a module with coatomic submodule lattice the quotient map of a projective module is a projective cover precisely when the submodule divided out lies in the radical. For the regular module this says that R →ₗ[R] R ⧸ I is a projective cover precisely when I ≤ Ring.jacobson R.

theorem TauCeti.isProjectiveCover_mkQ_smul_top_of_isNilpotent {R : Type u} {P : Type w} [Ring R] [AddCommGroup P] [Module R P] [Module.Projective R P] {I : Ideal R} (hI : IsNilpotent I) : IsProjectiveCover (I • ⊤).mkQ

The top of a projective module modulo a nilpotent ideal. If I is nilpotent, the quotient map P →ₗ[R] P ⧸ I • P of a projective module is a projective cover. Over a semiprimary ring this covers the radical top P ⧸ J • P by P.

A projective cover is invisible to a semisimple target

theorem TauCeti.IsProjectiveCover.exists_comp_eq {R : Type u} {M : Type v} {P : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {T : Type u_1} [AddCommGroup T] [Module R T] [IsSemisimpleModule R T] {f : P →ₗ[R] M} (hf : IsProjectiveCover f) (φ : P →ₗ[R] T) : ∃ (ψ : M →ₗ[R] T), ψ ∘ₗ f = φ

Every map from the source of a projective cover into a semisimple module factors through the cover: the kernel of the cover is superfluous, hence contained in the radical of the source, which the map annihilates.

noncomputable def TauCeti.IsProjectiveCover.homEquivOfIsSemisimpleModule {R : Type u} {M : Type v} {P : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {T : Type u_1} [AddCommGroup T] [Module R T] [IsSemisimpleModule R T] (k : Type u_2) [Semiring k] [Module k T] [SMulCommClass R k T] {f : P →ₗ[R] M} (hf : IsProjectiveCover f) : (M →ₗ[R] T) ≃ₗ[k] P →ₗ[R] T

A projective cover is invisible to a semisimple target. Precomposition with a projective cover f : P →ₗ[R] M is a k-linear isomorphism from Hom_R(M, T) to Hom_R(P, T) for every semisimple R-module T with commuting R- and k-actions. In particular, k can be the endomorphism ring Module.End R T, acting by postcomposition. The map is injective because f is onto, and surjective by TauCeti.IsProjectiveCover.exists_comp_eq.

Compare TauCeti.homCongrRight, which transports a hom space along an isomorphism of its target: here the map on the source side is only a cover, and it is the semisimplicity of T that makes the induced map on hom spaces invertible.

Equations

• TauCeti.IsProjectiveCover.homEquivOfIsSemisimpleModule k hf = LinearEquiv.ofBijective (LinearMap.lcomp k T f) ⋯

@[simp]

theorem TauCeti.IsProjectiveCover.homEquivOfIsSemisimpleModule_apply {R : Type u} {M : Type v} {P : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {T : Type u_1} [AddCommGroup T] [Module R T] [IsSemisimpleModule R T] {k : Type u_2} [Semiring k] [Module k T] [SMulCommClass R k T] {f : P →ₗ[R] M} (hf : IsProjectiveCover f) (ψ : M →ₗ[R] T) : (homEquivOfIsSemisimpleModule k hf) ψ = ψ ∘ₗ f

@[simp]

theorem TauCeti.IsProjectiveCover.homEquivOfIsSemisimpleModule_symm_comp {R : Type u} {M : Type v} {P : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup P] [Module R P] {T : Type u_1} [AddCommGroup T] [Module R T] [IsSemisimpleModule R T] {k : Type u_2} [Semiring k] [Module k T] [SMulCommClass R k T] {f : P →ₗ[R] M} (hf : IsProjectiveCover f) (φ : P →ₗ[R] T) : (homEquivOfIsSemisimpleModule k hf).symm φ ∘ₗ f = φ

The inverse of TauCeti.IsProjectiveCover.homEquivOfIsSemisimpleModule is the factorization through the cover.