Mixed split-component lifting between chosen meshes

This file proves the left-mesh-to-right-mesh case of Iyama, Tau-categories I, 3.5.2(1)(ii). It realizes the right-tau core of a chosen left mesh from finite Krull--Schmidt decomposition and mesh compatibility, then reduces mixed split lifting to the right-right theorem. The construction is entirely categorical.

The precise mixed interface

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.shortComplexBiproductHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] {S R : J → CategoryTheory.ShortComplex C} (φ : (j : J) → S j ⟶ R j) : shortComplexBiproduct S ⟶ shortComplexBiproduct R

The componentwise biproduct of a finite family of short-complex morphisms.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.isIso_shortComplexBiproductHom_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] {S R : J → CategoryTheory.ShortComplex C} (φ : (j : J) → S j ⟶ R j) (hφ : ∀ (j : J), CategoryTheory.IsIso (φ j).τ₃) : CategoryTheory.IsIso (shortComplexBiproductHom φ).τ₃

A componentwise biproduct morphism is invertible in degree three when all of its degree-three components are invertible.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.isSplitMono_shortComplexBiproductHom_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type w} [Fintype J] {S R : J → CategoryTheory.ShortComplex C} (φ : (j : J) → S j ⟶ R j) (hφ : ∀ (j : J), CategoryTheory.IsSplitMono (φ j).τ₁) : CategoryTheory.IsSplitMono (shortComplexBiproductHom φ).τ₁

A componentwise biproduct morphism is split monic in degree one when all of its degree-one components are split monic.

structure QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.RightCorePiece {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (A : Ind) : Type (max u v)

A right-tau piece mapping to the left mesh of one indecomposable, with an invertible map on third terms.

• S : CategoryTheory.ShortComplex C
• rightTau : RightTauSequence self.S
• inclusion : self.S ⟶ T.leftMesh (T.obj A)
• third_isIso : CategoryTheory.IsIso self.inclusion.τ₃

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.rightCorePiece {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (A : Ind) : RightCorePiece T A

For a noninjective label use the compatible right mesh. For an injective label use the zero right mesh; both source and target third terms are then zero.

structure QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.RightCoreDecomposition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (X : C) : Type (max u v)

A right tau-sequence mapping into a chosen left mesh, and exhausting its third term up to isomorphism. This packages Iyama's decomposition [X) ≅ [I) ⊕ (X₃] at exactly the strength needed for split lifting.

• S : CategoryTheory.ShortComplex C
• rightTau : RightTauSequence self.S
• inclusion : self.S ⟶ T.leftMesh X
• third_isIso : CategoryTheory.IsIso self.inclusion.τ₃

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.exists_rightCoreDecomposition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (X : C) : Nonempty (RightCoreDecomposition T X)

Finite Krull--Schmidt decomposition and mesh compatibility construct the right core of every chosen left mesh.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.isSplitEpi_of_isSplitEpi_precomp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (r : X ⟶ Y) (f : Y ⟶ Z) [CategoryTheory.IsSplitEpi (CategoryTheory.CategoryStruct.comp r f)] : CategoryTheory.IsSplitEpi f

A split-epic composite makes its second factor split epic.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.isSplitMono_of_isSplitMono_postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (r : Y ⟶ Z) [CategoryTheory.IsSplitMono (CategoryTheory.CategoryStruct.comp f r)] : CategoryTheory.IsSplitMono f

A split-monic composite makes its first factor split monic.

structure QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.LeftReplacement {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (A : Ind) : Type (max u v)

A left tau-sequence receiving a map from one indecomposable right mesh, split monic at the left endpoint.

• S : CategoryTheory.ShortComplex C
• leftTau : LeftTauSequence self.S
• projection : T.rightMesh (T.obj A) ⟶ self.S
• first_splitMono : CategoryTheory.IsSplitMono self.projection.τ₁

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.leftReplacement {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (A : Ind) : LeftReplacement T A

A nonprojective label uses mesh compatibility. At a projective boundary the zero chain map is split monic in degree one because its source is zero.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.splitEpi_components_of_leftMesh_hom_rightMesh {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (X Y : C) (phi : T.leftMesh X ⟶ T.rightMesh Y) (hphi₃ : CategoryTheory.IsSplitEpi phi.τ₃) : CategoryTheory.IsSplitEpi phi.τ₁ ∧ CategoryTheory.IsSplitEpi phi.τ₂

Mixed left-to-right split lifting, Tau I, 3.5.2(1)(ii), for the chosen meshes of a finite tau category.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.splitMono_components_of_leftMesh_hom_rightMesh {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (X Y : C) (phi : T.leftMesh X ⟶ T.rightMesh Y) (hphi₁ : CategoryTheory.IsSplitMono phi.τ₁) : CategoryTheory.IsSplitMono phi.τ₂ ∧ CategoryTheory.IsSplitMono phi.τ₃

Exact dual mixed lifting: a chain map from a chosen left mesh to a chosen right mesh which is split monic at the left endpoint is split monic in the other two degrees.

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.HasMixedSplitEpiLifting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) : Prop

The mixed split-lifting statement, Tau I, 3.5.2(1)(ii), packaged as a property of the chosen finite tau-category meshes.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.hasMixedSplitEpiLifting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) : HasMixedSplitEpiLifting T

The finite tau-category data prove the mixed split-lifting interface.

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.HasMixedSplitMonoLifting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) : Prop

The dual mixed split-lifting interface.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.hasMixedSplitMonoLifting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) : HasMixedSplitMonoLifting T

Finite tau-category data prove the dual mixed split-lifting interface.