Canonical primitive projectors of a finite linear category #
The endomorphism algebra of the biproduct of all covariant representables has the evident complete orthogonal idempotents given by its summand projectors. This file matches those projectors with the indecomposable projective labels of an arbitrary finite algebra-module skeleton.
theorem
MagnitudeConjecture.CoveringHom.biproductProjector_primitive
{ι : Type z}
[Fintype ι]
{D : Type w}
[CategoryTheory.Category.{u, w} D]
[CategoryTheory.Preadditive D]
(F : ι → D)
[CategoryTheory.Limits.HasBiproduct F]
(x : ι)
[IsLocalRing (CategoryTheory.End (F x))]
(hF : ¬CategoryTheory.Limits.IsZero (F x))
:
RightModule.PrimitiveIdempotentData
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π F x) (CategoryTheory.Limits.biproduct.ι F x))
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebraFiniteDimensional
{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.algebraOppositeIsNoetherian
{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)ᵐᵒᵖ
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalProjector
{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)
:
algebra hP
The projector onto one representable summand of the finite projective generator.
Instances For
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalProjector_complete
{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))
:
CompleteOrthogonalIdempotents (canonicalProjector hP)
The representable summand projectors are a complete orthogonal family.
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalProjector_primitive
{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))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(X : C)
:
A summand projector is primitive when the corresponding representable has local endomorphism ring.
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalRightIdealLinearEquiv
{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.rightIdealFGObj (canonicalProjector hP X)) ≃ₗ[(algebra hP)ᵐᵒᵖ] ↑((representedFGFunctor hP).obj
(MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representable✝ hP X))
The principal right ideal of a summand projector is the module represented by that summand.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalRightIdealIso
{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)
:
Categorical form of the identification between a canonical principal right ideal and its represented covariant representable.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalProjectorCoordinateLinearEquiv
{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.idempotentCoordinate (canonicalProjector hP X) ((representedFGFunctor hP).obj M)) ≃ₗ[k] ↑(M.obj.obj.obj X)
The canonical projector coordinate of a represented category module is its value at the matching category object.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalSkeletonCoordinateLinearEquiv
{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))
(S : RightModule.FiniteIndecomposableSkeleton k (algebra hP))
(X : C)
(M : FiniteDimensionalModuleCategory k)
(i : Fin S.n)
(eM : (representedFGFunctor hP).obj M ≅ S.fgObj i)
:
↥(RightModule.idempotentCoordinate (canonicalProjector hP X) (S.fgObj i)) ≃ₗ[k] ↑(M.obj.obj.obj X)
Transporting a represented module to the chosen algebra skeleton does not change its canonical primitive coordinate.
Instances For
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.primitiveMultiplicity_eq_finrank_obj
{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))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(S : RightModule.FiniteIndecomposableSkeleton k (algebra hP))
(X : C)
(M : FiniteDimensionalModuleCategory k)
(i : Fin S.n)
(eM : (representedFGFunctor hP).obj M ≅ S.fgObj i)
:
S.primitiveMultiplicity ⋯ i = Module.finrank k ↑(M.obj.obj.obj X)
The primitive multiplicity attached to a deleted category object is the dimension of the corresponding category-module fiber.
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalSourceLabel
{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))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(S : RightModule.FiniteIndecomposableSkeleton k (algebra hP))
(X : C)
:
The projective-skeleton label represented by one canonical summand projector.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalRepresentableSourceIso
{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))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(S : RightModule.FiniteIndecomposableSkeleton k (algebra hP))
(X : C)
:
(representedFGFunctor hP).obj (MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representable✝ hP X) ≅ S.fgObj (canonicalSourceLabel hP hlocal S X).label
The represented covariant representable is the chosen skeleton object at the source label of its canonical projector.
Instances For
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalSourceLabel_injective
{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))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(S : RightModule.FiniteIndecomposableSkeleton k (algebra hP))
(hskel : CategoryTheory.Skeletal C)
:
Function.Injective (canonicalSourceLabel hP hlocal S)
Distinct objects have distinct canonical projective-source labels in a skeletal finite category.
theorem
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalSourceLabel_surjective
{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))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(S : RightModule.FiniteIndecomposableSkeleton k (algebra hP))
:
Function.Surjective (canonicalSourceLabel hP hlocal S)
Every indecomposable projective in the algebra-module skeleton is the source of one canonical summand projector.
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalSourceEquiv
{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))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(S : RightModule.FiniteIndecomposableSkeleton k (algebra hP))
(hskel : CategoryTheory.Skeletal C)
:
C ≃ S.ProjectiveLabel
The canonical summands and the projective labels of any duplicate-free algebra-module skeleton have the same indexing set.
Instances For
noncomputable def
MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.primitiveProjectivePresentation
{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))
(hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X))
(S : RightModule.FiniteIndecomposableSkeleton k (algebra hP))
(hskel : CategoryTheory.Skeletal C)
:
The canonical primitive projectors, reindexed by the chosen projective skeleton, form the primitive-projective presentation required by the algebraic deletion theorem.