Factorization through injective objects

This file records the small categorical fragment of injective-stable Hom needed by the finite-functor Auslander--Reiten argument.

structure MagnitudeConjecture.InjectiveStable.FactorsThroughInjective {D : Type u} [CategoryTheory.Category.{v, u} D] {U V : D} (f : U ⟶ V) : Type (max u v)

A morphism factors through an injective object.

• middle : D
• injective : CategoryTheory.Injective self.middle
• left : U ⟶ self.middle
• right : self.middle ⟶ V
• fac : CategoryTheory.CategoryStruct.comp self.left self.right = f

theorem MagnitudeConjecture.InjectiveStable.idempotent_eq_zero_of_factorsThroughInjective {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.IsIdempotentComplete D] {T : D} (a : T ⟶ T) (haa : CategoryTheory.CategoryStruct.comp a a = a) (hfac : Nonempty (FactorsThroughInjective a)) (hzero : ∀ {I : D} [CategoryTheory.Injective I] (a : CategoryTheory.Retract I T), CategoryTheory.Limits.IsZero I) : a = 0

An idempotent which factors through an injective vanishes if its source has no nonzero injective retract.

noncomputable def MagnitudeConjecture.InjectiveStable.FactorsThroughInjective.zero {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] {X Y : D} : FactorsThroughInjective 0

The zero map factors through the zero injective.

noncomputable def MagnitudeConjecture.InjectiveStable.FactorsThroughInjective.add {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] {X Y : D} {f g : X ⟶ Y} (hf : FactorsThroughInjective f) (hg : FactorsThroughInjective g) : FactorsThroughInjective (f + g)

Injective factorizations are closed under addition.

def MagnitudeConjecture.InjectiveStable.FactorsThroughInjective.smul {D : Type u} [CategoryTheory.Category.{v, u} D] {k : Type uk} [Field k] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] {X Y : D} {f : X ⟶ Y} (a : k) (hf : FactorsThroughInjective f) : FactorsThroughInjective (a • f)

Injective factorizations are closed under scalar multiplication.

def MagnitudeConjecture.InjectiveStable.FactorsThroughInjective.postcomp {D : Type u} [CategoryTheory.Category.{v, u} D] {X Y Z : D} {f : X ⟶ Y} (hf : FactorsThroughInjective f) (g : Y ⟶ Z) : FactorsThroughInjective (CategoryTheory.CategoryStruct.comp f g)

Postcomposition preserves injective factorization.

def MagnitudeConjecture.InjectiveStable.FactorsThroughInjective.precomp {D : Type u} [CategoryTheory.Category.{v, u} D] {W X Y : D} (g : W ⟶ X) {f : X ⟶ Y} (hf : FactorsThroughInjective f) : FactorsThroughInjective (CategoryTheory.CategoryStruct.comp g f)

Precomposition preserves injective factorization.

def MagnitudeConjecture.InjectiveStable.factorSubmodule {D : Type u} [CategoryTheory.Category.{v, u} D] {k : Type uk} [Field k] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X Y : D) : Submodule k (X ⟶ Y)

The linear subspace of morphisms which factor through injectives.

@[reducible, inline]

abbrev MagnitudeConjecture.InjectiveStable.Hom {D : Type u} [CategoryTheory.Category.{v, u} D] {k : Type uk} [Field k] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X Y : D) : Type v

The injective-stable Hom space.

@[reducible, inline]

abbrev MagnitudeConjecture.InjectiveStable.mk {D : Type u} [CategoryTheory.Category.{v, u} D] {k : Type uk} [Field k] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {X Y : D} : (X ⟶ Y) →ₗ[k] Hom X Y

The class of an ordinary morphism in injective-stable Hom.

def MagnitudeConjecture.InjectiveStable.postcomp {D : Type u} [CategoryTheory.Category.{v, u} D] {k : Type uk} [Field k] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X : D) {Y Z : D} (g : Y ⟶ Z) : Hom X Y →ₗ[k] Hom X Z

Postcomposition on injective-stable Hom.

@[simp]

theorem MagnitudeConjecture.InjectiveStable.postcomp_mk {D : Type u} [CategoryTheory.Category.{v, u} D] {k : Type uk} [Field k] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X : D) {Y Z : D} (g : Y ⟶ Z) (f : X ⟶ Y) : (postcomp X g) (mk f) = mk (CategoryTheory.CategoryStruct.comp f g)

def MagnitudeConjecture.InjectiveStable.precomp {D : Type u} [CategoryTheory.Category.{v, u} D] {k : Type uk} [Field k] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {W X : D} (g : W ⟶ X) (Y : D) : Hom X Y →ₗ[k] Hom W Y

Precomposition on injective-stable Hom.

@[simp]

theorem MagnitudeConjecture.InjectiveStable.precomp_mk {D : Type u} [CategoryTheory.Category.{v, u} D] {k : Type uk} [Field k] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {W X : D} (g : W ⟶ X) (Y : D) (f : X ⟶ Y) : (precomp g Y) (mk f) = mk (CategoryTheory.CategoryStruct.comp g f)

theorem MagnitudeConjecture.InjectiveStable.injective_of_id_factorsThroughInjective {D : Type u} [CategoryTheory.Category.{v, u} D] (X : D) (h : FactorsThroughInjective (CategoryTheory.CategoryStruct.id X)) : CategoryTheory.Injective X

If the identity factors through an injective, then the object itself is injective.

theorem MagnitudeConjecture.InjectiveStable.mk_id_ne_zero {D : Type u} [CategoryTheory.Category.{v, u} D] {k : Type uk} [Field k] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (X : D) (hX : ¬CategoryTheory.Injective X) : mk (CategoryTheory.CategoryStruct.id X) ≠ 0

A noninjective object has a nonzero injective-stable identity class.