Filtered arrow sums for a numbered family under an equivalence #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ofFGFamily_inverse_filtered_arrow_sum_eq
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{ι : Type}
[Fintype ι]
{C : Type v}
[CategoryTheory.Category.{u, v} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
(E : FGModuleCat Aᵐᵒᵖ ≌ C)
[E.functor.Additive]
[CategoryTheory.Functor.Linear k E.functor]
(H : ι → C)
(hi : ∀ (i : ι), CategoryTheory.Indecomposable (E.inverse.obj (H i)))
(hc :
∀ (X : FinitelyGeneratedCategory A), CategoryTheory.Indecomposable X → ∃ (i : ι), Nonempty (X ≅ E.inverse.obj (H i)))
(hs : ∀ (i j : ι), Nonempty (E.inverse.obj (H i) ≅ E.inverse.obj (H j)) → i = j)
(P : ι → Prop)
[DecidablePred P]
:
∑ j : { j : Fin (Fintype.card ι) // P ((Fintype.equivFin ι).symm j) },
∑ i : Fin (Fintype.card ι),
FiniteTauMatrix.arrowMultiplicity
(ofFGFamily (fun (a : ι) => E.inverse.obj (H a)) hi hc hs).finiteTauCategoryData.toFiniteRightTauCategoryData i
↑j = ∑ b : { b : ι // P b }, ∑ a : ι, Module.finrank k (CategoricalIrreducible.Space k (H a) (H ↑b))
Filtering targets commutes with transferring the numbered arrow sum.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.ofFGFamily_inverse_filtered_arrow_sum_eq_of_sum
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{ι : Type}
[Fintype ι]
{C : Type v}
[CategoryTheory.Category.{u, v} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
(E : FGModuleCat Aᵐᵒᵖ ≌ C)
[E.functor.Additive]
[CategoryTheory.Functor.Linear k E.functor]
(H : ι → C)
(hi : ∀ (i : ι), CategoryTheory.Indecomposable (E.inverse.obj (H i)))
(hc :
∀ (X : FinitelyGeneratedCategory A), CategoryTheory.Indecomposable X → ∃ (i : ι), Nonempty (X ≅ E.inverse.obj (H i)))
(hs : ∀ (i j : ι), Nonempty (E.inverse.obj (H i) ≅ E.inverse.obj (H j)) → i = j)
(P : ι → Prop)
[DecidablePred P]
(N : ℕ)
(hN : ∑ b : { b : ι // P b }, ∑ a : ι, Module.finrank k (CategoricalIrreducible.Space k (H a) (H ↑b)) = N)
:
∑ j : { j : Fin (Fintype.card ι) // P ((Fintype.equivFin ι).symm j) },
∑ i : Fin (Fintype.card ι),
FiniteTauMatrix.arrowMultiplicity
(ofFGFamily (fun (a : ι) => E.inverse.obj (H a)) hi hc hs).finiteTauCategoryData.toFiniteRightTauCategoryData i
↑j = N
A known filtered quotient sum supplies the numbered arrow sum directly.