Categorical projective covers

A minimal projective presentation is a projective epimorphism which is right minimal. This file records its transport and uniqueness calculus and relates right minimality to the essential-epimorphism characterization of projective covers.

theorem MagnitudeConjecture.projective_of_retract {C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : C} (hP : CategoryTheory.Projective P) (i : Q ⟶ P) (r : P ⟶ Q) (hir : CategoryTheory.CategoryStruct.comp i r = CategoryTheory.CategoryStruct.id Q) : CategoryTheory.Projective Q

A retract of a projective object is projective.

structure MagnitudeConjecture.MinimalProjectivePresentation {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) extends CategoryTheory.ProjectivePresentation X : Type (max u v)

A projective presentation whose epimorphism is right minimal.

• p : C
• projective : Projective self.p
• f : self.p ⟶ X
• epi : Epi self.f
• rightMinimal : QuotientSubmoduleEquidistribution.IsRightMinimal self.f

instance MagnitudeConjecture.MinimalProjectivePresentation.instProjectiveP {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P : MinimalProjectivePresentation X) : CategoryTheory.Projective P.p

instance MagnitudeConjecture.MinimalProjectivePresentation.instEpiF {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P : MinimalProjectivePresentation X) : CategoryTheory.Epi P.f

def MagnitudeConjecture.MinimalProjectivePresentation.postIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (P : MinimalProjectivePresentation X) (e : X ≅ Y) : MinimalProjectivePresentation Y

Postcomposing the cover map with an isomorphism gives a minimal projective presentation of the new target.

noncomputable def MagnitudeConjecture.MinimalProjectivePresentation.preIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Preadditive C] {Z : C} (P : MinimalProjectivePresentation X) (e : Z ≅ P.p) : MinimalProjectivePresentation X

Precomposing a projective cover by an isomorphism gives the same minimal projective presentation in new source coordinates.

noncomputable def MagnitudeConjecture.MinimalProjectivePresentation.objectIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P Q : MinimalProjectivePresentation X) : P.p ≅ Q.p

The projective sources of two minimal projective presentations of the same object are isomorphic compatibly with their cover maps.

theorem MagnitudeConjecture.MinimalProjectivePresentation.objectIso_hom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P Q : MinimalProjectivePresentation X) : CategoryTheory.CategoryStruct.comp (P.objectIso Q).hom Q.f = P.f

theorem MagnitudeConjecture.MinimalProjectivePresentation.objectIso_hom_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P Q : MinimalProjectivePresentation X) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.objectIso Q).hom (CategoryTheory.CategoryStruct.comp Q.f h) = CategoryTheory.CategoryStruct.comp P.f h

noncomputable def MagnitudeConjecture.MinimalProjectivePresentation.objectIsoOfTargetIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (P : MinimalProjectivePresentation X) (Q : MinimalProjectivePresentation Y) (e : X ≅ Y) : P.p ≅ Q.p

Minimal projective presentations of isomorphic targets have isomorphic projective sources.

theorem MagnitudeConjecture.MinimalProjectivePresentation.objectIsoOfTargetIso_hom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (P : MinimalProjectivePresentation X) (Q : MinimalProjectivePresentation Y) (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp (P.objectIsoOfTargetIso Q e).hom Q.f = CategoryTheory.CategoryStruct.comp P.f e.hom

theorem MagnitudeConjecture.MinimalProjectivePresentation.objectIsoOfTargetIso_hom_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (P : MinimalProjectivePresentation X) (Q : MinimalProjectivePresentation Y) (e : X ≅ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.objectIsoOfTargetIso Q e).hom (CategoryTheory.CategoryStruct.comp Q.f h) = CategoryTheory.CategoryStruct.comp P.f (CategoryTheory.CategoryStruct.comp e.hom h)

structure MagnitudeConjecture.TwoStepMinimalProjectivePresentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (X : C) : Type (max u v)

A two-step minimal projective presentation consists of projective covers of an object and of the kernel of its cover.

• augmentation : MinimalProjectivePresentation X
• syzygyPresentation : MinimalProjectivePresentation (CategoryTheory.Limits.kernel self.augmentation.f)

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.differential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P : TwoStepMinimalProjectivePresentation X) : P.syzygyPresentation.p ⟶ P.augmentation.p

The first differential P₁ ⟶ P₀.

@[simp]

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.differential_comp_augmentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P : TwoStepMinimalProjectivePresentation X) : CategoryTheory.CategoryStruct.comp P.differential P.augmentation.f = 0

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.presentationComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P : TwoStepMinimalProjectivePresentation X) : CategoryTheory.ShortComplex C

The associated exact projective complex P₁ ⟶ P₀ ⟶ X.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.presentationComplex_exact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P : TwoStepMinimalProjectivePresentation X) : P.presentationComplex.Exact

The stored cover of the first syzygy certifies exactness of the two-step projective presentation.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.augmentationObjectIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P Q : TwoStepMinimalProjectivePresentation X) : P.augmentation.p ≅ Q.augmentation.p

The compatible isomorphism between the augmentation sources of two two-step minimal projective presentations.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.kernelObjectIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P Q : TwoStepMinimalProjectivePresentation X) : CategoryTheory.Limits.kernel P.augmentation.f ≅ CategoryTheory.Limits.kernel Q.augmentation.f

The augmentation-source comparison induces the corresponding isomorphism between the first syzygies.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P Q : TwoStepMinimalProjectivePresentation X) : P.syzygyPresentation.p ≅ Q.syzygyPresentation.p

The compatible isomorphism between the first projective sources of two two-step minimal projective presentations.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIso_hom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P Q : TwoStepMinimalProjectivePresentation X) : CategoryTheory.CategoryStruct.comp (P.syzygyObjectIso Q).hom Q.syzygyPresentation.f = CategoryTheory.CategoryStruct.comp P.syzygyPresentation.f (P.kernelObjectIso Q).hom

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIso_hom_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P Q : TwoStepMinimalProjectivePresentation X) {Z : C} (h : CategoryTheory.Limits.kernel Q.augmentation.f ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.syzygyObjectIso Q).hom (CategoryTheory.CategoryStruct.comp Q.syzygyPresentation.f h) = CategoryTheory.CategoryStruct.comp P.syzygyPresentation.f (CategoryTheory.CategoryStruct.comp (P.kernelObjectIso Q).hom h)

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIso_hom_comp_differential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P Q : TwoStepMinimalProjectivePresentation X) : CategoryTheory.CategoryStruct.comp (P.syzygyObjectIso Q).hom Q.differential = CategoryTheory.CategoryStruct.comp P.differential (P.augmentationObjectIso Q).hom

The two compatible source isomorphisms intertwine the first differentials.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIso_hom_comp_differential_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (P Q : TwoStepMinimalProjectivePresentation X) {Z : C} (h : Q.augmentation.p ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.syzygyObjectIso Q).hom (CategoryTheory.CategoryStruct.comp Q.differential h) = CategoryTheory.CategoryStruct.comp P.differential (CategoryTheory.CategoryStruct.comp (P.augmentationObjectIso Q).hom h)

The two compatible source isomorphisms intertwine the first differentials.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.augmentationObjectIsoOfTargetIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (P : TwoStepMinimalProjectivePresentation X) (Q : TwoStepMinimalProjectivePresentation Y) (e : X ≅ Y) : P.augmentation.p ≅ Q.augmentation.p

The compatible isomorphism between augmentation sources when the presented targets are isomorphic.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.kernelObjectIsoOfTargetIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (P : TwoStepMinimalProjectivePresentation X) (Q : TwoStepMinimalProjectivePresentation Y) (e : X ≅ Y) : CategoryTheory.Limits.kernel P.augmentation.f ≅ CategoryTheory.Limits.kernel Q.augmentation.f

An isomorphism of presented targets and the induced augmentation-source isomorphism identify the first syzygies.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIsoOfTargetIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (P : TwoStepMinimalProjectivePresentation X) (Q : TwoStepMinimalProjectivePresentation Y) (e : X ≅ Y) : P.syzygyPresentation.p ≅ Q.syzygyPresentation.p

The compatible isomorphism between the first projective sources when the presented targets are isomorphic.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIsoOfTargetIso_hom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (P : TwoStepMinimalProjectivePresentation X) (Q : TwoStepMinimalProjectivePresentation Y) (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp (P.syzygyObjectIsoOfTargetIso Q e).hom Q.syzygyPresentation.f = CategoryTheory.CategoryStruct.comp P.syzygyPresentation.f (P.kernelObjectIsoOfTargetIso Q e).hom

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIsoOfTargetIso_hom_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (P : TwoStepMinimalProjectivePresentation X) (Q : TwoStepMinimalProjectivePresentation Y) (e : X ≅ Y) {Z : C} (h : CategoryTheory.Limits.kernel Q.augmentation.f ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.syzygyObjectIsoOfTargetIso Q e).hom (CategoryTheory.CategoryStruct.comp Q.syzygyPresentation.f h) = CategoryTheory.CategoryStruct.comp P.syzygyPresentation.f (CategoryTheory.CategoryStruct.comp (P.kernelObjectIsoOfTargetIso Q e).hom h)

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIsoOfTargetIso_hom_comp_differential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (P : TwoStepMinimalProjectivePresentation X) (Q : TwoStepMinimalProjectivePresentation Y) (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp (P.syzygyObjectIsoOfTargetIso Q e).hom Q.differential = CategoryTheory.CategoryStruct.comp P.differential (P.augmentationObjectIsoOfTargetIso Q e).hom

Isomorphic targets of two-step minimal projective presentations induce compatible isomorphisms of both projective sources.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.syzygyObjectIsoOfTargetIso_hom_comp_differential_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (P : TwoStepMinimalProjectivePresentation X) (Q : TwoStepMinimalProjectivePresentation Y) (e : X ≅ Y) {Z : C} (h : Q.augmentation.p ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.syzygyObjectIsoOfTargetIso Q e).hom (CategoryTheory.CategoryStruct.comp Q.differential h) = CategoryTheory.CategoryStruct.comp P.differential (CategoryTheory.CategoryStruct.comp (P.augmentationObjectIsoOfTargetIso Q e).hom h)

Isomorphic targets of two-step minimal projective presentations induce compatible isomorphisms of both projective sources.

noncomputable def MagnitudeConjecture.TwoStepMinimalProjectivePresentation.recoordinate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X P₀ P₁ : C} (P : TwoStepMinimalProjectivePresentation X) (e₀ : P₀ ≅ P.augmentation.p) (e₁ : P₁ ≅ P.syzygyPresentation.p) : TwoStepMinimalProjectivePresentation X

Replace both projective sources of a two-step minimal presentation by isomorphic coordinate objects.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.recoordinate_differential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X P₀ P₁ : C} (P : TwoStepMinimalProjectivePresentation X) (e₀ : P₀ ≅ P.augmentation.p) (e₁ : P₁ ≅ P.syzygyPresentation.p) : (P.recoordinate e₀ e₁).differential = CategoryTheory.CategoryStruct.comp e₁.hom (CategoryTheory.CategoryStruct.comp P.differential e₀.inv)

Recoordinating both projective sources conjugates the first differential by the two source isomorphisms.

def MagnitudeConjecture.IsEssentialEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop

An epimorphism is essential if epimorphicity of a composite ending in it forces epimorphicity of the first factor.

theorem MagnitudeConjecture.isEssentialEpi_of_isRightMinimal {C : Type u} [CategoryTheory.Category.{v, u} C] {P X : C} [CategoryTheory.Projective P] (f : P ⟶ X) [CategoryTheory.Epi f] (hmin : QuotientSubmoduleEquidistribution.IsRightMinimal f) : IsEssentialEpi f

A right-minimal epimorphism from a projective object is essential.

theorem MagnitudeConjecture.isRightMinimal_of_isEssentialEpi {C : Type u} [CategoryTheory.Category.{v, u} C] {P X : C} [CategoryTheory.Projective P] (f : P ⟶ X) (hessential : IsEssentialEpi f) (hendo : ∀ (e : P ⟶ P), CategoryTheory.Epi e → CategoryTheory.IsIso e) : QuotientSubmoduleEquidistribution.IsRightMinimal f

An essential epimorphism from a projective object is right minimal when epic endomorphisms of the projective source are invertible.

theorem MagnitudeConjecture.isEssentialEpi_iff_isRightMinimal {C : Type u} [CategoryTheory.Category.{v, u} C] {P X : C} [CategoryTheory.Projective P] (f : P ⟶ X) [CategoryTheory.Epi f] : (∀ (e : P ⟶ P), CategoryTheory.Epi e → CategoryTheory.IsIso e) → (IsEssentialEpi f ↔ QuotientSubmoduleEquidistribution.IsRightMinimal f)

For an epimorphism from a projective object whose epic endomorphisms are invertible, categorical right minimality is equivalent to essentiality.

theorem MagnitudeConjecture.MinimalProjectivePresentation.exists_splitEpi_factor {C : Type u} [CategoryTheory.Category.{v, u} C] {X Q : C} (P : MinimalProjectivePresentation X) [CategoryTheory.Projective Q] (q : Q ⟶ X) [CategoryTheory.Epi q] : ∃ (a : Q ⟶ P.p), CategoryTheory.IsSplitEpi a ∧ CategoryTheory.CategoryStruct.comp a P.f = q

A projective cover is a split summand of every projective epimorphism onto the same target, compatibly with the two epimorphisms.