Documentation

TauCeti.Algebra.Category.ModuleCat.Biproducts

The carrier of a finite biproduct in ModuleCat #

Mathlib's ModuleCat.biproductIsoPi identifies a finite biproduct in ModuleCat A with the dependent function type ∀ i, P i. Over a finite index type the external direct sum ⨁ i, P i is the same module (DirectSum.linearEquivFunOnFintype), so a finite biproduct is also the external direct sum of the carriers of its summands. This file records that identification, together with the two lemmas that characterise it: its components are the biproduct projections, and it sends a biproduct inclusion to the corresponding direct-sum inclusion.

This is the transport along which results about DirectSum decompositions of a module — the Krull-Schmidt theorem among them — can be read as results about biproducts in ModuleCat A.

Main definitions #

Main results #

source
noncomputable def TauCeti.biproductDirectSumEquiv {A : Type u} [Ring A] {ι : Type} [Fintype ι] (P : ι → ModuleCat A) :
↑(⨁ P) ≃ₗ[A] DirectSum ι fun (i : ι) => ↑(P i)

The carrier of a finite biproduct in ModuleCat A is the external direct sum of the carriers of the summands.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.component_biproductDirectSumEquiv {A : Type u} [Ring A] {ι : Type} [Fintype ι] (P : ι → ModuleCat A) (x : ↑(⨁ P)) (i : ι) :
    (DirectSum.component A ι (fun (i : ι) => ↑(P i)) i) ((biproductDirectSumEquiv P) x) = (ModuleCat.Hom.hom (CategoryTheory.Limits.biproduct.π P i)) x

    The i-th component of TauCeti.biproductDirectSumEquiv is the i-th biproduct projection.

    source
    @[simp]
    theorem TauCeti.biproductDirectSumEquiv_ι {A : Type u} [Ring A] {ι : Type} [Fintype ι] (P : ι → ModuleCat A) [DecidableEq ι] (i : ι) (y : ↑(P i)) :
    (biproductDirectSumEquiv P) ((ModuleCat.Hom.hom (CategoryTheory.Limits.biproduct.ι P i)) y) = (DirectSum.lof A ι (fun (i : ι) => ↑(P i)) i) y

    TauCeti.biproductDirectSumEquiv carries the i-th biproduct inclusion to the i-th direct-sum inclusion.