Homogeneous inverses and local graded endomorphisms #
An invertible homogeneous map has a homogeneous inverse of the opposite degree. In particular the degree-zero endomorphism ring is local whenever the ungraded endomorphism ring is local. This supplies the target locality in the homogeneous splitting argument.
theorem
MagnitudeConjecture.GradedCategory.HomGrading.inv_mem_opposite_degree
{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)
[CategoryTheory.IsIso f]
(hf : f ∈ G.component X Y d)
:
CategoryTheory.inv f ∈ G.component Y X (-d)
theorem
MagnitudeConjecture.GradedCategory.HomGrading.isIso_of_underlying_isIso
{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.IsIso ↑f]
:
CategoryTheory.IsIso f
Forgetting degrees reflects invertibility of homogeneous maps.
theorem
MagnitudeConjecture.GradedCategory.HomGrading.isUnit_of_underlying_isUnit
{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 : DegreeObject G}
(f : CategoryTheory.End X)
(hf :
IsUnit
(have this := ↑f;
this))
:
IsUnit f
theorem
MagnitudeConjecture.GradedCategory.HomGrading.localEnd_of_underlying_localEnd
{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 : DegreeObject G)
[IsLocalRing (CategoryTheory.End X.obj)]
:
IsLocalRing (CategoryTheory.End X)
The degree-zero endomorphisms form a local ring if the ambient endomorphism ring is local.