Almost-split maps from pullbacks

Pulling back an epimorphism along a morphism which does not lift through it produces a right almost-split projection as soon as one right almost-split map to the endpoint lifts into the pullback.

noncomputable def MagnitudeConjecture.CategoryTheory.splitEpiComplementIsoKernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (g : X ⟶ Y) [CategoryTheory.IsSplitEpi g] (d : QuotientSubmoduleEquidistribution.SplitEpiComplement g) : d.complement ≅ CategoryTheory.Limits.kernel g

The complementary object attached to a split epimorphism is canonically isomorphic to its kernel. We keep this explicit bridge because split complements are convenient for counting indecomposable summands, whereas kernels are the objects naturally produced by pullback arguments.

theorem MagnitudeConjecture.CategoryTheory.splitMono_fst_or_snd_of_splitMono_to_biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y Z : C} [IsLocalRing (CategoryTheory.End X)] (f : X ⟶ Y ⊞ Z) [CategoryTheory.IsSplitMono f] : CategoryTheory.IsSplitMono (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst) ∨ CategoryTheory.IsSplitMono (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)

A split embedding of an object with local endomorphism ring into a binary biproduct splits through at least one coordinate. This is the two-summand Krull--Schmidt step, stated without choosing decompositions.

noncomputable def MagnitudeConjecture.CategoryTheory.pullbackIsoBiprodKernelOfFac {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P X Z : C} (q : P ⟶ Z) (h : X ⟶ Z) (s : P ⟶ X) (hs : CategoryTheory.CategoryStruct.comp s h = q) : CategoryTheory.Limits.pullback q h ≅ P ⊞ CategoryTheory.Limits.kernel h

If q : P ⟶ Z factors through h : X ⟶ Z, then its pullback along h is the direct sum of P and kernel h. The first summand is the graph of the chosen factorization.

def MagnitudeConjecture.CategoryTheory.endomorphismRingEquivOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} (e : X ≅ Y) : CategoryTheory.End X ≃+* CategoryTheory.End Y

Isomorphic objects have isomorphic endomorphism rings.

theorem MagnitudeConjecture.CategoryTheory.rightAlmostSplit_isRightMinimal_of_kernel_local {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {E Z : C} (f : E ⟶ Z) [CategoryTheory.Epi f] [IsLocalRing (CategoryTheory.End (CategoryTheory.Limits.kernel f))] (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) : QuotientSubmoduleEquidistribution.IsRightMinimal f

A right almost-split epimorphism is right minimal when the endomorphism ring of its kernel is local.

noncomputable def MagnitudeConjecture.CategoryTheory.pullbackCokernelKernelSourceIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {U P X : C} (g : U ⟶ P) [CategoryTheory.Mono g] (h : X ⟶ CategoryTheory.Limits.cokernel g) : U ≅ CategoryTheory.Limits.kernel (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.cokernel.π g) h)

The kernel of the pullback projection of a cokernel is canonically the source of the original monomorphism.

theorem MagnitudeConjecture.CategoryTheory.pullbackCokernelKernelSourceIso_hom_comp_kernel_ι_comp_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {U P X : C} (g : U ⟶ P) [CategoryTheory.Mono g] (h : X ⟶ CategoryTheory.Limits.cokernel g) : CategoryTheory.CategoryStruct.comp (pullbackCokernelKernelSourceIso g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.cokernel.π g) h)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.cokernel.π g) h)) = g

The canonical kernel identification respects the map into the projective object in the pullback square.

theorem MagnitudeConjecture.CategoryTheory.pullbackCokernelKernelSourceIso_hom_comp_kernel_ι_comp_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {U P X : C} (g : U ⟶ P) [CategoryTheory.Mono g] (h : X ⟶ CategoryTheory.Limits.cokernel g) {Z : C} (h✝ : P ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackCokernelKernelSourceIso g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.cokernel.π g) h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.cokernel.π g) h) h✝)) = CategoryTheory.CategoryStruct.comp g h✝

The canonical kernel identification respects the map into the projective object in the pullback square.

theorem MagnitudeConjecture.CategoryTheory.pullback_snd_isRightAlmostSplit_of_rightAlmostSplit_lifts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {P Z X B : C} (q : P ⟶ Z) [CategoryTheory.Epi q] (h : X ⟶ Z) (hnot : ¬∃ (a : X ⟶ P), CategoryTheory.CategoryStruct.comp a q = h) (d : B ⟶ X) (hd : QuotientSubmoduleEquidistribution.IsRightAlmostSplit d) (a : B ⟶ P) (ha : CategoryTheory.CategoryStruct.comp a q = CategoryTheory.CategoryStruct.comp d h) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.Limits.pullback.snd q h)

If q : P ⟶ Z is epic, h : X ⟶ Z does not lift through q, and a right almost-split map to X becomes liftable after composition with h, then the pullback projection to X is right almost split.