Homogeneous Hom equivalences under fully faithful graded realization

theorem MagnitudeConjecture.GradedCategory.HomGrading.map_part {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type v'} [CategoryTheory.Category.{u', v'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (G : HomGrading k C) (H : HomGrading k D) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : ∀ {X Y : C} {d : ℤ} {f : X ⟶ Y}, f ∈ G.component X Y d → F.map f ∈ H.component (F.obj X) (F.obj Y) d) {X Y : C} (d : ℤ) (f : X ⟶ Y) : F.map ((G.part X Y d) f) = (H.part (F.obj X) (F.obj Y) d) (F.map f)

A degree-preserving linear functor commutes with homogeneous projection.

theorem MagnitudeConjecture.GradedCategory.HomGrading.map_mem_iff {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type v'} [CategoryTheory.Category.{u', v'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (G : HomGrading k C) (H : HomGrading k D) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : ∀ {X Y : C} {d : ℤ} {f : X ⟶ Y}, f ∈ G.component X Y d → F.map f ∈ H.component (F.obj X) (F.obj Y) d) [F.Faithful] {X Y : C} {d : ℤ} {f : X ⟶ Y} : F.map f ∈ H.component (F.obj X) (F.obj Y) d ↔ f ∈ G.component X Y d

Faithfulness makes degree preservation an equivalence.

noncomputable def MagnitudeConjecture.GradedCategory.HomGrading.componentEquiv {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type v'} [CategoryTheory.Category.{u', v'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (G : HomGrading k C) (H : HomGrading k D) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : ∀ {X Y : C} {d : ℤ} {f : X ⟶ Y}, f ∈ G.component X Y d → F.map f ∈ H.component (F.obj X) (F.obj Y) d) [F.Full] [F.Faithful] (X Y : C) (d : ℤ) : ↥(G.component X Y d) ≃ₗ[k] ↥(H.component (F.obj X) (F.obj Y) d)

Full faithful degree-preserving realization identifies every homogeneous Hom space.

def MagnitudeConjecture.GradedCategory.HomGrading.degreeFunctor {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type v'} [CategoryTheory.Category.{u', v'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (G : HomGrading k C) (H : HomGrading k D) (F : CategoryTheory.Functor C D) (hF : ∀ {X Y : C} {d : ℤ} {f : X ⟶ Y}, f ∈ G.component X Y d → F.map f ∈ H.component (F.obj X) (F.obj Y) d) : CategoryTheory.Functor (DegreeObject G) (DegreeObject H)

A degree-preserving realization acts on the categories of shifted objects.

instance MagnitudeConjecture.GradedCategory.HomGrading.degreeFunctorFull {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type v'} [CategoryTheory.Category.{u', v'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (G : HomGrading k C) (H : HomGrading k D) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : ∀ {X Y : C} {d : ℤ} {f : X ⟶ Y}, f ∈ G.component X Y d → F.map f ∈ H.component (F.obj X) (F.obj Y) d) [F.Full] [F.Faithful] : (G.degreeFunctor H F ⋯).Full

instance MagnitudeConjecture.GradedCategory.HomGrading.degreeFunctorFaithful {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type v'} [CategoryTheory.Category.{u', v'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (G : HomGrading k C) (H : HomGrading k D) (F : CategoryTheory.Functor C D) (hF : ∀ {X Y : C} {d : ℤ} {f : X ⟶ Y}, f ∈ G.component X Y d → F.map f ∈ H.component (F.obj X) (F.obj Y) d) [F.Faithful] : (G.degreeFunctor H F ⋯).Faithful

instance MagnitudeConjecture.GradedCategory.HomGrading.degreeFunctorAdditive {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type v'} [CategoryTheory.Category.{u', v'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (G : HomGrading k C) (H : HomGrading k D) (F : CategoryTheory.Functor C D) [F.Additive] (hF : ∀ {X Y : C} {d : ℤ} {f : X ⟶ Y}, f ∈ G.component X Y d → F.map f ∈ H.component (F.obj X) (F.obj Y) d) : (G.degreeFunctor H F ⋯).Additive

instance MagnitudeConjecture.GradedCategory.HomGrading.degreeFunctorLinear {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type v'} [CategoryTheory.Category.{u', v'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (G : HomGrading k C) (H : HomGrading k D) (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Linear k F] (hF : ∀ {X Y : C} {d : ℤ} {f : X ⟶ Y}, f ∈ G.component X Y d → F.map f ∈ H.component (F.obj X) (F.obj Y) d) : CategoryTheory.Functor.Linear k (G.degreeFunctor H F ⋯)

theorem MagnitudeConjecture.GradedCategory.HomGrading.degreeFunctor_end_scalar {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {D : Type v'} [CategoryTheory.Category.{u', v'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] (G : HomGrading k C) (H : HomGrading k D) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (hF : ∀ {X Y : C} {d : ℤ} {f : X ⟶ Y}, f ∈ G.component X Y d → F.map f ∈ H.component (F.obj X) (F.obj Y) d) [F.Full] [F.Faithful] (hzero : ∀ (X : C), G.component X X 0 = k ∙ CategoryTheory.CategoryStruct.id X) (X : DegreeObject G) (f : (G.degreeFunctor H F ⋯).obj X ⟶ (G.degreeFunctor H F ⋯).obj X) : ∃ (c : k), f = c • CategoryTheory.CategoryStruct.id ((G.degreeFunctor H F ⋯).obj X)

Scalar degree-zero endomorphisms remain scalar in a fully faithful graded realization.