Primitive category-algebra deletion

For the canonical projector at an object of a finite linear category, the primitive ideal annihilates a represented module exactly when the original category module vanishes at that object. This is the objectwise bridge between algebraic primitive deletion and the literal object-deletion quotient.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.primitiveDeletionAlgebraFiniteDimensional {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : FiniteDimensional k (algebra hP)

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.primitiveDeletionAlgebraOppositeIsNoetherian {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : IsNoetherianRing (algebra hP)ᵐᵒᵖ

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.represented_isAnnihilatedBy_primitiveIdeal_iff_obj_isZero {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (X : C) (M : FiniteDimensionalModuleCategory k) : RightModule.IsAnnihilatedBy (RightModule.primitiveIdeal (canonicalProjector hP X)) ((representedFGFunctor hP).obj M) ↔ CategoryTheory.Limits.IsZero (M.obj.obj.obj X)

Under the projective-generator equivalence, annihilation by the primitive ideal of the projector at X is exactly vanishing at X.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.primitiveQuotientProperty_inverseImage_eq_singletonVanishes {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (X : C) : (RightModule.PrimitiveQuotientProperty (canonicalProjector hP X)).inverseImage (moduleEquivalence hP).functor = ObjectDeletion.finiteModuleVanishesOnDeleted C {X}

For a singleton deletion, the primitive-ideal annihilation property is the literal vanishing-on-deleted-objects property.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.deletionPrimitiveSubcategoryEquivalence {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (X : C) : FiniteDimensionalModuleCategory k ≌ RightModule.PrimitiveQuotientSubcategory (canonicalProjector hP X)

The finite modules over the literal object-deletion category are equivalent to the ambient algebra modules annihilated by the corresponding canonical primitive ideal.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.deletionPrimitiveQuotientEquivalence {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (X : C) : FiniteDimensionalModuleCategory k ≌ RightModule.FinitelyGeneratedCategory (RightModule.primitiveQuotientAlgebra (canonicalProjector hP X))

The finite-dimensional module category of literal object deletion is equivalent to finitely generated modules over the algebraic primitive quotient by the matching canonical projector.