Documentation

TauCeti.CategoryTheory.Linear.Biproduct

Hom from a finite biproduct in a linear category #

The universal property of a biproduct identifies morphisms out of it with families of morphisms out of its summands. In a linear category this is a linear equivalence, so finiteness and rank of the Hom module can be read summand by summand.

source
noncomputable def TauCeti.homBiproductLinearEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type t) [Semiring k] [CategoryTheory.Linear k C] {J : Type w} (X : J → C) [CategoryTheory.Limits.HasBiproduct X] (Y : C) :
(⨁ X ⟶ Y) ≃ₗ[k] (j : J) → X j ⟶ Y

Morphisms from a biproduct form the product of the Hom spaces from its summands.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.homBiproductLinearEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type t) [Semiring k] [CategoryTheory.Linear k C] {J : Type w} (X : J → C) [CategoryTheory.Limits.HasBiproduct X] (Y : C) (f : ⨁ X ⟶ Y) (j : J) :
    (homBiproductLinearEquiv k X Y) f j = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X j) f

    The equivalence reads off a morphism's component at a summand.

    source
    @[simp]
    theorem TauCeti.homBiproductLinearEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type t) [Semiring k] [CategoryTheory.Linear k C] {J : Type w} (X : J → C) [CategoryTheory.Limits.HasBiproduct X] (Y : C) (f : (j : J) → X j ⟶ Y) :
    (homBiproductLinearEquiv k X Y).symm f = CategoryTheory.Limits.biproduct.desc f

    The inverse assembles a family of morphisms by the biproduct desc map.

    source
    instance TauCeti.moduleFinite_hom_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type t) [Semiring k] [CategoryTheory.Linear k C] {J : Type w} (X : J → C) [CategoryTheory.Limits.HasBiproduct X] (Y : C) [Finite J] [∀ (j : J), Module.Finite k (X j ⟶ Y)] :
    Module.Finite k (⨁ X ⟶ Y)

    Finite Hom modules out of each summand give a finite Hom module out of a finite biproduct.

    source
    theorem TauCeti.finrank_hom_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (k : Type t) [Semiring k] [CategoryTheory.Linear k C] {J : Type w} (X : J → C) [CategoryTheory.Limits.HasBiproduct X] (Y : C) [Fintype J] [StrongRankCondition k] [∀ (j : J), Module.Free k (X j ⟶ Y)] [∀ (j : J), Module.Finite k (X j ⟶ Y)] :
    Module.finrank k (⨁ X ⟶ Y) = ∑ j : J, Module.finrank k (X j ⟶ Y)

    The rank of Hom out of a finite biproduct is the sum of the ranks from its summands, when these are finite free modules.