Binary (co)products
We define a category walking_pair
, which is the index category
for a binary (co)product diagram. A convenience method pair X Y
constructs the functor from the walking pair, hitting the given objects.
We define prod X Y
and coprod X Y
as limits and colimits of such functors.
Typeclasses has_binary_products
and has_binary_coproducts
assert the existence
of (co)limits shaped as walking pairs.
We include lemmas for simplifying equations involving projections and coprojections, and define braiding and associating isomorphisms, and the product comparison morphism.
References
The type of objects for the diagram indexing a binary (co)product.
The equivalence swapping left and right.
Equations
- category_theory.limits.walking_pair.swap = {to_fun := λ (j : category_theory.limits.walking_pair), j.rec_on category_theory.limits.walking_pair.right category_theory.limits.walking_pair.left, inv_fun := λ (j : category_theory.limits.walking_pair), j.rec_on category_theory.limits.walking_pair.right category_theory.limits.walking_pair.left, left_inv := category_theory.limits.walking_pair.swap._proof_1, right_inv := category_theory.limits.walking_pair.swap._proof_2}
An equivalence from walking_pair
to bool
, sometimes useful when reindexing limits.
Equations
- category_theory.limits.walking_pair.equiv_bool = {to_fun := λ (j : category_theory.limits.walking_pair), j.rec_on tt ff, inv_fun := λ (b : bool), b.rec_on category_theory.limits.walking_pair.right category_theory.limits.walking_pair.left, left_inv := category_theory.limits.walking_pair.equiv_bool._proof_1, right_inv := category_theory.limits.walking_pair.equiv_bool._proof_2}
The diagram on the walking pair, sending the two points to X
and Y
.
Equations
- category_theory.limits.pair X Y = category_theory.discrete.functor (λ (j : category_theory.limits.walking_pair), j.cases_on X Y)
The natural transformation between two functors out of the walking pair, specified by its components.
Equations
- category_theory.limits.map_pair f g = {app := λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on j f g, naturality' := _}
The natural isomorphism between two functors out of the walking pair, specified by its components.
Equations
- category_theory.limits.map_pair_iso f g = category_theory.nat_iso.of_components (λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on j f g) _
Every functor out of the walking pair is naturally isomorphic (actually, equal) to a pair
The natural isomorphism between pair X Y ⋙ F
and pair (F.obj X) (F.obj Y)
.
Equations
A binary fan is just a cone on a diagram indexing a product.
The first projection of a binary fan.
The second projection of a binary fan.
A binary cofan is just a cocone on a diagram indexing a coproduct.
The first inclusion of a binary cofan.
The second inclusion of a binary cofan.
A binary fan with vertex P
consists of the two projections π₁ : P ⟶ X
and π₂ : P ⟶ Y
.
Equations
- category_theory.limits.binary_fan.mk π₁ π₂ = {X := P, π := {app := λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on j π₁ π₂, naturality' := _}}
A binary cofan with vertex P
consists of the two inclusions ι₁ : X ⟶ P
and ι₂ : Y ⟶ P
.
Equations
- category_theory.limits.binary_cofan.mk ι₁ ι₂ = {X := P, ι := {app := λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on j ι₁ ι₂, naturality' := _}}
If s
is a limit binary fan over X
and Y
, then every pair of morphisms f : W ⟶ X
and
g : W ⟶ Y
induces a morphism l : W ⟶ s.X
satisfying l ≫ s.fst = f
and l ≫ s.snd = g
.
Equations
If s
is a colimit binary cofan over X
and Y
,, then every pair of morphisms f : X ⟶ W
and
g : Y ⟶ W
induces a morphism l : s.X ⟶ W
satisfying s.inl ≫ l = f
and s.inr ≫ l = g
.
Equations
An abbreviation for has_limit (pair X Y)
.
Instances
An abbreviation for has_colimit (pair X Y)
.
If we have a product of X
and Y
, we can access it using prod X Y
or
X ⨯ Y
.
If we have a coproduct of X
and Y
, we can access it using coprod X Y
or
X ⨿ Y
.
The projection map to the first component of the product.
The projecton map to the second component of the product.
The inclusion map from the first component of the coproduct.
The inclusion map from the second component of the coproduct.
The binary fan constructed from the projection maps is a limit.
The binary cofan constructed from the coprojection maps is a colimit.
Equations
- category_theory.limits.coprod_is_coprod = (category_theory.limits.colimit.is_colimit (category_theory.limits.pair X Y)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl (category_theory.limits.colimit.cocone (category_theory.limits.pair X Y)).X) category_theory.limits.coprod_is_coprod._proof_1)
If the product of X
and Y
exists, then every pair of morphisms f : W ⟶ X
and g : W ⟶ Y
induces a morphism prod.lift f g : W ⟶ X ⨯ Y
.
diagonal arrow of the binary product in the category fam I
If the coproduct of X
and Y
exists, then every pair of morphisms f : X ⟶ W
and
g : Y ⟶ W
induces a morphism coprod.desc f g : X ⨿ Y ⟶ W
.
codiagonal arrow of the binary coproduct
If the product of X
and Y
exists, then every pair of morphisms f : W ⟶ X
and g : W ⟶ Y
induces a morphism l : W ⟶ X ⨯ Y
satisfying l ≫ prod.fst = f
and l ≫ prod.snd = g
.
Equations
If the coproduct of X
and Y
exists, then every pair of morphisms f : X ⟶ W
and
g : Y ⟶ W
induces a morphism l : X ⨿ Y ⟶ W
satisfying coprod.inl ≫ l = f
and
coprod.inr ≫ l = g
.
Equations
If the products W ⨯ X
and Y ⨯ Z
exist, then every pair of morphisms f : W ⟶ Y
and
g : X ⟶ Z
induces a morphism prod.map f g : W ⨯ X ⟶ Y ⨯ Z
.
If the coproducts W ⨿ X
and Y ⨿ Z
exist, then every pair of morphisms f : W ⟶ Y
and
g : W ⟶ Z
induces a morphism coprod.map f g : W ⨿ X ⟶ Y ⨿ Z
.
If the products W ⨯ X
and Y ⨯ Z
exist, then every pair of isomorphisms f : W ≅ Y
and
g : X ≅ Z
induces an isomorphism prod.map_iso f g : W ⨯ X ≅ Y ⨯ Z
.
Equations
- category_theory.limits.prod.map_iso f g = {hom := category_theory.limits.prod.map f.hom g.hom, inv := category_theory.limits.prod.map f.inv g.inv, hom_inv_id' := _, inv_hom_id' := _}
Equations
If the coproducts W ⨿ X
and Y ⨿ Z
exist, then every pair of isomorphisms f : W ≅ Y
and
g : W ≅ Z
induces a isomorphism coprod.map_iso f g : W ⨿ X ≅ Y ⨿ Z
.
Equations
- category_theory.limits.coprod.map_iso f g = {hom := category_theory.limits.coprod.map f.hom g.hom, inv := category_theory.limits.coprod.map f.inv g.inv, hom_inv_id' := _, inv_hom_id' := _}
has_binary_products
represents a choice of product for every pair of objects.
See https://stacks.math.columbia.edu/tag/001T.
has_binary_coproducts
represents a choice of coproduct for every pair of objects.
See https://stacks.math.columbia.edu/tag/04AP.
If C
has all limits of diagrams pair X Y
, then it has all binary products
If C
has all colimits of diagrams pair X Y
, then it has all binary coproducts
The braiding isomorphism which swaps a binary product.
The braiding isomorphism can be passed through a map by swapping the order.
The braiding isomorphism is symmetric.
The associator isomorphism for binary products.
Equations
- category_theory.limits.prod.associator P Q R = {hom := category_theory.limits.prod.lift (category_theory.limits.prod.fst ≫ category_theory.limits.prod.fst) (category_theory.limits.prod.lift (category_theory.limits.prod.fst ≫ category_theory.limits.prod.snd) category_theory.limits.prod.snd), inv := category_theory.limits.prod.lift (category_theory.limits.prod.lift category_theory.limits.prod.fst (category_theory.limits.prod.snd ≫ category_theory.limits.prod.fst)) (category_theory.limits.prod.snd ≫ category_theory.limits.prod.snd), hom_inv_id' := _, inv_hom_id' := _}
The left unitor isomorphism for binary products with the terminal object.
Equations
- category_theory.limits.prod.left_unitor P = {hom := category_theory.limits.prod.snd _inst_3, inv := category_theory.limits.prod.lift (category_theory.limits.terminal.from P) (𝟙 P), hom_inv_id' := _, inv_hom_id' := _}
The right unitor isomorphism for binary products with the terminal object.
Equations
- category_theory.limits.prod.right_unitor P = {hom := category_theory.limits.prod.fst _inst_3, inv := category_theory.limits.prod.lift (𝟙 P) (category_theory.limits.terminal.from P), hom_inv_id' := _, inv_hom_id' := _}
The braiding isomorphism which swaps a binary coproduct.
Equations
- category_theory.limits.coprod.braiding P Q = {hom := category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl, inv := category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl, hom_inv_id' := _, inv_hom_id' := _}
The braiding isomorphism is symmetric.
The associator isomorphism for binary coproducts.
Equations
- category_theory.limits.coprod.associator P Q R = {hom := category_theory.limits.coprod.desc (category_theory.limits.coprod.desc category_theory.limits.coprod.inl (category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.inr)) (category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.inr), inv := category_theory.limits.coprod.desc (category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.inl) (category_theory.limits.coprod.desc (category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.inl) category_theory.limits.coprod.inr), hom_inv_id' := _, inv_hom_id' := _}
The left unitor isomorphism for binary coproducts with the initial object.
Equations
The right unitor isomorphism for binary coproducts with the initial object.
Equations
The binary product functor.
Equations
- category_theory.limits.prod.functor = {obj := λ (X : C), {obj := λ (Y : C), X ⨯ Y, map := λ (Y Z : C), category_theory.limits.prod.map (𝟙 X), map_id' := _, map_comp' := _}, map := λ (Y Z : C) (f : Y ⟶ Z), {app := λ (T : C), category_theory.limits.prod.map f (𝟙 T), naturality' := _}, map_id' := _, map_comp' := _}
The product functor can be decomposed.
The binary coproduct functor.
Equations
- category_theory.limits.coprod.functor = {obj := λ (X : C), {obj := λ (Y : C), X ⨿ Y, map := λ (Y Z : C), category_theory.limits.coprod.map (𝟙 X), map_id' := _, map_comp' := _}, map := λ (Y Z : C) (f : Y ⟶ Z), {app := λ (T : C), category_theory.limits.coprod.map f (𝟙 T), naturality' := _}, map_id' := _, map_comp' := _}
The coproduct functor can be decomposed.
The product comparison morphism.
In category_theory/limits/preserves
we show this is always an iso iff F preserves binary products.
Naturality of the prod_comparison morphism in both arguments.
The product comparison morphism from F(A ⨯ -)
to FA ⨯ F-
, whose components are given by
prod_comparison
.
Equations
- category_theory.limits.prod_comparison_nat_trans F A = {app := λ (B : C), category_theory.limits.prod_comparison F A B, naturality' := _}
If the product comparison morphism is an iso, its inverse is natural.
The natural isomorphism F(A ⨯ -) ≅ FA ⨯ F-
, provided each prod_comparison F A B
is an
isomorphism (as B
changes).
Equations
- category_theory.limits.prod_comparison_nat_iso F A = {hom := category_theory.limits.prod_comparison_nat_trans F A, inv := category_theory.is_iso.inv {app := λ (B : C), category_theory.limits.prod_comparison F A B, naturality' := _} (category_theory.nat_iso.is_iso_of_is_iso_app {app := λ (B : C), category_theory.limits.prod_comparison F A B, naturality' := _}), hom_inv_id' := _, inv_hom_id' := _}