Biproducts and binary biproducts #
We introduce the notion of (finite) biproducts and binary biproducts.
These are slightly unusual relative to the other shapes in the library, as they are simultaneously limits and colimits. (Zero objects are similar; they are "biterminal".)
For results about biproducts in preadditive categories see
CategoryTheory.Preadditive.Biproducts
.
In a category with zero morphisms, we model the (binary) biproduct of P Q : C
using a BinaryBicone
, which has a cone point X
,
and morphisms fst : X ⟶ P
, snd : X ⟶ Q
, inl : P ⟶ X
and inr : X ⟶ Q
,
such that inl ≫ fst = 𝟙 P
, inl ≫ snd = 0
, inr ≫ fst = 0
, and inr ≫ snd = 𝟙 Q
.
Such a BinaryBicone
is a biproduct if the cone is a limit cone, and the cocone is a colimit
cocone.
For biproducts indexed by a Fintype J
, a bicone
again consists of a cone point X
and morphisms π j : X ⟶ F j
and ι j : F j ⟶ X
for each j
,
such that ι j ≫ π j'
is the identity when j = j'
and zero otherwise.
Notation #
As ⊕
is already taken for the sum of types, we introduce the notation X ⊞ Y
for
a binary biproduct. We introduce ⨁ f
for the indexed biproduct.
Implementation notes #
Prior to https://github.com/leanprover-community/mathlib3/pull/14046,
HasFiniteBiproducts
required a DecidableEq
instance on the indexing type.
As this had no pay-off (everything about limits is non-constructive in mathlib),
and occasional cost
(constructing decidability instances appropriate for constructions involving the indexing type),
we made everything classical.
A c : Bicone F
is:
- an object
c.pt
and - morphisms
π j : pt ⟶ F j
andι j : F j ⟶ pt
for eachj
, - such that
ι j ≫ π j'
is the identity whenj = j'
and zero otherwise.
- pt : C
Instances For
A bicone morphism between two bicones for the same diagram is a morphism of the bicone points which commutes with the cone and cocone legs.
A morphism between the two vertex objects of the bicones
The triangle consisting of the two natural transformations and
hom
commutesThe triangle consisting of the two natural transformations and
hom
commutes
Instances For
The category of bicones on a given diagram.
Equations
To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.
Equations
- CategoryTheory.Limits.Bicones.ext φ wι wπ = { hom := { hom := φ.hom, wπ := ⋯, wι := ⋯ }, inv := { hom := φ.inv, wπ := ⋯, wι := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
A functor G : C ⥤ D
sends bicones over F
to bicones over G.obj ∘ F
functorially.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extract the cone from a bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A shorthand for toConeFunctor.obj
Equations
Instances For
Extract the cocone from a bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A shorthand for toCoconeFunctor.obj
Equations
Instances For
We can turn any limit cone over a discrete collection of objects into a bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
We can turn any colimit cocone over a discrete collection of objects into a bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Structure witnessing that a bicone is both a limit cone and a colimit cocone.
Structure witnessing that a bicone is both a limit cone and a colimit cocone.
Structure witnessing that a bicone is both a limit cone and a colimit cocone.
Instances For
Whisker a bicone with an equivalence between the indexing types.
Equations
Instances For
Taking the cone of a whiskered bicone results in a cone isomorphic to one gained by whiskering the cone and postcomposing with a suitable isomorphism.
Equations
Instances For
Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained by whiskering the cocone and precomposing with a suitable isomorphism.
Equations
Instances For
Whiskering a bicone with an equivalence between types preserves being a bilimit bicone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A bicone over F : J → C
, which is both a limit cone and a colimit cocone.
- bicone : Bicone F
A bicone over
F : J → C
, which is both a limit cone and a colimit cocone. A bicone over
F : J → C
, which is both a limit cone and a colimit cocone.
Instances For
HasBiproduct F
expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram F
.
- mk' :: (
- exists_biproduct : Nonempty (LimitBicone F)
HasBiproduct F
expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagramF
. - )
Instances
Use the axiom of choice to extract explicit BiproductData F
from HasBiproduct F
.
Equations
Instances For
A bicone for F
which is both a limit cone and a colimit cocone.
Equations
Instances For
biproduct.bicone F
is a bilimit bicone.
Equations
Instances For
biproduct.bicone F
is a limit cone.
Equations
Instances For
biproduct.bicone F
is a colimit cocone.
Equations
Instances For
C
has biproducts of shape J
if we have
a limit and a colimit, with the same cone points,
of every function F : J → C
.
- has_biproduct (F : J → C) : HasBiproduct F
Instances
HasFiniteBiproducts C
represents a choice of biproduct for every family of objects in C
indexed by a finite type.
- out (n : ℕ) : HasBiproductsOfShape (Fin n) C
HasFiniteBiproducts C
represents a choice of biproduct for every family of objects inC
indexed by a finite type.
Instances
The isomorphism between the specified limit and the specified colimit for a functor with a bilimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
biproduct f
computes the biproduct of a family of elements f
. (It is defined as an
abbreviation for limit (Discrete.functor f)
, so for most facts about biproduct f
, you will
just use general facts about limits and colimits.)
Equations
- (⨁ f) = (CategoryTheory.Limits.biproduct.bicone f).pt
Instances For
biproduct f
computes the biproduct of a family of elements f
. (It is defined as an
abbreviation for limit (Discrete.functor f)
, so for most facts about biproduct f
, you will
just use general facts about limits and colimits.)
Equations
- CategoryTheory.Limits.«term⨁_» = Lean.ParserDescr.node `CategoryTheory.Limits.«term⨁_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨁ ") (Lean.ParserDescr.cat `term 20))
Instances For
The projection onto a summand of a biproduct.
Equations
Instances For
The inclusion into a summand of a biproduct.
Equations
Instances For
Note that as this lemma has an if
in the statement, we include a DecidableEq
argument.
This means you may not be able to simp
using this lemma unless you open scoped Classical
.
Given a collection of maps into the summands, we obtain a map into the biproduct.
Equations
Instances For
Given a collection of maps out of the summands, we obtain a map out of the biproduct.
Equations
Instances For
Given a collection of maps between corresponding summands of a pair of biproducts indexed by the same type, we obtain a map between the biproducts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An alternative to biproduct.map
constructed via colimits.
This construction only exists in order to show it is equal to biproduct.map
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical isomorphism between the chosen biproduct and the chosen product.
Equations
Instances For
The canonical isomorphism between the chosen biproduct and the chosen coproduct.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If a category has biproducts of a shape J
, its colim
and lim
functor on diagrams over J
are isomorphic.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a collection of isomorphisms between corresponding summands of a pair of biproducts indexed by the same type, we obtain an isomorphism between the biproducts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two biproducts which differ by an equivalence in the indexing type, and up to isomorphism in the factors, are isomorphic.
Unfortunately there are two natural ways to define each direction of this isomorphism (because it is true for both products and coproducts separately). We give the alternative definitions as lemmas below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An iterated biproduct is a biproduct over a sigma type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical morphism from the biproduct over a restricted index type to the biproduct of the full index type.
Equations
Instances For
The canonical morphism from a biproduct to the biproduct over a restriction of its index type.
Equations
Instances For
The kernel of biproduct.π f i
is the inclusion from the biproduct which omits i
from the index set J
into the biproduct over J
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The kernel of biproduct.π f i
is ⨁ Subtype.restrict {i}ᶜ f
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cokernel of biproduct.ι f i
is the projection from the biproduct over the index set J
onto the biproduct omitting i
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cokernel of biproduct.ι f i
is ⨁ Subtype.restrict {i}ᶜ f
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The limit cone exhibiting ⨁ Subtype.restrict pᶜ f
as the kernel of
biproduct.toSubtype f p
Equations
- One or more equations did not get rendered due to their size.
Instances For
The kernel of biproduct.toSubtype f p
is ⨁ Subtype.restrict pᶜ f
.
Equations
Instances For
The colimit cocone exhibiting ⨁ Subtype.restrict pᶜ f
as the cokernel of
biproduct.fromSubtype f p
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cokernel of biproduct.fromSubtype f p
is ⨁ Subtype.restrict pᶜ f
.
Equations
Instances For
Convert a (dependently typed) matrix to a morphism of biproducts.
Equations
- CategoryTheory.Limits.biproduct.matrix m = CategoryTheory.Limits.biproduct.desc fun (j : J) => CategoryTheory.Limits.biproduct.lift fun (k : K) => m j k
Instances For
Extract the matrix components from a morphism of biproducts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Morphisms between direct sums are matrices.
Equations
- CategoryTheory.Limits.biproduct.matrixEquiv = { toFun := CategoryTheory.Limits.biproduct.components, invFun := CategoryTheory.Limits.biproduct.matrix, left_inv := ⋯, right_inv := ⋯ }
Instances For
Auxiliary lemma for biproduct.uniqueUpToIso
.
Auxiliary lemma for biproduct.uniqueUpToIso
.
Biproducts are unique up to isomorphism. This already follows because bilimits are limits,
but in the case of biproducts we can give an isomorphism with particularly nice definitional
properties, namely that biproduct.lift b.π
and biproduct.desc b.ι
are inverses of each
other.
Equations
- CategoryTheory.Limits.biproduct.uniqueUpToIso f hb = { hom := CategoryTheory.Limits.biproduct.lift b.π, inv := CategoryTheory.Limits.biproduct.desc b.ι, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
A category with finite biproducts has a zero object.
The limit bicone for the biproduct over an index type with exactly one term.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A biproduct over an index type with exactly one term is just the object over that term.
Equations
Instances For
A binary bicone for a pair of objects P Q : C
consists of the cone point X
,
maps from X
to both P
and Q
, and maps from both P
and Q
to X
,
so that inl ≫ fst = 𝟙 P
, inl ≫ snd = 0
, inr ≫ fst = 0
, and inr ≫ snd = 𝟙 Q
- pt : C
Instances For
A binary bicone morphism between two binary bicones for the same diagram is a morphism of the binary bicone points which commutes with the cone and cocone legs.
A morphism between the two vertex objects of the bicones
The triangle consisting of the two natural transformations and
hom
commutesThe triangle consisting of the two natural transformations and
hom
commutesThe triangle consisting of the two natural transformations and
hom
commutesThe triangle consisting of the two natural transformations and
hom
commutes
Instances For
The category of binary bicones on a given diagram.
To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A functor F : C ⥤ D
sends binary bicones for P
and Q
to binary bicones for G.obj P
and G.obj Q
functorially.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extract the cone from a binary bicone.
Equations
Instances For
Extract the cocone from a binary bicone.
Equations
Instances For
Convert a BinaryBicone
into a Bicone
over a pair.
Equations
- One or more equations did not get rendered due to their size.