Homogeneous splitting of a finite identity decomposition

Taking degree zero in ∑ gⱼ fⱼ = 1 gives a finite sum of endomorphisms of the graded source. In a local endomorphism ring, one summand is a unit. The corresponding homogeneous map splits into one shifted target. If that target also has local endomorphisms, the split map is an isomorphism.

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.outPart {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (X Y : C) (d : ℤ) (f : X ⟶ Y) : { obj := X, degree := 0 } ⟶ { obj := Y, degree := -d }

The degree d component as a degree-zero map into the shift by -d.

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.inPart {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) (X Y : C) (d : ℤ) (g : Y ⟶ X) : { obj := Y, degree := -d } ⟶ { obj := X, degree := 0 }

The opposite-degree component returning from that shifted target.

theorem MagnitudeConjecture.GradedCategory.HomGrading.sum_part_composites_eq_id {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) {ι : Type z} (s : Finset ι) (X : C) (Y : ι → C) (f : (j : ι) → X ⟶ Y j) (g : (j : ι) → Y j ⟶ X) (hsum : ∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) (g j) = CategoryTheory.CategoryStruct.id X) : ∑ j ∈ s, ∑ d ∈ DFinsupp.support ((G.decomposeHom X (Y j)) (f j)), CategoryTheory.CategoryStruct.comp (G.outPart X (Y j) d (f j)) (G.inPart X (Y j) d (g j)) = CategoryTheory.CategoryStruct.id { obj := X, degree := 0 }

The actual graded identity obtained by taking degree zero of an ungraded finite identity decomposition.

theorem MagnitudeConjecture.GradedCategory.HomGrading.exists_splitMono_part_of_identity {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) {ι : Type z} (s : Finset ι) (X : C) (Y : ι → C) (f : (j : ι) → X ⟶ Y j) (g : (j : ι) → Y j ⟶ X) (hsum : ∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) (g j) = CategoryTheory.CategoryStruct.id X) (hlocal : IsLocalRing (CategoryTheory.End { obj := X, degree := 0 })) : ∃ j ∈ s, ∃ (d : ℤ), CategoryTheory.IsSplitMono (G.outPart X (Y j) d (f j))

One homogeneous component splits when the graded source endomorphism ring is local. Neither a covering hypothesis nor an orbit-density theorem is needed for this conclusion.

theorem MagnitudeConjecture.GradedCategory.HomGrading.exists_iso_shift_of_identity {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) {ι : Type z} (s : Finset ι) (X : C) (Y : ι → C) (f : (j : ι) → X ⟶ Y j) (g : (j : ι) → Y j ⟶ X) (hsum : ∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) (g j) = CategoryTheory.CategoryStruct.id X) (hlocal : IsLocalRing (CategoryTheory.End { obj := X, degree := 0 })) (htarget : ∀ j ∈ s, ∀ (d : ℤ), IsLocalRing (CategoryTheory.End { obj := Y j, degree := -d })) : ∃ j ∈ s, ∃ (d : ℤ), Nonempty ({ obj := X, degree := 0 } ≅ { obj := Y j, degree := -d })

With local target endomorphisms, the split component identifies the graded source with one shift of a target in its ungraded decomposition.

theorem MagnitudeConjecture.GradedCategory.HomGrading.exists_iso_shift_of_identity_of_local_targets {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (G : HomGrading k C) {ι : Type z} (s : Finset ι) (X : C) (Y : ι → C) (f : (j : ι) → X ⟶ Y j) (g : (j : ι) → Y j ⟶ X) (hsum : ∑ j ∈ s, CategoryTheory.CategoryStruct.comp (f j) (g j) = CategoryTheory.CategoryStruct.id X) (hlocal : IsLocalRing (CategoryTheory.End { obj := X, degree := 0 })) (htarget : ∀ j ∈ s, IsLocalRing (CategoryTheory.End (Y j))) : ∃ j ∈ s, ∃ (d : ℤ), Nonempty ({ obj := X, degree := 0 } ≅ { obj := Y j, degree := -d })

Ungraded target locality suffices: the homogeneous inverse theorem makes each shifted target's degree-zero endomorphism ring local automatically.