Finite displayed decompositions into indecomposables

This small generic interface and its biproduct combiner are adapted from the Cartan formalization's ClosedRayChain/GenericFiniteness.lean at homological-conjectures commit eade4e75.

structure MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] (X : C) : Type (max u v)

A concrete finite biproduct decomposition into indecomposable objects.

• n : ℕ
• summand : Fin self.n → C
• indecomposable (j : Fin self.n) : CategoryTheory.Indecomposable (self.summand j)
• isoBiproduct : X ≅ ⨁ self.summand

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.singleton {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] (X : C) (hX : CategoryTheory.Indecomposable X) : FiniteIndecomposableDecomposition X

The one-term displayed decomposition of an indecomposable object.

noncomputable def MagnitudeConjecture.CategoryTheory.zeroIsoEmptyBiproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] (X : C) (hX : CategoryTheory.Limits.IsZero X) : X ≅ ⨁ fun (i : Fin 0) => i.elim0

The empty biproduct is isomorphic to every zero object.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] {X Y : C} (dX : FiniteIndecomposableDecomposition X) (dY : FiniteIndecomposableDecomposition Y) : FiniteIndecomposableDecomposition (X ⊞ Y)

Concatenate two displayed finite biproduct decompositions.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.ofIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] {X Y : C} (e : X ≅ Y) (d : FiniteIndecomposableDecomposition Y) : FiniteIndecomposableDecomposition X

Transport a displayed decomposition across an isomorphism.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.mapOfIndecomposable {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Limits.HasFiniteBiproducts D] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] (F : CategoryTheory.Functor C D) [F.Additive] {X : C} (d : FiniteIndecomposableDecomposition X) (h : ∀ (i : Fin d.n), CategoryTheory.Indecomposable (F.obj (d.summand i))) : FiniteIndecomposableDecomposition (F.obj X)

An additive functor carries a displayed finite indecomposable decomposition to one in the target whenever it preserves the indecomposability of the displayed summands.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.mapOpOfIndecomposable {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Limits.HasFiniteBiproducts D] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] (F : CategoryTheory.Functor Cᵒᵖ D) [F.Additive] {X : C} (d : FiniteIndecomposableDecomposition X) (h : ∀ (i : Fin d.n), CategoryTheory.Indecomposable (F.obj (Opposite.op (d.summand i)))) : FiniteIndecomposableDecomposition (F.obj (Opposite.op X))

An additive functor out of the opposite category carries a displayed finite indecomposable decomposition to the corresponding dual decomposition. Opposite passage turns the source biproduct, viewed as a coproduct, into a product; additivity then identifies the resulting product with the target biproduct.

theorem MagnitudeConjecture.CategoryTheory.finiteIndecomposableDecomposition_of_rank {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] (rank : C → ℕ) (zero_of_rank_eq_zero : ∀ (X : C), rank X = 0 → CategoryTheory.Limits.IsZero X) (rank_biprod : ∀ {X Y Z : C} (a : X ≅ Y ⊞ Z), rank X = rank Y + rank Z) (X : C) : Nonempty (FiniteIndecomposableDecomposition X)

A natural-number-valued rank which is positive on nonzero objects and additive across binary biproduct decompositions guarantees existence of a finite decomposition into indecomposable objects.

theorem MagnitudeConjecture.CategoryTheory.functor_essSurj_of_indec_dense {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] (decomposition : ∀ (Y : D), Nonempty (FiniteIndecomposableDecomposition Y)) (dense : ∀ (Y : D), CategoryTheory.Indecomposable Y → ∃ (X : C), Nonempty (F.obj X ≅ Y)) : F.EssSurj

An additive functor is essentially surjective if every target object has a finite indecomposable decomposition and every indecomposable target object has a lift.