Finite category algebras under full linear functors

A linear functor between finite linear categories acts entrywise on the Yoneda-coordinate matrices of their representable projective generators. This file packages that construction as an algebra homomorphism. Unlike the existing category-algebra equivalence, faithfulness is not required: quotient functors therefore give quotient maps of category algebras.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.SmallIndex {C : Type u} [Fintype C] : Type

A small finite index for the objects of the source category.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mappedGenerator {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) : FiniteDimensionalModuleCategory k

The sum of the target representables indexed through a small enumeration of the source objects.

@[reducible, inline]

abbrev MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mappedAlgebra {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) : Type u

The endomorphism algebra of the source-indexed sum of target representables.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.generatorSmallIso {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : finiteCategoryProjectiveGenerator hC ≅ MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.sourceSmallGenerator✝ hC

Reindex the possibly large finite object type by the small type Fin (card C).

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalProjector {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (i : SmallIndex) : algebra hC

The projector onto one representable summand, indexed by the small enumeration Fin (card C) of the possibly large finite object type.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.generatorSmallIso_hom_comp_π {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (i : SmallIndex) : CategoryTheory.CategoryStruct.comp (generatorSmallIso hC).hom (CategoryTheory.Limits.biproduct.π (fun (j : SmallIndex) => MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representable✝ hC ((Fintype.equivFin C).symm j)) i) = CategoryTheory.Limits.biproduct.π (fun (Y : C) => MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representable✝ hC Y) ((Fintype.equivFin C).symm i)

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallCanonicalProjector_eq_conjugate {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (i : SmallIndex) : smallCanonicalProjector hC i = CategoryTheory.CategoryStruct.comp (generatorSmallIso hC).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (j : SmallIndex) => MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representable✝ hC ((Fintype.equivFin C).symm j)) i) (CategoryTheory.Limits.biproduct.ι (fun (j : SmallIndex) => MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representable✝ hC ((Fintype.equivFin C).symm j)) i)) (generatorSmallIso hC).inv)

Under the reindexing isomorphism, a small canonical projector is the usual projector onto the corresponding summand.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mapAlgHom {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] : algebra hC →ₐ[k] mappedAlgebra hD F

The algebra homomorphism induced entrywise by a linear functor.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mapAlgHom_surjective {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] : Function.Surjective ⇑(mapAlgHom hC hD F)

A full linear functor induces a surjection onto the endomorphism algebra of the source-indexed target generator.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mappedGeneratorIsoOfBijective {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) [Fintype D] (hobj : Function.Bijective F.obj) : mappedGenerator hD F ≅ finiteCategoryProjectiveGenerator hD

If the functor is bijective on objects, its source-indexed sum of target representables is the usual target projective generator.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mappedAlgebraEquivOfBijective {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) [Fintype D] (hobj : Function.Bijective F.obj) : mappedAlgebra hD F ≃ₐ[k] algebra hD

The target-generator identification attached to an object-bijective functor.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mapAlgebraHomOfBijective {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [Fintype D] (hobj : Function.Bijective F.obj) : algebra hC →ₐ[k] algebra hD

The algebra homomorphism induced by a linear functor which is bijective on objects, now with the usual target category algebra as codomain.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mapAlgebraHomOfBijective_surjective {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [F.Full] [Fintype D] (hobj : Function.Bijective F.obj) : Function.Surjective ⇑(mapAlgebraHomOfBijective hC hD F hobj)

A full, object-bijective linear functor induces a surjection of finite category algebras.

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallAlgebraCategoryCoordinate {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (a : algebra hC) (i j : SmallIndex) : (Fintype.equivFin C).symm j ⟶ (Fintype.equivFin C).symm i

The category morphism in one reindexed matrix coordinate of a finite category algebra element. The orientation is reversed by covariant Yoneda: the (i,j) map between representables is represented by a morphism from the j-object to the i-object.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallAlgebraCategoryCoordinate_smul {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (c : k) (a : algebra hC) (i j : SmallIndex) : smallAlgebraCategoryCoordinate hC (c • a) i j = c • smallAlgebraCategoryCoordinate hC a i j

noncomputable def MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebraCategoryCoordinate {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (a : algebra hC) (X Y : C) : Y ⟶ X

The category morphism in an object-indexed matrix coordinate of a finite category algebra element. As for the small reindexing above, covariant Yoneda reverses the orientation of the displayed category morphism.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.algebraCategoryCoordinate_ext {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) {a b : algebra hC} (h : ∀ (X Y : C), algebraCategoryCoordinate hC a X Y = algebraCategoryCoordinate hC b X Y) : a = b

An element of a finite category algebra is determined by its object-indexed category-morphism coordinates.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.smallAlgebraCategoryCoordinate_eq_algebraCategoryCoordinate {k C : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (a : algebra hC) (i j : SmallIndex) : smallAlgebraCategoryCoordinate hC a i j = algebraCategoryCoordinate hC a ((Fintype.equivFin C).symm i) ((Fintype.equivFin C).symm j)

Reindexing the finite projective generator does not change its category morphism coordinates.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mapAlgHom_eq_zero_iff_smallAlgebraCategoryCoordinate {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] (a : algebra hC) : (mapAlgHom hC hD F) a = 0 ↔ ∀ (i j : SmallIndex), F.map (smallAlgebraCategoryCoordinate hC a i j) = 0

The functor-induced category-algebra map kills an element exactly when the functor kills every one of its category-morphism matrix coordinates.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mapAlgebraHomOfBijective_eq_zero_iff_smallAlgebraCategoryCoordinate {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [Fintype D] (hobj : Function.Bijective F.obj) (a : algebra hC) : (mapAlgebraHomOfBijective hC hD F hobj) a = 0 ↔ ∀ (i j : SmallIndex), F.map (smallAlgebraCategoryCoordinate hC a i j) = 0

The same coordinatewise kernel criterion after identifying the source-indexed target generator with the ordinary target generator.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.mapAlgebraHomOfBijective_eq_zero_iff_algebraCategoryCoordinate {k C D : Type u} [Field k] [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Category.{u, u} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k D] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hD : ∀ (X : D), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] [Fintype D] (hobj : Function.Bijective F.obj) (a : algebra hC) : (mapAlgebraHomOfBijective hC hD F hobj) a = 0 ↔ ∀ (X Y : C), F.map (algebraCategoryCoordinate hC a X Y) = 0

The object-indexed form of the coordinatewise kernel criterion.