Additivity of finite module surplus across orthogonal blocks #
def
MagnitudeConjecture.CoveringHom.blockComplement
{C : Type u}
{J : Type w}
(block : C → J)
(j : J)
:
Set C
Delete all objects outside a specified block.
Instances For
theorem
MagnitudeConjecture.CoveringHom.blockExtendedDensity_eq
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{J : Type w}
(block : C → J)
(hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0)
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
(j : J)
(M : FiniteDimensionalModuleCategory k)
(hM : CategoryTheory.Indecomposable M)
(hvan : ObjectDeletion.ModuleVanishesOnDeleted C (blockComplement block j) M.obj.obj)
:
ObjectDeletion.finiteDeletionExtendedLocalDensity C hrep (blockComplement block j) M hM = finiteModuleLocalDensity hrep M hM
Restriction to the unique support block preserves an indecomposable's local density.
theorem
MagnitudeConjecture.CoveringHom.sum_blockExtendedDensity
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{J : Type w}
(block : C → J)
(hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0)
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
[Fintype J]
(M : FiniteDimensionalModuleCategory k)
(hM : CategoryTheory.Indecomposable M)
:
∑ j : J, ObjectDeletion.finiteDeletionExtendedLocalDensity C hrep (blockComplement block j) M hM = finiteModuleLocalDensity hrep M hM
Summing the densities retained by all blocks counts an indecomposable exactly once.
theorem
MagnitudeConjecture.CoveringHom.finiteCategorySurplus_eq_sum_blockDeletionSurplus
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{J : Type w}
(block : C → J)
(hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0)
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
[Fintype C]
[Fintype J]
:
finiteCategorySurplus hP hrep = ∑ j : J, ObjectDeletion.finiteDeletionSurplus hP hrep (blockComplement block j)
The intrinsic surplus is the sum of the surpluses of the separate blocks.
theorem
MagnitudeConjecture.CoveringHom.blockComplement_noDeletedFactorization
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
{J : Type w}
(block : C → J)
(hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0)
(j : J)
:
ObjectDeletion.NoDeletedFactorization C (blockComplement block j)
No nonzero composite between objects of a block can pass through its complement.
theorem
MagnitudeConjecture.CoveringHom.finiteCategorySurplus_eq_card_mul_of_blockEquivalences
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{J : Type w}
(block : C → J)
(hcross : ∀ (X Y : C), block X ≠ block Y → ∀ (f : X ⟶ Y), f = 0)
(hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrep : IsLocallyRepresentationFinite)
[Fintype C]
[Fintype J]
{D : Type u}
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.Preadditive D]
[CategoryTheory.Linear k D]
[Fintype D]
(hQ : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X))
(hrepD : IsLocallyRepresentationFinite)
(E : (j : J) → ObjectDeletion.DeletionCategory C (blockComplement block j) ≌ D)
[∀ (j : J), (E j).functor.Additive]
[∀ (j : J), CategoryTheory.Functor.Linear k (E j).functor]
:
finiteCategorySurplus hP hrep = ↑(Fintype.card J) * finiteCategorySurplus hQ hrepD
When all blocks are equivalent to the same finite category, surplus is its surplus multiplied by the number of blocks.