Finite length bounds Hom-dimension from the unit

In the setting of Deligne's theorem — an abelian ℂ-linear rigid monoidal category whose unit endomorphisms are exactly the scalars — the Hom-space out of the tensor unit is finite dimensional whenever the target has bounded length, with dimension at most the length bound. This is the Hom-finiteness input of Deligne's Proposition 2.1.

The route: a nonzero map φ : 𝟙 ⟶ Z is a monomorphism because the unit is simple (simple_unit_of_hasScalarUnit), and pulling subobjects of cokernel φ back along the projection embeds its subobject chains strictly above the nonzero subobject φ, so the length bound drops by one on the cokernel. Left-exactness of Hom (𝟙, −), in the concrete form that a map annihilated by the projection factors through φ with a scalar coefficient, bounds the kernel of the induced linear map by one dimension, and induction along the length bound does the rest.

At the bottom of the induction sits the simple case, recorded separately: Hom (𝟙, S) vanishes for a simple S not isomorphic to the unit, and is the line End (𝟙_ A) = ℂ when it is — the scalar-unit hypothesis read as a ℂ-linear equivalence.

The unit endomorphisms are a line

The scalar-unit hypothesis says that scaling the identity of the tensor unit is a bijection ℂ → End (𝟙). Scaling is ℂ-linear, so the bijection is a ℂ-linear equivalence and End (𝟙) is a line. Transporting along an isomorphism 𝟙 ≅ S gives the same for 𝟙 ⟶ S.

def RS.unitScalarMap {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] : ℂ →ₗ[ℂ] CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit A

Scaling the identity of the tensor unit, as a ℂ-linear map.

Equations

• RS.unitScalarMap = { toFun := fun (c : ℂ) => c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def RS.unitEndEquiv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] (hu : HasScalarUnit A) : ℂ ≃ₗ[ℂ] CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit A

The scalars exhaust the unit endomorphisms, as a ℂ-linear equivalence ℂ ≃ₗ End (𝟙_ A): this is exactly the content of HasScalarUnit, packaged linearly.

Equations

• RS.unitEndEquiv hu = LinearEquiv.ofBijective RS.unitScalarMap hu

@[simp]

theorem RS.unitEndEquiv_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] (hu : HasScalarUnit A) (c : ℂ) : (unitEndEquiv hu) c = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)

theorem RS.finrank_end_unit {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] (hu : HasScalarUnit A) : Module.finrank ℂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit A) = 1

The unit endomorphisms are one dimensional.

noncomputable def RS.homUnitEquivOfIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] {S : A} (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ≅ S) : (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ S) ≃ₗ[ℂ] CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit A

An isomorphism 𝟙 ≅ S identifies 𝟙 ⟶ S with the unit endomorphisms, ℂ-linearly.

Equations

• RS.homUnitEquivOfIso e = CategoryTheory.Linear.homCongr ℂ (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit A)) e.symm

theorem RS.finrank_hom_unit_of_iso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] (hu : HasScalarUnit A) {S : A} (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ≅ S) : Module.finrank ℂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ S) = 1

Hom (𝟙, S) is a line when S is isomorphic to the unit: it is then End (𝟙_ A) = ℂ.

Maps from the unit to a simple object are proportional

Schur's lemma between the simple unit and a simple target: any nonzero φ : 𝟙 ⟶ S is an isomorphism, so every ψ : 𝟙 ⟶ S is a scalar multiple of it, the scalar produced by HasScalarUnit.

theorem RS.nonempty_unitIso_of_hom_ne_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {S : A} [CategoryTheory.Simple S] {φ : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ S} (hφ : φ ≠ 0) : Nonempty (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ≅ S)

A nonzero map from the unit to a simple object is an isomorphism, the unit being simple; so a simple object receiving a nonzero map from the unit is the unit up to isomorphism.

theorem RS.hom_unit_simple_eq_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {S : A} [CategoryTheory.Simple S] (h : IsEmpty (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ≅ S)) (φ : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ S) : φ = 0

Maps from the unit to a simple object not isomorphic to it vanish.

theorem RS.subsingleton_hom_unit_simple {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {S : A} [CategoryTheory.Simple S] (h : IsEmpty (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ≅ S)) : Subsingleton (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ S)

Hom (𝟙, S) is trivial for a simple S not isomorphic to the unit.

theorem RS.finrank_hom_unit_simple_eq_zero {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {S : A} [CategoryTheory.Simple S] (h : IsEmpty (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ≅ S)) : Module.finrank ℂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ S) = 0

Hom (𝟙, S) vanishes for a simple S not isomorphic to the unit.

Quotients drop the length bound

Pulling a subobject of a quotient back along the projection gives a subobject of the ambient object. The operation is monotone, and along an epimorphism it reflects inequalities, so it embeds strict chains; every pullback contains the kernel of the projection, so for the quotient by a nonzero subobject the embedded chain sits strictly above ⊥ and the length bound drops by one.

The induction along the length bound

Hom (𝟙, −) is left exact; concretely, a map 𝟙 ⟶ Z annihilated by the projection to cokernel φ factors through the kernel φ of that projection, with coefficient a unit endomorphism — a scalar. So the kernel of postcomposition by the projection is at most one dimensional, the quotient lemma above drops the length bound on the cokernel, and rank-nullity closes the induction.

The theorems

theorem RS.finrank_hom_unit_le {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {Z : A} {N : ℕ} (h : LengthLE Z N) : Module.Finite ℂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ Z) ∧ Module.finrank ℂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ Z) ≤ N

Finite length bounds Hom-dimension from the unit: in the setting of Deligne's theorem, a length bound of N on Z makes 𝟙 ⟶ Z a finite dimensional ℂ-module of dimension at most N.

noncomputable def RS.homUnitDualEquiv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (X Y : A) : (X ⟶ Y) ≃ₗ[ℂ] CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Xᘁ

The duality correspondence (X ⟶ Y) ≃ₗ (𝟙 ⟶ Y ⊗ Xᘁ) as a ℂ-linear equivalence: precomposition by the left unitor followed by the right-dual adjunction tensorRightHomEquiv. Linearity follows from bilinearity of composition and of the tensor product.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.finrank_hom_le {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.MonoidalLinear ℂ A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {X Y : A} {N : ℕ} (h : LengthLE (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Xᘁ) N) : Module.Finite ℂ (X ⟶ Y) ∧ Module.finrank ℂ (X ⟶ Y) ≤ N

Finite length bounds every Hom-dimension: in the setting of Deligne's theorem, a length bound of N on Y ⊗ Xᘁ makes X ⟶ Y a finite dimensional ℂ-module of dimension at most N, via the duality correspondence (X ⟶ Y) ≃ₗ (𝟙 ⟶ Y ⊗ Xᘁ).

Finite length, unquantified

LengthLE Z N is the bound-shaped finite-length predicate of this development; "Z has finite length" is ∃ N, LengthLE Z N, and "every object has finite length" is that statement quantified over all objects. There is no finite-length typeclass here, so the hypothesis is carried explicitly.

theorem RS.finiteDimensional_hom_unit {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.Linear ℂ A] [CategoryTheory.MonoidalCategory A] [CategoryTheory.MonoidalPreadditive A] [CategoryTheory.RigidCategory A] (hu : HasScalarUnit A) {Z : A} (h : ∃ (N : ℕ), LengthLE Z N) : FiniteDimensional ℂ (CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ Z)

Hom out of the unit is finite dimensional whenever the target has finite length.