Categorical injective envelopes

An injective envelope is an injective monomorphism which is left minimal. This file records the direct dual of the projective-cover calculus already used in the formalization and relates left minimality to essential monomorphisms.

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

An injective presentation whose monomorphism is left minimal.

• J : C
• injective : Injective self.J
• f : X ⟶ self.J
• mono : Mono self.f
• leftMinimal : QuotientSubmoduleEquidistribution.IsLeftMinimal self.f

instance MagnitudeConjecture.MinimalInjectivePresentation.instInjectiveJ {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (I : MinimalInjectivePresentation X) : CategoryTheory.Injective I.J

instance MagnitudeConjecture.MinimalInjectivePresentation.instMonoF {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (I : MinimalInjectivePresentation X) : CategoryTheory.Mono I.f

def MagnitudeConjecture.MinimalInjectivePresentation.preIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (I : MinimalInjectivePresentation X) (e : Y ≅ X) : MinimalInjectivePresentation Y

Precomposing the envelope map with an isomorphism gives a minimal injective presentation of the new source.

noncomputable def MagnitudeConjecture.MinimalInjectivePresentation.objectIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (I J : MinimalInjectivePresentation X) : I.J ≅ J.J

The injective targets of two minimal injective presentations of the same object are isomorphic compatibly with their envelope maps.

theorem MagnitudeConjecture.MinimalInjectivePresentation.comp_objectIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (I J : MinimalInjectivePresentation X) : CategoryTheory.CategoryStruct.comp I.f (I.objectIso J).hom = J.f

theorem MagnitudeConjecture.MinimalInjectivePresentation.comp_objectIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (I J : MinimalInjectivePresentation X) {Z : C} (h : J.J ⟶ Z) : CategoryTheory.CategoryStruct.comp I.f (CategoryTheory.CategoryStruct.comp (I.objectIso J).hom h) = CategoryTheory.CategoryStruct.comp J.f h

noncomputable def MagnitudeConjecture.MinimalInjectivePresentation.objectIsoOfSourceIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (I : MinimalInjectivePresentation X) (J : MinimalInjectivePresentation Y) (e : X ≅ Y) : I.J ≅ J.J

Minimal injective presentations of isomorphic sources have isomorphic injective targets.

theorem MagnitudeConjecture.MinimalInjectivePresentation.comp_objectIsoOfSourceIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (I : MinimalInjectivePresentation X) (J : MinimalInjectivePresentation Y) (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp I.f (I.objectIsoOfSourceIso J e).hom = CategoryTheory.CategoryStruct.comp e.hom J.f

theorem MagnitudeConjecture.MinimalInjectivePresentation.comp_objectIsoOfSourceIso_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (I : MinimalInjectivePresentation X) (J : MinimalInjectivePresentation Y) (e : X ≅ Y) {Z : C} (h : J.J ⟶ Z) : CategoryTheory.CategoryStruct.comp I.f (CategoryTheory.CategoryStruct.comp (I.objectIsoOfSourceIso J e).hom h) = CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp J.f h)

theorem MagnitudeConjecture.isLeftMinimal_of_mono_nonzero_of_local_end {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X I : C} [IsLocalRing (CategoryTheory.End I)] (f : X ⟶ I) [CategoryTheory.Mono f] (hf : f ≠ 0) : QuotientSubmoduleEquidistribution.IsLeftMinimal f

A nonzero monomorphism into an object with local endomorphism ring is left minimal.

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

A two-step minimal injective presentation consists of injective envelopes of an object and of the cokernel of its envelope.

• augmentation : MinimalInjectivePresentation X
• cosyzygyPresentation : MinimalInjectivePresentation (CategoryTheory.Limits.cokernel self.augmentation.f)

noncomputable def MagnitudeConjecture.TwoStepMinimalInjectivePresentation.differential {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X : C} (I : TwoStepMinimalInjectivePresentation X) : I.augmentation.J ⟶ I.cosyzygyPresentation.J

The first injective differential I₀ ⟶ I₁.

@[simp]

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

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

The associated exact injective complex X ⟶ I₀ ⟶ I₁.

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

The stored envelope of the first cosyzygy certifies exactness of the two-step injective presentation.

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

A monomorphism is essential if monicity after postcomposition forces monicity of the postcomposed morphism.

theorem MagnitudeConjecture.isEssentialMono_of_isLeftMinimal {C : Type u} [CategoryTheory.Category.{v, u} C] {X I : C} [CategoryTheory.Injective I] (f : X ⟶ I) [CategoryTheory.Mono f] (hmin : QuotientSubmoduleEquidistribution.IsLeftMinimal f) : IsEssentialMono f

A left-minimal monomorphism into an injective object is essential.

theorem MagnitudeConjecture.isEssentialMono_of_mono_nonzero_of_injective_local_end {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X I : C} [CategoryTheory.Injective I] [IsLocalRing (CategoryTheory.End I)] (f : X ⟶ I) [CategoryTheory.Mono f] (hf : f ≠ 0) : IsEssentialMono f

A nonzero monomorphism into an injective object with local endomorphism ring is an essential monomorphism.

theorem MagnitudeConjecture.isLeftMinimal_of_isEssentialMono {C : Type u} [CategoryTheory.Category.{v, u} C] {X I : C} [CategoryTheory.Injective I] (f : X ⟶ I) (hessential : IsEssentialMono f) (hendo : ∀ (e : I ⟶ I), CategoryTheory.Mono e → CategoryTheory.IsIso e) : QuotientSubmoduleEquidistribution.IsLeftMinimal f

An essential monomorphism into an injective object is left minimal when monic endomorphisms of the injective target are invertible.

theorem MagnitudeConjecture.isEssentialMono_iff_isLeftMinimal {C : Type u} [CategoryTheory.Category.{v, u} C] {X I : C} [CategoryTheory.Injective I] (f : X ⟶ I) [CategoryTheory.Mono f] : (∀ (e : I ⟶ I), CategoryTheory.Mono e → CategoryTheory.IsIso e) → (IsEssentialMono f ↔ QuotientSubmoduleEquidistribution.IsLeftMinimal f)

For an injective target whose monic endomorphisms are invertible, categorical left minimality is equivalent to essentiality.

theorem MagnitudeConjecture.exists_factor_thru_of_isEssentialMono_of_simple {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X I S : C} (f : X ⟶ I) (hessential : IsEssentialMono f) [CategoryTheory.Simple S] (s : S ⟶ I) [CategoryTheory.Mono s] (hs : s ≠ 0) : ∃ (t : S ⟶ X), CategoryTheory.CategoryStruct.comp t f = s

A nonzero simple subobject of the target of an essential monomorphism is already contained in its source. This is the categorical form of the socle-intersection property of an injective envelope.

theorem MagnitudeConjecture.simple_comp_cokernel_π_eq_zero_of_isEssentialMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X I S : C} (f : X ⟶ I) (hessential : IsEssentialMono f) [CategoryTheory.Simple S] (s : S ⟶ I) : CategoryTheory.CategoryStruct.comp s (CategoryTheory.Limits.cokernel.π f) = 0

Every map from a simple object into an essential extension lands in the essential subobject. Equivalently, its composite with the canonical cokernel projection vanishes.

theorem MagnitudeConjecture.isEssentialMono_of_simple_factors_of_exists_simple_subobject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L F : C} [CategoryTheory.Simple L] (l : L ⟶ F) [CategoryTheory.Mono l] (hsimple : ∀ {K : C} (i : K ⟶ F) [CategoryTheory.Mono i], ¬CategoryTheory.Limits.IsZero K → ∃ (T : C) (s : T ⟶ K), CategoryTheory.Simple T ∧ CategoryTheory.Mono s) (hfactor : ∀ {T : C} [CategoryTheory.Simple T] (t : T ⟶ F) [CategoryTheory.Mono t], t ≠ 0 → ∃ (a : T ⟶ L), CategoryTheory.CategoryStruct.comp a l = t) : IsEssentialMono l

A simple subobject through which every simple subobject factors is essential, provided every nonzero subobject contains a simple subobject.

theorem MagnitudeConjecture.isEssentialMono_of_simple_factors {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {L F : C} [CategoryTheory.IsArtinianObject F] [CategoryTheory.Simple L] (l : L ⟶ F) [CategoryTheory.Mono l] (hfactor : ∀ {T : C} [CategoryTheory.Simple T] (t : T ⟶ F) [CategoryTheory.Mono t], t ≠ 0 → ∃ (a : T ⟶ L), CategoryTheory.CategoryStruct.comp a l = t) : IsEssentialMono l

In an Artinian object, a simple subobject containing every simple subobject is essential.

theorem MagnitudeConjecture.leftMinimal_unop {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : Cᵒᵖ} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsRightMinimal f) : QuotientSubmoduleEquidistribution.IsLeftMinimal f.unop

Right minimality becomes left minimality after taking the opposite morphism.