Biproducts and binary biproducts #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
category_theory.preadditive.biproducts.
In a category with zero morphisms, we model the (binary) biproduct of P Q : C
using a binary_bicone, 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 binary_bicone 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 #
Prior to #14046, has_finite_biproducts required a decidable_eq 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.
@[nolint]
structure
category_theory.limits.bicone
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(F : J → C) :
Type (max u v w)
- X : C
- π : Π (j : J), self.X ⟶ F j
- ι : Π (j : J), F j ⟶ self.X
- ι_π : (∀ (j j' : J), self.ι j ≫ self.π j' = dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0)) . "obviously"
A c : bicone F is:
- an object
c.Xand - morphisms
π j : X ⟶ F jandι j : F j ⟶ Xfor eachj, - such that
ι j ≫ π j'is the identity whenj = j'and zero otherwise.
Instances for category_theory.limits.bicone
- category_theory.limits.bicone.has_sizeof_inst
@[simp]
theorem
category_theory.limits.bicone_ι_π_self
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F)
(j : J) :
@[simp]
theorem
category_theory.limits.bicone_ι_π_self_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F)
(j : J)
{X' : C}
(f' : F j ⟶ X') :
@[simp]
theorem
category_theory.limits.bicone_ι_π_ne
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F)
{j j' : J}
(h : j ≠ j') :
@[simp]
theorem
category_theory.limits.bicone_ι_π_ne_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F)
{j j' : J}
(h : j ≠ j')
{X' : C}
(f' : F j' ⟶ X') :
def
category_theory.limits.bicone.to_cone
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F) :
Extract the cone from a bicone.
@[simp]
theorem
category_theory.limits.bicone.to_cone_X
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F) :
@[simp]
theorem
category_theory.limits.bicone.to_cone_π_app
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F)
(j : category_theory.discrete J) :
theorem
category_theory.limits.bicone.to_cone_π_app_mk
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F)
(j : J) :
def
category_theory.limits.bicone.to_cocone
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F) :
Extract the cocone from a bicone.
@[simp]
theorem
category_theory.limits.bicone.to_cocone_X
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F) :
@[simp]
theorem
category_theory.limits.bicone.to_cocone_ι_app
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F)
(j : category_theory.discrete J) :
theorem
category_theory.limits.bicone.to_cocone_ι_app_mk
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F)
(j : J) :
@[simp]
theorem
category_theory.limits.bicone.of_limit_cone_ι
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.cone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_limit t)
(j : J) :
(category_theory.limits.bicone.of_limit_cone ht).ι j = ht.lift (category_theory.limits.fan.mk (f j) (λ (j' : J), dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0)))
noncomputable
def
category_theory.limits.bicone.of_limit_cone
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.cone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_limit t) :
We can turn any limit cone over a discrete collection of objects into a bicone.
@[simp]
theorem
category_theory.limits.bicone.of_limit_cone_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.cone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_limit t)
(j : J) :
@[simp]
theorem
category_theory.limits.bicone.of_limit_cone_X
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.cone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_limit t) :
theorem
category_theory.limits.bicone.ι_of_is_limit
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.bicone f}
(ht : category_theory.limits.is_limit t.to_cone)
(j : J) :
t.ι j = ht.lift (category_theory.limits.fan.mk (f j) (λ (j' : J), dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0)))
@[simp]
theorem
category_theory.limits.bicone.of_colimit_cocone_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.cocone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_colimit t)
(j : J) :
(category_theory.limits.bicone.of_colimit_cocone ht).π j = ht.desc (category_theory.limits.cofan.mk (f j) (λ (j' : J), dite (j' = j) (λ (h : j' = j), category_theory.eq_to_hom _) (λ (h : ¬j' = j), 0)))
@[simp]
theorem
category_theory.limits.bicone.of_colimit_cocone_X
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.cocone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_colimit t) :
@[simp]
theorem
category_theory.limits.bicone.of_colimit_cocone_ι
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.cocone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_colimit t)
(j : J) :
noncomputable
def
category_theory.limits.bicone.of_colimit_cocone
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.cocone (category_theory.discrete.functor f)}
(ht : category_theory.limits.is_colimit t) :
We can turn any colimit cocone over a discrete collection of objects into a bicone.
theorem
category_theory.limits.bicone.π_of_is_colimit
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{t : category_theory.limits.bicone f}
(ht : category_theory.limits.is_colimit t.to_cocone)
(j : J) :
t.π j = ht.desc (category_theory.limits.cofan.mk (f j) (λ (j' : J), dite (j' = j) (λ (h : j' = j), category_theory.eq_to_hom _) (λ (h : ¬j' = j), 0)))
@[nolint]
structure
category_theory.limits.bicone.is_bilimit
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(B : category_theory.limits.bicone F) :
Type (max u v w)
- is_limit : category_theory.limits.is_limit B.to_cone
- is_colimit : category_theory.limits.is_colimit B.to_cocone
Structure witnessing that a bicone is both a limit cone and a colimit cocone.
Instances for category_theory.limits.bicone.is_bilimit
- category_theory.limits.bicone.is_bilimit.has_sizeof_inst
- category_theory.limits.bicone.subsingleton_is_bilimit
theorem
category_theory.limits.bicone.is_bilimit.ext
{J : Type w}
{C : Type u}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.limits.has_zero_morphisms C}
{F : J → C}
{B : category_theory.limits.bicone F}
(x y : B.is_bilimit)
(h : x.is_limit = y.is_limit)
(h_1 : x.is_colimit = y.is_colimit) :
x = y
theorem
category_theory.limits.bicone.is_bilimit.ext_iff
{J : Type w}
{C : Type u}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.limits.has_zero_morphisms C}
{F : J → C}
{B : category_theory.limits.bicone F}
(x y : B.is_bilimit) :
x = y ↔ x.is_limit = y.is_limit ∧ x.is_colimit = y.is_colimit
@[protected, instance]
def
category_theory.limits.bicone.subsingleton_is_bilimit
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
{c : category_theory.limits.bicone f} :
@[simp]
theorem
category_theory.limits.bicone.whisker_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type w'}
{f : J → C}
(c : category_theory.limits.bicone f)
(g : K ≃ J)
(k : K) :
@[simp]
theorem
category_theory.limits.bicone.whisker_X
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type w'}
{f : J → C}
(c : category_theory.limits.bicone f)
(g : K ≃ J) :
def
category_theory.limits.bicone.whisker
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type w'}
{f : J → C}
(c : category_theory.limits.bicone f)
(g : K ≃ J) :
Whisker a bicone with an equivalence between the indexing types.
@[simp]
theorem
category_theory.limits.bicone.whisker_ι
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type w'}
{f : J → C}
(c : category_theory.limits.bicone f)
(g : K ≃ J)
(k : K) :
def
category_theory.limits.bicone.whisker_to_cone
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type w'}
{f : J → C}
(c : category_theory.limits.bicone f)
(g : K ≃ J) :
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
def
category_theory.limits.bicone.whisker_to_cocone
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type w'}
{f : J → C}
(c : category_theory.limits.bicone f)
(g : K ≃ J) :
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
def
category_theory.limits.bicone.whisker_is_bilimit_iff
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type w'}
{f : J → C}
(c : category_theory.limits.bicone f)
(g : K ≃ J) :
(c.whisker g).is_bilimit ≃ c.is_bilimit
Whiskering a bicone with an equivalence between types preserves being a bilimit bicone.
Equations
- c.whisker_is_bilimit_iff g = equiv_of_subsingleton_of_subsingleton (λ (hc : (c.whisker g).is_bilimit), {is_limit := let this : category_theory.limits.is_limit ((category_theory.limits.cones.postcompose (category_theory.discrete.functor_comp f ⇑g).inv).obj (category_theory.limits.cone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cone)) := hc.is_limit.of_iso_limit (c.whisker_to_cone g), this : category_theory.limits.is_limit (category_theory.limits.cone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cone) := ⇑(category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.discrete.functor_comp f ⇑g).symm (category_theory.limits.cone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cone)) this in category_theory.limits.is_limit.of_whisker_equivalence (category_theory.discrete.equivalence g) this, is_colimit := let this : category_theory.limits.is_colimit ((category_theory.limits.cocones.precompose (category_theory.discrete.functor_comp f ⇑g).hom).obj (category_theory.limits.cocone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cocone)) := hc.is_colimit.of_iso_colimit (c.whisker_to_cocone g), this : category_theory.limits.is_colimit (category_theory.limits.cocone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cocone) := ⇑(category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.discrete.functor_comp f ⇑g) (category_theory.limits.cocone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cocone)) this in category_theory.limits.is_colimit.of_whisker_equivalence (category_theory.discrete.equivalence g) this}) (λ (hc : c.is_bilimit), {is_limit := (⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.discrete.functor_comp f ⇑g).symm (category_theory.limits.cone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cone)).symm) (hc.is_limit.whisker_equivalence (category_theory.discrete.equivalence g))).of_iso_limit (c.whisker_to_cone g).symm, is_colimit := (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.discrete.functor_comp f ⇑g) (category_theory.limits.cocone.whisker (category_theory.discrete.functor (category_theory.discrete.mk ∘ ⇑g)) c.to_cocone)).symm) (hc.is_colimit.whisker_equivalence (category_theory.discrete.equivalence g))).of_iso_colimit (c.whisker_to_cocone g).symm})
@[nolint]
structure
category_theory.limits.limit_bicone
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(F : J → C) :
Type (max u v w)
- bicone : category_theory.limits.bicone F
- is_bilimit : self.bicone.is_bilimit
A bicone over F : J → C, which is both a limit cone and a colimit cocone.
Instances for category_theory.limits.limit_bicone
- category_theory.limits.limit_bicone.has_sizeof_inst
@[class]
structure
category_theory.limits.has_biproduct
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(F : J → C) :
Prop
- exists_biproduct : nonempty (category_theory.limits.limit_bicone F)
has_biproduct F expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram F.
theorem
category_theory.limits.has_biproduct.mk
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
(d : category_theory.limits.limit_bicone F) :
noncomputable
def
category_theory.limits.get_biproduct_data
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(F : J → C)
[category_theory.limits.has_biproduct F] :
Use the axiom of choice to extract explicit biproduct_data F from has_biproduct F.
noncomputable
def
category_theory.limits.biproduct.bicone
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(F : J → C)
[category_theory.limits.has_biproduct F] :
A bicone for F which is both a limit cone and a colimit cocone.
noncomputable
def
category_theory.limits.biproduct.is_bilimit
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(F : J → C)
[category_theory.limits.has_biproduct F] :
biproduct.bicone F is a bilimit bicone.
noncomputable
def
category_theory.limits.biproduct.is_limit
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(F : J → C)
[category_theory.limits.has_biproduct F] :
biproduct.bicone F is a limit cone.
noncomputable
def
category_theory.limits.biproduct.is_colimit
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(F : J → C)
[category_theory.limits.has_biproduct F] :
biproduct.bicone F is a colimit cocone.
@[protected, instance]
def
category_theory.limits.has_product_of_has_biproduct
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
[category_theory.limits.has_biproduct F] :
@[protected, instance]
def
category_theory.limits.has_coproduct_of_has_biproduct
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{F : J → C}
[category_theory.limits.has_biproduct F] :
@[class]
structure
category_theory.limits.has_biproducts_of_shape
(J : Type w)
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
Prop
- has_biproduct : ∀ (F : J → C), category_theory.limits.has_biproduct F
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.
Instances of this typeclass
@[class]
structure
category_theory.limits.has_finite_biproducts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
Prop
- out : ∀ (n : ℕ), category_theory.limits.has_biproducts_of_shape (fin n) C
has_finite_biproducts C represents a choice of biproduct for every family of objects in C
indexed by a finite type.
theorem
category_theory.limits.has_biproducts_of_shape_of_equiv
{J : Type w}
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type w'}
[category_theory.limits.has_biproducts_of_shape K C]
(e : J ≃ K) :
@[protected, instance]
@[protected, instance]
noncomputable
def
category_theory.limits.biproduct_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(F : J → C)
[category_theory.limits.has_biproduct F] :
The isomorphism between the specified limit and the specified colimit for a functor with a bilimit.
Equations
- category_theory.limits.biproduct_iso F = (category_theory.limits.limit.is_limit (category_theory.discrete.functor F)).cone_point_unique_up_to_iso (category_theory.limits.biproduct.is_limit F) ≪≫ (category_theory.limits.biproduct.is_colimit F).cocone_point_unique_up_to_iso (category_theory.limits.colimit.is_colimit (category_theory.discrete.functor F))
@[reducible]
noncomputable
def
category_theory.limits.biproduct
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f] :
C
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.)
@[reducible]
noncomputable
def
category_theory.limits.biproduct.π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(b : J) :
The projection onto a summand of a biproduct.
@[simp]
theorem
category_theory.limits.biproduct.bicone_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(b : J) :
@[reducible]
noncomputable
def
category_theory.limits.biproduct.ι
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(b : J) :
The inclusion into a summand of a biproduct.
@[simp]
theorem
category_theory.limits.biproduct.bicone_ι
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(b : J) :
theorem
category_theory.limits.biproduct.ι_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[decidable_eq J]
(f : J → C)
[category_theory.limits.has_biproduct f]
(j j' : J) :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j' = dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0)
Note that as this lemma has a if in the statement, we include a decidable_eq argument.
This means you may not be able to simp using this lemma unless you open_locale classical.
theorem
category_theory.limits.biproduct.ι_π_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[decidable_eq J]
(f : J → C)
[category_theory.limits.has_biproduct f]
(j j' : J)
{X' : C}
(f' : f j' ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j' ≫ f' = dite (j = j') (λ (h : j = j'), category_theory.eq_to_hom _) (λ (h : ¬j = j'), 0) ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.ι_π_self_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(j : J)
{X' : C}
(f' : f j ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j ≫ f' = f'
@[simp]
theorem
category_theory.limits.biproduct.ι_π_self
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(j : J) :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j = 𝟙 (f j)
@[simp]
theorem
category_theory.limits.biproduct.ι_π_ne
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
{j j' : J}
(h : j ≠ j') :
@[simp]
theorem
category_theory.limits.biproduct.ι_π_ne_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
{j j' : J}
(h : j ≠ j')
{X' : C}
(f' : f j' ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.π f j' ≫ f' = 0 ≫ f'
@[reducible]
noncomputable
def
category_theory.limits.biproduct.lift
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f]
{P : C}
(p : Π (b : J), P ⟶ f b) :
Given a collection of maps into the summands, we obtain a map into the biproduct.
@[reducible]
noncomputable
def
category_theory.limits.biproduct.desc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f]
{P : C}
(p : Π (b : J), f b ⟶ P) :
Given a collection of maps out of the summands, we obtain a map out of the biproduct.
@[simp]
theorem
category_theory.limits.biproduct.lift_π_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f]
{P : C}
(p : Π (b : J), P ⟶ f b)
(j : J)
{X' : C}
(f' : f j ⟶ X') :
category_theory.limits.biproduct.lift p ≫ category_theory.limits.biproduct.π f j ≫ f' = p j ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.lift_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f]
{P : C}
(p : Π (b : J), P ⟶ f b)
(j : J) :
@[simp]
theorem
category_theory.limits.biproduct.ι_desc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f]
{P : C}
(p : Π (b : J), f b ⟶ P)
(j : J) :
@[simp]
theorem
category_theory.limits.biproduct.ι_desc_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f]
{P : C}
(p : Π (b : J), f b ⟶ P)
(j : J)
{X' : C}
(f' : P ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.desc p ≫ f' = p j ≫ f'
@[reducible]
noncomputable
def
category_theory.limits.biproduct.map
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (b : J), f b ⟶ g b) :
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.
@[reducible]
noncomputable
def
category_theory.limits.biproduct.map'
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (b : J), f b ⟶ g b) :
An alternative to biproduct.map constructed via colimits.
This construction only exists in order to show it is equal to biproduct.map.
@[ext]
theorem
category_theory.limits.biproduct.hom_ext
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f]
{Z : C}
(g h : Z ⟶ ⨁ f)
(w : ∀ (j : J), g ≫ category_theory.limits.biproduct.π f j = h ≫ category_theory.limits.biproduct.π f j) :
g = h
@[ext]
theorem
category_theory.limits.biproduct.hom_ext'
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f]
{Z : C}
(g h : ⨁ f ⟶ Z)
(w : ∀ (j : J), category_theory.limits.biproduct.ι f j ≫ g = category_theory.limits.biproduct.ι f j ≫ h) :
g = h
noncomputable
def
category_theory.limits.biproduct.iso_product
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f] :
The canonical isomorphism between the chosen biproduct and the chosen product.
@[simp]
theorem
category_theory.limits.biproduct.iso_product_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f] :
@[simp]
theorem
category_theory.limits.biproduct.iso_product_inv
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f] :
noncomputable
def
category_theory.limits.biproduct.iso_coproduct
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f] :
The canonical isomorphism between the chosen biproduct and the chosen coproduct.
@[simp]
theorem
category_theory.limits.biproduct.iso_coproduct_inv
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f] :
@[simp]
theorem
category_theory.limits.biproduct.iso_coproduct_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f : J → C}
[category_theory.limits.has_biproduct f] :
theorem
category_theory.limits.biproduct.map_eq_map'
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (b : J), f b ⟶ g b) :
@[simp]
theorem
category_theory.limits.biproduct.map_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (j : J), f j ⟶ g j)
(j : J) :
@[simp]
theorem
category_theory.limits.biproduct.map_π_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (j : J), f j ⟶ g j)
(j : J)
{X' : C}
(f' : g j ⟶ X') :
@[simp]
theorem
category_theory.limits.biproduct.ι_map_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (j : J), f j ⟶ g j)
(j : J)
{X' : C}
(f' : (⨁ λ (j : J), g j) ⟶ X') :
@[simp]
theorem
category_theory.limits.biproduct.ι_map
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (j : J), f j ⟶ g j)
(j : J) :
@[simp]
theorem
category_theory.limits.biproduct.map_desc_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (j : J), f j ⟶ g j)
{P : C}
(k : Π (j : J), g j ⟶ P)
{X' : C}
(f' : P ⟶ X') :
category_theory.limits.biproduct.map p ≫ category_theory.limits.biproduct.desc k ≫ f' = category_theory.limits.biproduct.desc (λ (j : J), p j ≫ k j) ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.map_desc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (j : J), f j ⟶ g j)
{P : C}
(k : Π (j : J), g j ⟶ P) :
category_theory.limits.biproduct.map p ≫ category_theory.limits.biproduct.desc k = category_theory.limits.biproduct.desc (λ (j : J), p j ≫ k j)
@[simp]
theorem
category_theory.limits.biproduct.lift_map_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
{P : C}
(k : Π (j : J), P ⟶ f j)
(p : Π (j : J), f j ⟶ g j)
{X' : C}
(f' : (⨁ λ (j : J), g j) ⟶ X') :
category_theory.limits.biproduct.lift k ≫ category_theory.limits.biproduct.map p ≫ f' = category_theory.limits.biproduct.lift (λ (j : J), k j ≫ p j) ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.lift_map
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
{P : C}
(k : Π (j : J), P ⟶ f j)
(p : Π (j : J), f j ⟶ g j) :
category_theory.limits.biproduct.lift k ≫ category_theory.limits.biproduct.map p = category_theory.limits.biproduct.lift (λ (j : J), k j ≫ p j)
@[simp]
theorem
category_theory.limits.biproduct.map_iso_inv
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (b : J), f b ≅ g b) :
(category_theory.limits.biproduct.map_iso p).inv = category_theory.limits.biproduct.map (λ (b : J), (p b).inv)
@[simp]
theorem
category_theory.limits.biproduct.map_iso_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (b : J), f b ≅ g b) :
(category_theory.limits.biproduct.map_iso p).hom = category_theory.limits.biproduct.map (λ (b : J), (p b).hom)
noncomputable
def
category_theory.limits.biproduct.map_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{f g : J → C}
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct g]
(p : Π (b : J), f b ≅ g b) :
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
- category_theory.limits.biproduct.map_iso p = {hom := category_theory.limits.biproduct.map (λ (b : J), (p b).hom), inv := category_theory.limits.biproduct.map (λ (b : J), (p b).inv), hom_inv_id' := _, inv_hom_id' := _}
noncomputable
def
category_theory.limits.biproduct.from_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)] :
⨁ subtype.restrict p f ⟶ ⨁ f
The canonical morphism from the biproduct over a restricted index type to the biproduct of the full index type.
Equations
noncomputable
def
category_theory.limits.biproduct.to_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)] :
⨁ f ⟶ ⨁ subtype.restrict p f
The canonical morphism from a biproduct to the biproduct over a restriction of its index type.
Equations
@[simp]
theorem
category_theory.limits.biproduct.from_subtype_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
[decidable_pred p]
(j : J) :
category_theory.limits.biproduct.from_subtype f p ≫ category_theory.limits.biproduct.π f j = dite (p j) (λ (h : p j), category_theory.limits.biproduct.π (subtype.restrict p f) ⟨j, h⟩) (λ (h : ¬p j), 0)
@[simp]
theorem
category_theory.limits.biproduct.from_subtype_π_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
[decidable_pred p]
(j : J)
{X' : C}
(f' : f j ⟶ X') :
category_theory.limits.biproduct.from_subtype f p ≫ category_theory.limits.biproduct.π f j ≫ f' = dite (p j) (λ (h : p j), category_theory.limits.biproduct.π (subtype.restrict p f) ⟨j, h⟩) (λ (h : ¬p j), 0) ≫ f'
theorem
category_theory.limits.biproduct.from_subtype_eq_lift
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
[decidable_pred p] :
category_theory.limits.biproduct.from_subtype f p = category_theory.limits.biproduct.lift (λ (j : J), dite (p j) (λ (h : p j), category_theory.limits.biproduct.π (subtype.restrict p f) ⟨j, h⟩) (λ (h : ¬p j), 0))
@[simp]
theorem
category_theory.limits.biproduct.from_subtype_π_subtype_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
(j : subtype p)
{X' : C}
(f' : f ↑j ⟶ X') :
@[simp]
theorem
category_theory.limits.biproduct.from_subtype_π_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
(j : subtype p) :
@[simp]
theorem
category_theory.limits.biproduct.to_subtype_π_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
(j : subtype p)
{X' : C}
(f' : subtype.restrict p f j ⟶ X') :
@[simp]
theorem
category_theory.limits.biproduct.to_subtype_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
(j : subtype p) :
@[simp]
theorem
category_theory.limits.biproduct.ι_to_subtype_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
[decidable_pred p]
(j : J)
{X' : C}
(f' : ⨁ subtype.restrict p f ⟶ X') :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.to_subtype f p ≫ f' = dite (p j) (λ (h : p j), category_theory.limits.biproduct.ι (subtype.restrict p f) ⟨j, h⟩) (λ (h : ¬p j), 0) ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.ι_to_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
[decidable_pred p]
(j : J) :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.to_subtype f p = dite (p j) (λ (h : p j), category_theory.limits.biproduct.ι (subtype.restrict p f) ⟨j, h⟩) (λ (h : ¬p j), 0)
theorem
category_theory.limits.biproduct.to_subtype_eq_desc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
[decidable_pred p] :
category_theory.limits.biproduct.to_subtype f p = category_theory.limits.biproduct.desc (λ (j : J), dite (p j) (λ (h : p j), category_theory.limits.biproduct.ι (subtype.restrict p f) ⟨j, h⟩) (λ (h : ¬p j), 0))
@[simp]
theorem
category_theory.limits.biproduct.ι_to_subtype_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
(j : subtype p) :
@[simp]
theorem
category_theory.limits.biproduct.ι_to_subtype_subtype_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
(j : subtype p)
{X' : C}
(f' : ⨁ subtype.restrict p f ⟶ X') :
@[simp]
theorem
category_theory.limits.biproduct.ι_from_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
(j : subtype p) :
@[simp]
theorem
category_theory.limits.biproduct.ι_from_subtype_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
(j : subtype p)
{X' : C}
(f' : ⨁ f ⟶ X') :
@[simp]
theorem
category_theory.limits.biproduct.from_subtype_to_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)] :
@[simp]
theorem
category_theory.limits.biproduct.from_subtype_to_subtype_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
{X' : C}
(f' : ⨁ subtype.restrict p f ⟶ X') :
@[simp]
theorem
category_theory.limits.biproduct.to_subtype_from_subtype_assoc
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
[decidable_pred p]
{X' : C}
(f' : ⨁ f ⟶ X') :
category_theory.limits.biproduct.to_subtype f p ≫ category_theory.limits.biproduct.from_subtype f p ≫ f' = category_theory.limits.biproduct.map (λ (j : J), ite (p j) (𝟙 (f j)) 0) ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.to_subtype_from_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(p : J → Prop)
[category_theory.limits.has_biproduct (subtype.restrict p f)]
[decidable_pred p] :
category_theory.limits.biproduct.to_subtype f p ≫ category_theory.limits.biproduct.from_subtype f p = category_theory.limits.biproduct.map (λ (j : J), ite (p j) (𝟙 (f j)) 0)
noncomputable
def
category_theory.limits.biproduct.is_limit_from_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
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
- category_theory.limits.biproduct.is_limit_from_subtype f i = category_theory.limits.fork.is_limit.mk' (category_theory.limits.kernel_fork.of_ι (category_theory.limits.biproduct.from_subtype f (λ (j : J), j ≠ i)) _) (λ (s : category_theory.limits.fork (category_theory.limits.biproduct.π f i) 0), ⟨s.ι ≫ category_theory.limits.biproduct.to_subtype f (λ (j : J), j ≠ i), _⟩)
@[protected, instance]
def
category_theory.limits.biproduct.π.has_kernel
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
noncomputable
def
category_theory.limits.kernel_biproduct_π_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
category_theory.limits.kernel (category_theory.limits.biproduct.π f i) ≅ ⨁ subtype.restrict (λ (j : J), j ≠ i) f
The kernel of biproduct.π f i is ⨁ subtype.restrict {i}ᶜ f.
Equations
@[simp]
theorem
category_theory.limits.kernel_biproduct_π_iso_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
@[simp]
theorem
category_theory.limits.kernel_biproduct_π_iso_inv
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
noncomputable
def
category_theory.limits.biproduct.is_colimit_to_subtype
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
The cokernel of biproduct.ι f i is the projection from the biproduct over the index set J
onto the biproduct omitting i.
Equations
- category_theory.limits.biproduct.is_colimit_to_subtype f i = category_theory.limits.cofork.is_colimit.mk' (category_theory.limits.cokernel_cofork.of_π (category_theory.limits.biproduct.to_subtype f (λ (j : J), j ≠ i)) _) (λ (s : category_theory.limits.cofork (category_theory.limits.biproduct.ι f i) 0), ⟨category_theory.limits.biproduct.from_subtype f (λ (j : J), j ≠ i) ≫ s.π, _⟩)
@[protected, instance]
def
category_theory.limits.biproduct.ι.has_cokernel
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
@[simp]
theorem
category_theory.limits.cokernel_biproduct_ι_iso_inv
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
@[simp]
theorem
category_theory.limits.cokernel_biproduct_ι_iso_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
noncomputable
def
category_theory.limits.cokernel_biproduct_ι_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
(i : J)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (subtype.restrict (λ (j : J), j ≠ i) f)] :
category_theory.limits.cokernel (category_theory.limits.biproduct.ι f i) ≅ ⨁ subtype.restrict (λ (j : J), j ≠ i) f
The cokernel of biproduct.ι f i is ⨁ subtype.restrict {i}ᶜ f.
Equations
- category_theory.limits.cokernel_biproduct_ι_iso f i = category_theory.limits.colimit.iso_colimit_cocone {cocone := category_theory.limits.cokernel_cofork.of_π (category_theory.limits.biproduct.to_subtype f (λ (j : J), j ≠ i)) _, is_colimit := category_theory.limits.biproduct.is_colimit_to_subtype f i _inst_4}
@[simp]
theorem
category_theory.limits.kernel_fork_biproduct_to_subtype_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
(category_theory.limits.kernel_fork_biproduct_to_subtype f p).is_limit = category_theory.limits.kernel_fork.is_limit.of_ι (category_theory.limits.biproduct.from_subtype f pᶜ) _ (λ (W : C) (g : W ⟶ ⨁ f) (h : g ≫ category_theory.limits.biproduct.to_subtype f p = 0), g ≫ category_theory.limits.biproduct.to_subtype f pᶜ) _ _
@[simp]
theorem
category_theory.limits.kernel_fork_biproduct_to_subtype_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
noncomputable
def
category_theory.limits.kernel_fork_biproduct_to_subtype
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
The limit cone exhibiting ⨁ subtype.restrict pᶜ f as the kernel of
biproduct.to_subtype f p
Equations
- category_theory.limits.kernel_fork_biproduct_to_subtype f p = {cone := category_theory.limits.kernel_fork.of_ι (category_theory.limits.biproduct.from_subtype f pᶜ) _, is_limit := category_theory.limits.kernel_fork.is_limit.of_ι (category_theory.limits.biproduct.from_subtype f pᶜ) _ (λ (W : C) (g : W ⟶ ⨁ f) (h : g ≫ category_theory.limits.biproduct.to_subtype f p = 0), g ≫ category_theory.limits.biproduct.to_subtype f pᶜ) _ _}
@[protected, instance]
def
category_theory.limits.biproduct.to_subtype.has_kernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
noncomputable
def
category_theory.limits.kernel_biproduct_to_subtype_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
The kernel of biproduct.to_subtype f p is ⨁ subtype.restrict pᶜ f.
@[simp]
theorem
category_theory.limits.kernel_biproduct_to_subtype_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
@[simp]
theorem
category_theory.limits.kernel_biproduct_to_subtype_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
(category_theory.limits.kernel_biproduct_to_subtype_iso f p).hom = (category_theory.limits.kernel_fork.is_limit.of_ι (category_theory.limits.biproduct.from_subtype f pᶜ) _ (λ (W : C) (g : W ⟶ ⨁ f) (h : g ≫ category_theory.limits.biproduct.to_subtype f p = 0), g ≫ category_theory.limits.biproduct.to_subtype f pᶜ) _ _).lift (category_theory.limits.limit.cone (category_theory.limits.parallel_pair (category_theory.limits.biproduct.to_subtype f p) 0))
noncomputable
def
category_theory.limits.cokernel_cofork_biproduct_from_subtype
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
The colimit cocone exhibiting ⨁ subtype.restrict pᶜ f as the cokernel of
biproduct.from_subtype f p
Equations
- category_theory.limits.cokernel_cofork_biproduct_from_subtype f p = {cocone := category_theory.limits.cokernel_cofork.of_π (category_theory.limits.biproduct.to_subtype f pᶜ) _, is_colimit := category_theory.limits.cokernel_cofork.is_colimit.of_π (category_theory.limits.biproduct.to_subtype f pᶜ) _ (λ (W : C) (g : ⨁ f ⟶ W) (h : category_theory.limits.biproduct.from_subtype f p ≫ g = 0), category_theory.limits.biproduct.from_subtype f pᶜ ≫ g) _ _}
@[simp]
theorem
category_theory.limits.cokernel_cofork_biproduct_from_subtype_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
(category_theory.limits.cokernel_cofork_biproduct_from_subtype f p).is_colimit = category_theory.limits.cokernel_cofork.is_colimit.of_π (category_theory.limits.biproduct.to_subtype f pᶜ) _ (λ (W : C) (g : ⨁ f ⟶ W) (h : category_theory.limits.biproduct.from_subtype f p ≫ g = 0), category_theory.limits.biproduct.from_subtype f pᶜ ≫ g) _ _
@[simp]
theorem
category_theory.limits.cokernel_cofork_biproduct_from_subtype_cocone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
@[protected, instance]
def
category_theory.limits.biproduct.from_subtype.has_cokernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
@[simp]
theorem
category_theory.limits.cokernel_biproduct_from_subtype_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
noncomputable
def
category_theory.limits.cokernel_biproduct_from_subtype_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
The cokernel of biproduct.from_subtype f p is ⨁ subtype.restrict pᶜ f.
@[simp]
theorem
category_theory.limits.cokernel_biproduct_from_subtype_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{K : Type}
[fintype K]
[category_theory.limits.has_finite_biproducts C]
(f : K → C)
(p : set K) :
(category_theory.limits.cokernel_biproduct_from_subtype_iso f p).inv = (category_theory.limits.cokernel_cofork.is_colimit.of_π (category_theory.limits.biproduct.to_subtype f pᶜ) _ (λ (W : C) (g : ⨁ f ⟶ W) (h : category_theory.limits.biproduct.from_subtype f p ≫ g = 0), category_theory.limits.biproduct.from_subtype f pᶜ ≫ g) _ _).desc (category_theory.limits.colimit.cocone (category_theory.limits.parallel_pair (category_theory.limits.biproduct.from_subtype f p) 0))
noncomputable
def
category_theory.limits.biproduct.matrix
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k) :
Convert a (dependently typed) matrix to a morphism of biproducts.
Equations
- category_theory.limits.biproduct.matrix m = category_theory.limits.biproduct.desc (λ (j : J), category_theory.limits.biproduct.lift (λ (k : K), m j k))
@[simp]
theorem
category_theory.limits.biproduct.matrix_π
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k)
(k : K) :
category_theory.limits.biproduct.matrix m ≫ category_theory.limits.biproduct.π g k = category_theory.limits.biproduct.desc (λ (j : J), m j k)
@[simp]
theorem
category_theory.limits.biproduct.matrix_π_assoc
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k)
(k : K)
{X' : C}
(f' : g k ⟶ X') :
category_theory.limits.biproduct.matrix m ≫ category_theory.limits.biproduct.π g k ≫ f' = category_theory.limits.biproduct.desc (λ (j : J), m j k) ≫ f'
@[simp]
theorem
category_theory.limits.biproduct.ι_matrix_assoc
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k)
(j : J)
{X' : C}
(f' : (⨁ λ (k : K), g k) ⟶ X') :
@[simp]
theorem
category_theory.limits.biproduct.ι_matrix
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k)
(j : J) :
category_theory.limits.biproduct.ι f j ≫ category_theory.limits.biproduct.matrix m = category_theory.limits.biproduct.lift (λ (k : K), m j k)
noncomputable
def
category_theory.limits.biproduct.components
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : ⨁ f ⟶ ⨁ g)
(j : J)
(k : K) :
f j ⟶ g k
Extract the matrix components from a morphism of biproducts.
Equations
@[simp]
theorem
category_theory.limits.biproduct.matrix_components
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : Π (j : J) (k : K), f j ⟶ g k)
(j : J)
(k : K) :
@[simp]
theorem
category_theory.limits.biproduct.components_matrix
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : ⨁ f ⟶ ⨁ g) :
category_theory.limits.biproduct.matrix (λ (j : J) (k : K), category_theory.limits.biproduct.components m j k) = m
noncomputable
def
category_theory.limits.biproduct.matrix_equiv
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C} :
Morphisms between direct sums are matrices.
Equations
- category_theory.limits.biproduct.matrix_equiv = {to_fun := category_theory.limits.biproduct.components g, inv_fun := category_theory.limits.biproduct.matrix (λ (k : K), g k), left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.limits.biproduct.matrix_equiv_symm_apply
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : Π (j : J) (k : K), (λ (j : J), f j) j ⟶ (λ (k : K), g k) k) :
@[simp]
theorem
category_theory.limits.biproduct.matrix_equiv_apply
{J : Type}
[fintype J]
{K : Type}
[fintype K]
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C]
{f : J → C}
{g : K → C}
(m : ⨁ f ⟶ ⨁ g)
(j : J)
(k : K) :
@[protected, instance]
def
category_theory.limits.biproduct.ι_mono
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(b : J) :
@[protected, instance]
def
category_theory.limits.biproduct.π_epi
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
(b : J) :
theorem
category_theory.limits.biproduct.cone_point_unique_up_to_iso_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
{b : category_theory.limits.bicone f}
(hb : b.is_bilimit) :
Auxiliary lemma for biproduct.unique_up_to_iso.
theorem
category_theory.limits.biproduct.cone_point_unique_up_to_iso_inv
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
{b : category_theory.limits.bicone f}
(hb : b.is_bilimit) :
Auxiliary lemma for biproduct.unique_up_to_iso.
noncomputable
def
category_theory.limits.biproduct.unique_up_to_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
{b : category_theory.limits.bicone f}
(hb : b.is_bilimit) :
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
@[simp]
theorem
category_theory.limits.biproduct.unique_up_to_iso_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
{b : category_theory.limits.bicone f}
(hb : b.is_bilimit) :
@[simp]
theorem
category_theory.limits.biproduct.unique_up_to_iso_inv
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(f : J → C)
[category_theory.limits.has_biproduct f]
{b : category_theory.limits.bicone f}
(hb : b.is_bilimit) :
@[protected, instance]
def
category_theory.limits.has_zero_object_of_has_finite_biproducts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C] :
A category with finite biproducts has a zero object.
@[simp]
theorem
category_theory.limits.limit_bicone_of_unique_bicone_ι
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C)
(j : J) :
@[simp]
theorem
category_theory.limits.limit_bicone_of_unique_is_bilimit_is_colimit
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C) :
def
category_theory.limits.limit_bicone_of_unique
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C) :
The limit bicone for the biproduct over an index type with exactly one term.
Equations
- category_theory.limits.limit_bicone_of_unique f = {bicone := {X := f inhabited.default, π := λ (j : J), category_theory.eq_to_hom _, ι := λ (j : J), category_theory.eq_to_hom _, ι_π := _}, is_bilimit := {is_limit := (category_theory.limits.limit_cone_of_unique f).is_limit, is_colimit := (category_theory.limits.colimit_cocone_of_unique f).is_colimit}}
@[simp]
theorem
category_theory.limits.limit_bicone_of_unique_bicone_X
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C) :
@[simp]
theorem
category_theory.limits.limit_bicone_of_unique_bicone_π
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C)
(j : J) :
@[simp]
theorem
category_theory.limits.limit_bicone_of_unique_is_bilimit_is_limit
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C) :
@[protected, instance]
def
category_theory.limits.has_biproduct_unique
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C) :
noncomputable
def
category_theory.limits.biproduct_unique_iso
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C) :
⨁ f ≅ f inhabited.default
A biproduct over a index type with exactly one term is just the object over that term.
@[simp]
theorem
category_theory.limits.biproduct_unique_iso_hom
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C) :
@[simp]
theorem
category_theory.limits.biproduct_unique_iso_inv
{J : Type w}
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[unique J]
(f : J → C) :
@[nolint]
structure
category_theory.limits.binary_bicone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(P Q : C) :
Type (max u v)
- X : C
- fst : self.X ⟶ P
- snd : self.X ⟶ Q
- inl : P ⟶ self.X
- inr : Q ⟶ self.X
- inl_fst' : self.inl ≫ self.fst = 𝟙 P . "obviously"
- inl_snd' : self.inl ≫ self.snd = 0 . "obviously"
- inr_fst' : self.inr ≫ self.fst = 0 . "obviously"
- inr_snd' : self.inr ≫ self.snd = 𝟙 Q . "obviously"
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
Instances for category_theory.limits.binary_bicone
- category_theory.limits.binary_bicone.has_sizeof_inst
@[simp]
theorem
category_theory.limits.binary_bicone.inl_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(self : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.inl_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(self : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.inr_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(self : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.inr_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(self : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.inr_snd_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(self : category_theory.limits.binary_bicone P Q)
{X' : C}
(f' : Q ⟶ X') :
@[simp]
theorem
category_theory.limits.binary_bicone.inl_fst_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(self : category_theory.limits.binary_bicone P Q)
{X' : C}
(f' : P ⟶ X') :
@[simp]
theorem
category_theory.limits.binary_bicone.inr_fst_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(self : category_theory.limits.binary_bicone P Q)
{X' : C}
(f' : P ⟶ X') :
@[simp]
theorem
category_theory.limits.binary_bicone.inl_snd_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(self : category_theory.limits.binary_bicone P Q)
{X' : C}
(f' : Q ⟶ X') :
def
category_theory.limits.binary_bicone.to_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
Extract the cone from a binary bicone.
Equations
@[simp]
theorem
category_theory.limits.binary_bicone.to_cone_X
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.to_cone_π_app_left
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.to_cone_π_app_right
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.binary_fan_fst_to_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.binary_fan_snd_to_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
def
category_theory.limits.binary_bicone.to_cocone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
Extract the cocone from a binary bicone.
Equations
@[simp]
theorem
category_theory.limits.binary_bicone.to_cocone_X
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.to_cocone_ι_app_left
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.to_cocone_ι_app_right
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.binary_cofan_inl_to_cocone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
@[simp]
theorem
category_theory.limits.binary_bicone.binary_cofan_inr_to_cocone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(c : category_theory.limits.binary_bicone P Q) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem
category_theory.limits.binary_bicone.to_bicone_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y)
(j : category_theory.limits.walking_pair) :
def
category_theory.limits.binary_bicone.to_bicone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
Convert a binary_bicone into a bicone over a pair.
@[simp]
theorem
category_theory.limits.binary_bicone.to_bicone_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y)
(j : category_theory.limits.walking_pair) :
@[simp]
theorem
category_theory.limits.binary_bicone.to_bicone_X
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
def
category_theory.limits.binary_bicone.to_bicone_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
A binary bicone is a limit cone if and only if the corresponding bicone is a limit cone.
def
category_theory.limits.binary_bicone.to_bicone_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
A binary bicone is a colimit cocone if and only if the corresponding bicone is a colimit cocone.
@[simp]
theorem
category_theory.limits.bicone.to_binary_bicone_inl
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.bicone (category_theory.limits.pair_function X Y)) :
def
category_theory.limits.bicone.to_binary_bicone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.bicone (category_theory.limits.pair_function X Y)) :
Convert a bicone over a function on walking_pair to a binary_bicone.
Equations
- b.to_binary_bicone = {X := b.X, fst := b.π category_theory.limits.walking_pair.left, snd := b.π category_theory.limits.walking_pair.right, inl := b.ι category_theory.limits.walking_pair.left, inr := b.ι category_theory.limits.walking_pair.right, inl_fst' := _, inl_snd' := _, inr_fst' := _, inr_snd' := _}
@[simp]
theorem
category_theory.limits.bicone.to_binary_bicone_X
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.bicone (category_theory.limits.pair_function X Y)) :
b.to_binary_bicone.X = b.X
@[simp]
theorem
category_theory.limits.bicone.to_binary_bicone_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.bicone (category_theory.limits.pair_function X Y)) :
@[simp]
theorem
category_theory.limits.bicone.to_binary_bicone_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.bicone (category_theory.limits.pair_function X Y)) :
@[simp]
theorem
category_theory.limits.bicone.to_binary_bicone_inr
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.bicone (category_theory.limits.pair_function X Y)) :
def
category_theory.limits.bicone.to_binary_bicone_is_limit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.bicone (category_theory.limits.pair_function X Y)) :
A bicone over a pair is a limit cone if and only if the corresponding binary bicone is a limit cone.
def
category_theory.limits.bicone.to_binary_bicone_is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.bicone (category_theory.limits.pair_function X Y)) :
A bicone over a pair is a colimit cocone if and only if the corresponding binary bicone is a colimit cocone.
@[nolint]
structure
category_theory.limits.binary_bicone.is_bilimit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(b : category_theory.limits.binary_bicone P Q) :
Type (max u v)
- is_limit : category_theory.limits.is_limit b.to_cone
- is_colimit : category_theory.limits.is_colimit b.to_cocone
Structure witnessing that a binary bicone is a limit cone and a limit cocone.
Instances for category_theory.limits.binary_bicone.is_bilimit
- category_theory.limits.binary_bicone.is_bilimit.has_sizeof_inst
def
category_theory.limits.binary_bicone.to_bicone_is_bilimit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit.
Equations
- b.to_bicone_is_bilimit = {to_fun := λ (h : b.to_bicone.is_bilimit), {is_limit := ⇑(b.to_bicone_is_limit) h.is_limit, is_colimit := ⇑(b.to_bicone_is_colimit) h.is_colimit}, inv_fun := λ (h : b.is_bilimit), {is_limit := ⇑(b.to_bicone_is_limit.symm) h.is_limit, is_colimit := ⇑(b.to_bicone_is_colimit.symm) h.is_colimit}, left_inv := _, right_inv := _}
def
category_theory.limits.bicone.to_binary_bicone_is_bilimit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(b : category_theory.limits.bicone (category_theory.limits.pair_function X Y)) :
A bicone over a pair is a bilimit bicone if and only if the corresponding binary bicone is a bilimit.
Equations
- b.to_binary_bicone_is_bilimit = {to_fun := λ (h : b.to_binary_bicone.is_bilimit), {is_limit := ⇑(b.to_binary_bicone_is_limit) h.is_limit, is_colimit := ⇑(b.to_binary_bicone_is_colimit) h.is_colimit}, inv_fun := λ (h : b.is_bilimit), {is_limit := ⇑(b.to_binary_bicone_is_limit.symm) h.is_limit, is_colimit := ⇑(b.to_binary_bicone_is_colimit.symm) h.is_colimit}, left_inv := _, right_inv := _}
@[nolint]
structure
category_theory.limits.binary_biproduct_data
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(P Q : C) :
Type (max u v)
- bicone : category_theory.limits.binary_bicone P Q
- is_bilimit : self.bicone.is_bilimit
A bicone over P Q : C, which is both a limit cone and a colimit cocone.
Instances for category_theory.limits.binary_biproduct_data
- category_theory.limits.binary_biproduct_data.has_sizeof_inst
@[class]
structure
category_theory.limits.has_binary_biproduct
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(P Q : C) :
Prop
- exists_binary_biproduct : nonempty (category_theory.limits.binary_biproduct_data P Q)
has_binary_biproduct P Q expresses the mere existence of a bicone which is
simultaneously a limit and a colimit of the diagram pair P Q.
theorem
category_theory.limits.has_binary_biproduct.mk
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{P Q : C}
(d : category_theory.limits.binary_biproduct_data P Q) :
noncomputable
def
category_theory.limits.get_binary_biproduct_data
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(P Q : C)
[category_theory.limits.has_binary_biproduct P Q] :
Use the axiom of choice to extract explicit binary_biproduct_data F from has_binary_biproduct F.
noncomputable
def
category_theory.limits.binary_biproduct.bicone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(P Q : C)
[category_theory.limits.has_binary_biproduct P Q] :
A bicone for P Q which is both a limit cone and a colimit cocone.
noncomputable
def
category_theory.limits.binary_biproduct.is_bilimit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(P Q : C)
[category_theory.limits.has_binary_biproduct P Q] :
binary_biproduct.bicone P Q is a limit bicone.
noncomputable
def
category_theory.limits.binary_biproduct.is_limit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(P Q : C)
[category_theory.limits.has_binary_biproduct P Q] :
binary_biproduct.bicone P Q is a limit cone.
noncomputable
def
category_theory.limits.binary_biproduct.is_colimit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(P Q : C)
[category_theory.limits.has_binary_biproduct P Q] :
binary_biproduct.bicone P Q is a colimit cocone.
@[class]
structure
category_theory.limits.has_binary_biproducts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
Prop
- has_binary_biproduct : ∀ (P Q : C), category_theory.limits.has_binary_biproduct P Q
has_binary_biproducts C represents the existence of a bicone which is
simultaneously a limit and a colimit of the diagram pair P Q, for every P Q : C.
theorem
category_theory.limits.has_binary_biproducts_of_finite_biproducts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_finite_biproducts C] :
A category with finite biproducts has binary biproducts.
This is not an instance as typically in concrete categories there will be an alternative construction with nicer definitional properties.
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable
def
category_theory.limits.biprod_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The isomorphism between the specified binary product and the specified binary coproduct for a pair for a binary biproduct.
Equations
- category_theory.limits.biprod_iso X Y = (category_theory.limits.limit.is_limit (category_theory.limits.pair X Y)).cone_point_unique_up_to_iso (category_theory.limits.binary_biproduct.is_limit X Y) ≪≫ (category_theory.limits.binary_biproduct.is_colimit X Y).cocone_point_unique_up_to_iso (category_theory.limits.colimit.is_colimit (category_theory.limits.pair X Y))
@[reducible]
noncomputable
def
category_theory.limits.biprod
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
C
An arbitrary choice of biproduct of a pair of objects.
@[reducible]
noncomputable
def
category_theory.limits.biprod.fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
The projection onto the first summand of a binary biproduct.
@[reducible]
noncomputable
def
category_theory.limits.biprod.snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
The projection onto the second summand of a binary biproduct.
@[reducible]
noncomputable
def
category_theory.limits.biprod.inl
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
The inclusion into the first summand of a binary biproduct.
@[reducible]
noncomputable
def
category_theory.limits.biprod.inr
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
The inclusion into the second summand of a binary biproduct.
@[simp]
theorem
category_theory.limits.binary_biproduct.bicone_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
theorem
category_theory.limits.binary_biproduct.bicone_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
theorem
category_theory.limits.binary_biproduct.bicone_inl
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
theorem
category_theory.limits.binary_biproduct.bicone_inr
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
@[simp]
theorem
category_theory.limits.biprod.inl_fst_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
{X' : C}
(f' : X ⟶ X') :
@[simp]
@[simp]
theorem
category_theory.limits.biprod.inl_snd_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
{X' : C}
(f' : Y ⟶ X') :
@[simp]
@[simp]
theorem
category_theory.limits.biprod.inr_fst_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
{X' : C}
(f' : X ⟶ X') :
@[simp]
@[simp]
theorem
category_theory.limits.biprod.inr_snd_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
{X' : C}
(f' : Y ⟶ X') :
@[reducible]
noncomputable
def
category_theory.limits.biprod.lift
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : W ⟶ X)
(g : W ⟶ Y) :
Given a pair of maps into the summands of a binary biproduct, we obtain a map into the binary biproduct.
@[reducible]
noncomputable
def
category_theory.limits.biprod.desc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : X ⟶ W)
(g : Y ⟶ W) :
Given a pair of maps out of the summands of a binary biproduct, we obtain a map out of the binary biproduct.
@[simp]
theorem
category_theory.limits.biprod.lift_fst_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : W ⟶ X)
(g : W ⟶ Y)
{X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.limits.biprod.lift_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : W ⟶ X)
(g : W ⟶ Y) :
@[simp]
theorem
category_theory.limits.biprod.lift_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : W ⟶ X)
(g : W ⟶ Y) :
@[simp]
theorem
category_theory.limits.biprod.lift_snd_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : W ⟶ X)
(g : W ⟶ Y)
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.biprod.inl_desc_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : X ⟶ W)
(g : Y ⟶ W)
{X' : C}
(f' : W ⟶ X') :
@[simp]
theorem
category_theory.limits.biprod.inl_desc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : X ⟶ W)
(g : Y ⟶ W) :
@[simp]
theorem
category_theory.limits.biprod.inr_desc_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : X ⟶ W)
(g : Y ⟶ W)
{X' : C}
(f' : W ⟶ X') :
@[simp]
theorem
category_theory.limits.biprod.inr_desc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : X ⟶ W)
(g : Y ⟶ W) :
@[protected, instance]
def
category_theory.limits.biprod.mono_lift_of_mono_left
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : W ⟶ X)
(g : W ⟶ Y)
[category_theory.mono f] :
@[protected, instance]
def
category_theory.limits.biprod.mono_lift_of_mono_right
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : W ⟶ X)
(g : W ⟶ Y)
[category_theory.mono g] :
@[protected, instance]
def
category_theory.limits.biprod.epi_desc_of_epi_left
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : X ⟶ W)
(g : Y ⟶ W)
[category_theory.epi f] :
@[protected, instance]
def
category_theory.limits.biprod.epi_desc_of_epi_right
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(f : X ⟶ W)
(g : Y ⟶ W)
[category_theory.epi g] :
@[reducible]
noncomputable
def
category_theory.limits.biprod.map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z) :
Given a pair of maps between the summands of a pair of binary biproducts, we obtain a map between the binary biproducts.
@[reducible]
noncomputable
def
category_theory.limits.biprod.map'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z) :
An alternative to biprod.map constructed via colimits.
This construction only exists in order to show it is equal to biprod.map.
@[ext]
theorem
category_theory.limits.biprod.hom_ext
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
[category_theory.limits.has_binary_biproduct X Y]
(f g : Z ⟶ X ⊞ Y)
(h₀ : f ≫ category_theory.limits.biprod.fst = g ≫ category_theory.limits.biprod.fst)
(h₁ : f ≫ category_theory.limits.biprod.snd = g ≫ category_theory.limits.biprod.snd) :
f = g
@[ext]
theorem
category_theory.limits.biprod.hom_ext'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
[category_theory.limits.has_binary_biproduct X Y]
(f g : X ⊞ Y ⟶ Z)
(h₀ : category_theory.limits.biprod.inl ≫ f = category_theory.limits.biprod.inl ≫ g)
(h₁ : category_theory.limits.biprod.inr ≫ f = category_theory.limits.biprod.inr ≫ g) :
f = g
noncomputable
def
category_theory.limits.biprod.iso_prod
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The canonical isomorphism between the chosen biproduct and the chosen product.
@[simp]
theorem
category_theory.limits.biprod.iso_prod_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
theorem
category_theory.limits.biprod.iso_prod_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
noncomputable
def
category_theory.limits.biprod.iso_coprod
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The canonical isomorphism between the chosen biproduct and the chosen coproduct.
@[simp]
theorem
category_theory.limits.biprod.iso_coprod_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
theorem
category_theory.limits.biprod_iso_coprod_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
theorem
category_theory.limits.biprod.map_eq_map'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem
category_theory.limits.biprod.map_fst_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z)
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.biprod.map_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.biprod.map_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.biprod.map_snd_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z)
{X' : C}
(f' : Z ⟶ X') :
@[simp]
theorem
category_theory.limits.biprod.inl_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.biprod.inl_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z)
{X' : C}
(f' : Y ⊞ Z ⟶ X') :
@[simp]
theorem
category_theory.limits.biprod.inr_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.biprod.inr_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ⟶ Y)
(g : X ⟶ Z)
{X' : C}
(f' : Y ⊞ Z ⟶ X') :
noncomputable
def
category_theory.limits.biprod.map_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ≅ Y)
(g : X ≅ Z) :
Given a pair of isomorphisms between the summands of a pair of binary biproducts, we obtain an isomorphism between the binary biproducts.
Equations
- category_theory.limits.biprod.map_iso f g = {hom := category_theory.limits.biprod.map f.hom g.hom, inv := category_theory.limits.biprod.map f.inv g.inv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.biprod.map_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ≅ Y)
(g : X ≅ Z) :
@[simp]
theorem
category_theory.limits.biprod.map_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{W X Y Z : C}
[category_theory.limits.has_binary_biproduct W X]
[category_theory.limits.has_binary_biproduct Y Z]
(f : W ≅ Y)
(g : X ≅ Z) :
theorem
category_theory.limits.biprod.cone_point_unique_up_to_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
{b : category_theory.limits.binary_bicone X Y}
(hb : b.is_bilimit) :
Auxiliary lemma for biprod.unique_up_to_iso.
theorem
category_theory.limits.biprod.cone_point_unique_up_to_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
{b : category_theory.limits.binary_bicone X Y}
(hb : b.is_bilimit) :
Auxiliary lemma for biprod.unique_up_to_iso.
@[simp]
theorem
category_theory.limits.biprod.unique_up_to_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
{b : category_theory.limits.binary_bicone X Y}
(hb : b.is_bilimit) :
noncomputable
def
category_theory.limits.biprod.unique_up_to_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
{b : category_theory.limits.binary_bicone X Y}
(hb : b.is_bilimit) :
Binary 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 biprod.lift b.fst b.snd and biprod.desc b.inl b.inr
are inverses of each other.
Equations
- category_theory.limits.biprod.unique_up_to_iso X Y hb = {hom := category_theory.limits.biprod.lift b.fst b.snd, inv := category_theory.limits.biprod.desc b.inl b.inr, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.biprod.unique_up_to_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
{b : category_theory.limits.binary_bicone X Y}
(hb : b.is_bilimit) :
theorem
category_theory.limits.biprod.is_iso_inl_iff_id_eq_fst_comp_inl
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
def
category_theory.limits.binary_bicone.fst_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(c : category_theory.limits.binary_bicone X Y) :
A kernel fork for the kernel of binary_bicone.fst. It consists of the morphism
binary_bicone.inr.
Equations
@[simp]
theorem
category_theory.limits.binary_bicone.fst_kernel_fork_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(c : category_theory.limits.binary_bicone X Y) :
def
category_theory.limits.binary_bicone.snd_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(c : category_theory.limits.binary_bicone X Y) :
A kernel fork for the kernel of binary_bicone.snd. It consists of the morphism
binary_bicone.inl.
Equations
@[simp]
theorem
category_theory.limits.binary_bicone.snd_kernel_fork_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(c : category_theory.limits.binary_bicone X Y) :
def
category_theory.limits.binary_bicone.inl_cokernel_cofork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(c : category_theory.limits.binary_bicone X Y) :
A cokernel cofork for the cokernel of binary_bicone.inl. It consists of the morphism
binary_bicone.snd.
Equations
@[simp]
theorem
category_theory.limits.binary_bicone.inl_cokernel_cofork_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(c : category_theory.limits.binary_bicone X Y) :
def
category_theory.limits.binary_bicone.inr_cokernel_cofork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(c : category_theory.limits.binary_bicone X Y) :
A cokernel cofork for the cokernel of binary_bicone.inr. It consists of the morphism
binary_bicone.fst.
Equations
@[simp]
theorem
category_theory.limits.binary_bicone.inr_cokernel_cofork_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(c : category_theory.limits.binary_bicone X Y) :
def
category_theory.limits.binary_bicone.is_limit_fst_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{c : category_theory.limits.binary_bicone X Y}
(i : category_theory.limits.is_limit c.to_cone) :
The fork defined in binary_bicone.fst_kernel_fork is indeed a kernel.
Equations
def
category_theory.limits.binary_bicone.is_limit_snd_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{c : category_theory.limits.binary_bicone X Y}
(i : category_theory.limits.is_limit c.to_cone) :
The fork defined in binary_bicone.snd_kernel_fork is indeed a kernel.
Equations
def
category_theory.limits.binary_bicone.is_colimit_inl_cokernel_cofork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{c : category_theory.limits.binary_bicone X Y}
(i : category_theory.limits.is_colimit c.to_cocone) :
The cofork defined in binary_bicone.inl_cokernel_cofork is indeed a cokernel.
Equations
def
category_theory.limits.binary_bicone.is_colimit_inr_cokernel_cofork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{c : category_theory.limits.binary_bicone X Y}
(i : category_theory.limits.is_colimit c.to_cocone) :
The cofork defined in binary_bicone.inr_cokernel_cofork is indeed a cokernel.
Equations
noncomputable
def
category_theory.limits.biprod.fst_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
A kernel fork for the kernel of biprod.fst. It consists of the
morphism biprod.inr.
@[simp]
theorem
category_theory.limits.biprod.fst_kernel_fork_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
noncomputable
def
category_theory.limits.biprod.is_kernel_fst_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The fork biprod.fst_kernel_fork is indeed a limit.
noncomputable
def
category_theory.limits.biprod.snd_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
A kernel fork for the kernel of biprod.snd. It consists of the
morphism biprod.inl.
@[simp]
theorem
category_theory.limits.biprod.snd_kernel_fork_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
noncomputable
def
category_theory.limits.biprod.is_kernel_snd_kernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The fork biprod.snd_kernel_fork is indeed a limit.
noncomputable
def
category_theory.limits.biprod.inl_cokernel_cofork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
A cokernel cofork for the cokernel of biprod.inl. It consists of the
morphism biprod.snd.
@[simp]
theorem
category_theory.limits.biprod.inl_cokernel_cofork_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
noncomputable
def
category_theory.limits.biprod.is_cokernel_inl_cokernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The cofork biprod.inl_cokernel_fork is indeed a colimit.
noncomputable
def
category_theory.limits.biprod.inr_cokernel_cofork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
A cokernel cofork for the cokernel of biprod.inr. It consists of the
morphism biprod.fst.
@[simp]
theorem
category_theory.limits.biprod.inr_cokernel_cofork_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
noncomputable
def
category_theory.limits.biprod.is_cokernel_inr_cokernel_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y] :
The cofork biprod.inr_cokernel_fork is indeed a colimit.
@[protected, instance]
noncomputable
def
category_theory.limits.kernel_biprod_fst_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
The kernel of biprod.fst : X ⊞ Y ⟶ X is Y.
@[simp]
theorem
category_theory.limits.kernel_biprod_fst_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
theorem
category_theory.limits.kernel_biprod_fst_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[protected, instance]
noncomputable
def
category_theory.limits.kernel_biprod_snd_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
The kernel of biprod.snd : X ⊞ Y ⟶ Y is X.
@[simp]
theorem
category_theory.limits.kernel_biprod_snd_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
theorem
category_theory.limits.kernel_biprod_snd_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[protected, instance]
@[simp]
theorem
category_theory.limits.cokernel_biprod_inl_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
theorem
category_theory.limits.cokernel_biprod_inl_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
noncomputable
def
category_theory.limits.cokernel_biprod_inl_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
The cokernel of biprod.inl : X ⟶ X ⊞ Y is Y.
@[protected, instance]
@[simp]
theorem
category_theory.limits.cokernel_biprod_inr_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
@[simp]
theorem
category_theory.limits.cokernel_biprod_inr_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
noncomputable
def
category_theory.limits.cokernel_biprod_inr_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y] :
The cokernel of biprod.inr : Y ⟶ X ⊞ Y is X.
noncomputable
def
category_theory.limits.iso_biprod_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(hY : category_theory.limits.is_zero Y) :
If Y is a zero object, X ≅ X ⊞ Y for any X.
Equations
- category_theory.limits.iso_biprod_zero hY = {hom := category_theory.limits.biprod.inl _inst_3, inv := category_theory.limits.biprod.fst _inst_3, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.iso_biprod_zero_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(hY : category_theory.limits.is_zero Y) :
@[simp]
theorem
category_theory.limits.iso_biprod_zero_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(hY : category_theory.limits.is_zero Y) :
@[simp]
theorem
category_theory.limits.iso_zero_biprod_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(hY : category_theory.limits.is_zero X) :
@[simp]
theorem
category_theory.limits.iso_zero_biprod_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(hY : category_theory.limits.is_zero X) :
noncomputable
def
category_theory.limits.iso_zero_biprod
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_binary_biproduct X Y]
(hY : category_theory.limits.is_zero X) :
If X is a zero object, Y ≅ X ⊞ Y for any Y.
Equations
- category_theory.limits.iso_zero_biprod hY = {hom := category_theory.limits.biprod.inr _inst_3, inv := category_theory.limits.biprod.snd _inst_3, hom_inv_id' := _, inv_hom_id' := _}
noncomputable
def
category_theory.limits.biprod.braiding
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C) :
The braiding isomorphism which swaps a binary biproduct.
Equations
- category_theory.limits.biprod.braiding P Q = {hom := category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst, inv := category_theory.limits.biprod.lift category_theory.limits.biprod.snd category_theory.limits.biprod.fst, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.biprod.braiding_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C) :
@[simp]
theorem
category_theory.limits.biprod.braiding_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C) :
@[simp]
theorem
category_theory.limits.biprod.braiding'_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C) :
noncomputable
def
category_theory.limits.biprod.braiding'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C) :
An alternative formula for the braiding isomorphism which swaps a binary biproduct, using the fact that the biproduct is a coproduct.
Equations
- category_theory.limits.biprod.braiding' P Q = {hom := category_theory.limits.biprod.desc category_theory.limits.biprod.inr category_theory.limits.biprod.inl, inv := category_theory.limits.biprod.desc category_theory.limits.biprod.inr category_theory.limits.biprod.inl, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.biprod.braiding'_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C) :
theorem
category_theory.limits.biprod.braid_natural_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : Z ⟶ W)
{X' : C}
(f' : W ⊞ Y ⟶ X') :
theorem
category_theory.limits.biprod.braid_natural
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : Z ⟶ W) :
The braiding isomorphism can be passed through a map by swapping the order.
theorem
category_theory.limits.biprod.braiding_map_braiding_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z)
{X' : C}
(f' : Z ⊞ Y ⟶ X') :
theorem
category_theory.limits.biprod.braiding_map_braiding
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.biprod.symmetry'_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C)
{X' : C}
(f' : P ⊞ Q ⟶ X') :
@[simp]
theorem
category_theory.limits.biprod.symmetry'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C) :
theorem
category_theory.limits.biprod.symmetry_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C)
{X' : C}
(f' : P ⊞ Q ⟶ X') :
(category_theory.limits.biprod.braiding P Q).hom ≫ (category_theory.limits.biprod.braiding Q P).hom ≫ f' = f'
theorem
category_theory.limits.biprod.symmetry
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(P Q : C) :
(category_theory.limits.biprod.braiding P Q).hom ≫ (category_theory.limits.biprod.braiding Q P).hom = 𝟙 (P ⊞ Q)
The braiding isomorphism is symmetric.
def
category_theory.indecomposable
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
(X : C) :
Prop
An object is indecomposable if it cannot be written as the biproduct of two nonzero objects.
Equations
- category_theory.indecomposable X = (¬category_theory.limits.is_zero X ∧ ∀ (Y Z : C), (X ≅ Y ⊞ Z) → category_theory.limits.is_zero Y ∨ category_theory.limits.is_zero Z)
theorem
category_theory.is_iso_left_of_is_iso_biprod_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso (category_theory.limits.biprod.map f g)] :
If
(f 0)
(0 g)
is invertible, then f is invertible.
theorem
category_theory.is_iso_right_of_is_iso_biprod_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_binary_biproducts C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z)
[category_theory.is_iso (category_theory.limits.biprod.map f g)] :
If
(f 0)
(0 g)
is invertible, then g is invertible.