Theorems · Definition · category theory
CategoryTheory.Limits.coprod.map
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
{W X Y Z : C} →
[inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] →
[inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z] → (W ⟶ Y) → (X ⟶ Z) → (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.
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Limits.coprodstatement · cited by 252
- CategoryTheory.Limits.HasBinaryCoproductstatement and proof · cited by 81
- CategoryTheory.Limits.colimMapproof · cited by 69
- CategoryTheory.Limits.mapPairproof · cited by 18
Cited by54
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.coprod.map_descstatement · cited by 16
- AlgebraicGeometry.Scheme.Hom.normalizationCoprodIsoproof · cited by 15
- CategoryTheory.Limits.coprod.inl_mapstatement · cited by 11
- CategoryTheory.Limits.coprod.inr_mapstatement · cited by 10
- CategoryTheory.Limits.coprod.functorproof · cited by 8
- CategoryTheory.Limits.coprod.map_mapstatement and proof · cited by 5
- CategoryTheory.Limits.coprod.inr_map_assocstatement and proof · cited by 4
- CategoryTheory.Limits.coprod.mapIsoproof · cited by 4
- CategoryTheory.Over.coprodObjproof · cited by 4
- CategoryTheory.Limits.coprod.inl_map_assocstatement and proof · cited by 3
- CategoryTheory.Limits.coprod.mapIso_homstatement · cited by 2
- AlgebraicGeometry.isPullback_inl_inl_coprodMapstatement and proof · cited by 2