Almost-split maps and minimality after taking homogeneous components #
theorem
MagnitudeConjecture.GradedCategory.HomGrading.part_comp_right_homogeneous
{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 Z : C}
{d : ℤ}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(hg : g ∈ G.component Y Z d)
(t : ℤ)
:
If the last factor is homogeneous, one component of the first factor computes any prescribed component of their composite.
theorem
MagnitudeConjecture.GradedCategory.HomGrading.isSplitEpi_of_underlying_isSplitEpi
{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 : DegreeObject G}
(f : X ⟶ Y)
(hf : CategoryTheory.IsSplitEpi ↑f)
:
CategoryTheory.IsSplitEpi f
A section of a homogeneous map can be replaced by its opposite-degree component.
theorem
MagnitudeConjecture.GradedCategory.HomGrading.isSplitEpi_iff_underlying
{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 : DegreeObject G}
(f : X ⟶ Y)
:
CategoryTheory.IsSplitEpi f ↔ CategoryTheory.IsSplitEpi ↑f
Forgetting degrees preserves and reflects whether a homogeneous map splits.
theorem
MagnitudeConjecture.GradedCategory.HomGrading.rightAlmostSplit_of_underlying
{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 : DegreeObject G}
(f : X ⟶ Y)
(hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit ↑f)
:
An ungraded almost-split map remains almost split in the degree category when the given map is homogeneous.
theorem
MagnitudeConjecture.GradedCategory.HomGrading.rightMinimal_of_underlying
{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 : DegreeObject G}
(f : X ⟶ Y)
(hf : QuotientSubmoduleEquidistribution.IsRightMinimal ↑f)
:
Right minimality passes because a homogeneous invertible endomorphism has a homogeneous inverse.