Finite support of degrees extracted from orbit push-down maps #
A linear map from a finite-dimensional space into a direct sum has only finitely many nonzero component maps. Applied objectwise to a transformation between Gabriel push-downs, and then combined with finite object support, this packages all extracted degree components as a genuine shift-orbit morphism.
theorem
MagnitudeConjecture.CoveringHom.finite_nonzero_components_of_finiteDimensional
{k : Type uK}
[Field k]
{V : Type uV}
[AddCommGroup V]
[Module k V]
{I : Type uI}
(W : I → Type uW)
[(i : I) → AddCommGroup (W i)]
[(i : I) → Module k (W i)]
[FiniteDimensional k V]
(f : V →ₗ[k] DirectSum I W)
:
{i : I | DirectSum.component k I W i ∘ₗ f ≠ 0}.Finite
A linear map from a finite-dimensional space into a direct sum has only finitely many nonzero component maps.
theorem
MagnitudeConjecture.CoveringHom.finite_orbitPushdownNatTransDegreeAppLinear_ne
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
{M N : CategoryTheory.Functor C (ModuleCat k)}
[M.Additive]
[CategoryTheory.Functor.Linear k M]
[N.Additive]
[CategoryTheory.Functor.Linear k N]
(X : C)
[FiniteDimensional k ↑(M.obj X)]
(α : orbitPushdown M ⟶ orbitPushdown N)
:
{a : A | orbitPushdownNatTransDegreeAppLinear D a X α ≠ 0}.Finite
At a finite-dimensional source value, only finitely many extracted degrees can be nonzero.
theorem
MagnitudeConjecture.CoveringHom.finite_orbitPushdownNatTransDegreeRaw_ne
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ : FiniteDimensionalModuleCategory k)
(N₀ : LinearModuleCategory k)
(α : orbitPushdown M₀.obj.obj ⟶ orbitPushdown N₀.obj)
:
{a : A | orbitPushdownNatTransDegreeRaw D a α ≠ 0}.Finite
For a finite-dimensional source module, only finitely many extracted raw module transformations can be nonzero.
theorem
MagnitudeConjecture.CoveringHom.finite_linearModuleOrbitPushdownDegree_ne
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ : FiniteDimensionalModuleCategory k)
(N₀ : LinearModuleCategory k)
(α : linearModuleOrbitPushdown.obj M₀.obj ⟶ linearModuleOrbitPushdown.obj N₀)
:
{a : A | linearModuleOrbitPushdownDegree D M₀.obj N₀ a α ≠ 0}.Finite
Only finitely many shifted module maps extracted from a push-down transformation can be nonzero.
noncomputable def
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegrees
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ : FiniteDimensionalModuleCategory k)
(N₀ : LinearModuleCategory k)
:
(linearModuleOrbitPushdown.obj M₀.obj ⟶ linearModuleOrbitPushdown.obj N₀) → ShiftOrbitHom A M₀.obj N₀
Package all degree components extracted from a push-down transformation as a finite-support shift-orbit morphism.
Instances For
@[simp]
theorem
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegrees_apply
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ : FiniteDimensionalModuleCategory k)
(N₀ : LinearModuleCategory k)
(α : linearModuleOrbitPushdown.obj M₀.obj ⟶ linearModuleOrbitPushdown.obj N₀)
(a : A)
:
(linearModuleOrbitPushdownDegrees D M₀ N₀ α) a = linearModuleOrbitPushdownDegree D M₀.obj N₀ a α
noncomputable def
MagnitudeConjecture.CoveringHom.linearModuleOrbitPushdownDegreesLinear
{k : Type uK}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{A : Type w}
[AddGroup A]
(D : CategoryTheory.ShiftMkCore C A)
[∀ (a : A), (D.F a).Additive]
[∀ (a : A), CategoryTheory.Functor.Linear k (D.F a)]
(M₀ : FiniteDimensionalModuleCategory k)
(N₀ : LinearModuleCategory k)
:
(linearModuleOrbitPushdown.obj M₀.obj ⟶ linearModuleOrbitPushdown.obj N₀) →ₗ[k] ShiftOrbitHom A M₀.obj N₀
All extracted degrees form a linear map into the finite-support direct sum.