Binary (co)products

We define prod X Y and coprod X Y as limits and colimits of walking-pair diagrams.

Typeclasses HasBinaryProducts and HasBinaryCoproducts 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

• Stacks: Products of pairs
• Stacks: coproducts of pairs

@[reducible, inline]

abbrev CategoryTheory.Limits.HasBinaryProduct {C : Type u} [Category.{v, u} C] (X Y : C) : Prop

An abbreviation for HasLimit (pair X Y).

Equations

• CategoryTheory.Limits.HasBinaryProduct X Y = CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)

@[reducible, inline]

abbrev CategoryTheory.Limits.HasBinaryCoproduct {C : Type u} [Category.{v, u} C] (X Y : C) : Prop

An abbreviation for HasColimit (pair X Y).

Equations

• CategoryTheory.Limits.HasBinaryCoproduct X Y = CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair X Y)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.prod {C : Type u} [Category.{v, u} C] (X Y : C) [HasBinaryProduct X Y] : C

If we have a product of X and Y, we can access it using prod X Y or X ⨯ Y.

Equations

• (X ⨯ Y) = CategoryTheory.Limits.limit (CategoryTheory.Limits.pair X Y)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coprod {C : Type u} [Category.{v, u} C] (X Y : C) [HasBinaryCoproduct X Y] : C

If we have a coproduct of X and Y, we can access it using coprod X Y or X ⨿ Y.

Equations

• (X ⨿ Y) = CategoryTheory.Limits.colimit (CategoryTheory.Limits.pair X Y)

def CategoryTheory.Limits.«term_⨯_» : Lean.TrailingParserDescr

Notation for the product

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.«term_⨿_» : Lean.TrailingParserDescr

Notation for the coproduct

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.prod.fst {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] : X ⨯ Y ⟶ X

The projection map to the first component of the product.

Equations

• CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left }

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coprod.inl {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] : X ⟶ X ⨿ Y

The inclusion map from the first component of the coproduct.

Equations

• CategoryTheory.Limits.coprod.inl = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left }

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.prod.snd {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] : X ⨯ Y ⟶ Y

The projection map to the second component of the product.

Equations

• CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right }

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coprod.inr {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] : Y ⟶ X ⨿ Y

The inclusion map from the second component of the coproduct.

Equations

• CategoryTheory.Limits.coprod.inr = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right }

noncomputable def CategoryTheory.Limits.prodIsProd {C : Type u} [Category.{v, u} C] (X Y : C) [HasBinaryProduct X Y] : IsLimit (BinaryFan.mk prod.fst prod.snd)

The binary fan constructed from the projection maps is a limit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.coprodIsCoprod {C : Type u} [Category.{v, u} C] (X Y : C) [HasBinaryCoproduct X Y] : IsColimit (BinaryCofan.mk coprod.inl coprod.inr)

The binary cofan constructed from the coprojection maps is a colimit.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.prod.hom_ext {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y} (h₁ : CategoryStruct.comp f fst = CategoryStruct.comp g fst) (h₂ : CategoryStruct.comp f snd = CategoryStruct.comp g snd) : f = g

theorem CategoryTheory.Limits.coprod.hom_ext {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W} (h₁ : CategoryStruct.comp inl f = CategoryStruct.comp inl g) (h₂ : CategoryStruct.comp inr f = CategoryStruct.comp inr g) : f = g

theorem CategoryTheory.Limits.prod.hom_ext_iff {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y} : f = g ↔ CategoryStruct.comp f fst = CategoryStruct.comp g fst ∧ CategoryStruct.comp f snd = CategoryStruct.comp g snd

theorem CategoryTheory.Limits.coprod.hom_ext_iff {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W} : f = g ↔ CategoryStruct.comp inl f = CategoryStruct.comp inl g ∧ CategoryStruct.comp inr f = CategoryStruct.comp inr g

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.prod.lift {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : W ⟶ X ⨯ Y

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.

Equations

• CategoryTheory.Limits.prod.lift f g = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.pair X Y) (CategoryTheory.Limits.BinaryFan.mk f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.coprod.desc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : X ⨿ Y ⟶ W

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.

Equations

• CategoryTheory.Limits.coprod.desc f g = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.pair X Y) (CategoryTheory.Limits.BinaryCofan.mk f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.diag {C : Type u} [Category.{v, u} C] (X : C) [HasBinaryProduct X X] : X ⟶ X ⨯ X

diagonal arrow of the binary product in the category fam I

Equations

• CategoryTheory.Limits.diag X = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.codiag {C : Type u} [Category.{v, u} C] (X : C) [HasBinaryCoproduct X X] : X ⨿ X ⟶ X

codiagonal arrow of the binary coproduct

Equations

• CategoryTheory.Limits.codiag X = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)

theorem CategoryTheory.Limits.prod.lift_fst {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : CategoryStruct.comp (lift f g) fst = f

theorem CategoryTheory.Limits.coprod.inl_desc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : CategoryStruct.comp inl (desc f g) = f

theorem CategoryTheory.Limits.prod.lift_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp fst h) = CategoryStruct.comp f h

theorem CategoryTheory.Limits.coprod.inl_desc_assoc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z) : CategoryStruct.comp inl (CategoryStruct.comp (desc f g) h) = CategoryStruct.comp f h

theorem CategoryTheory.Limits.prod.lift_snd {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : CategoryStruct.comp (lift f g) snd = g

theorem CategoryTheory.Limits.coprod.inr_desc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : CategoryStruct.comp inr (desc f g) = g

theorem CategoryTheory.Limits.coprod.inr_desc_assoc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z) : CategoryStruct.comp inr (CategoryStruct.comp (desc f g) h) = CategoryStruct.comp g h

theorem CategoryTheory.Limits.prod.lift_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (lift f g) (CategoryStruct.comp snd h) = CategoryStruct.comp g h

instance CategoryTheory.Limits.prod.mono_lift_of_mono_left {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono f] : Mono (lift f g)

instance CategoryTheory.Limits.coprod.epi_desc_of_epi_left {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi f] : Epi (desc f g)

instance CategoryTheory.Limits.prod.mono_lift_of_mono_right {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [Mono g] : Mono (lift f g)

instance CategoryTheory.Limits.coprod.epi_desc_of_epi_right {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [Epi g] : Epi (desc f g)

noncomputable def CategoryTheory.Limits.prod.lift' {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : { l : W ⟶ X ⨯ Y // CategoryStruct.comp l fst = f ∧ CategoryStruct.comp l snd = g }

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

• CategoryTheory.Limits.prod.lift' f g = ⟨CategoryTheory.Limits.prod.lift f g, ⋯⟩

noncomputable def CategoryTheory.Limits.coprod.desc' {C : Type u} [Category.{v, u} C] {W X Y : C} [HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : { l : X ⨿ Y ⟶ W // CategoryStruct.comp inl l = f ∧ CategoryStruct.comp inr l = g }

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

• CategoryTheory.Limits.coprod.desc' f g = ⟨CategoryTheory.Limits.coprod.desc f g, ⋯⟩

noncomputable def CategoryTheory.Limits.prod.map {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : W ⨯ X ⟶ Y ⨯ Z

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.

Equations

• CategoryTheory.Limits.prod.map f g = CategoryTheory.Limits.limMap (CategoryTheory.Limits.mapPair f g)

noncomputable def CategoryTheory.Limits.coprod.map {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : Y ⟶ W) (g : Z ⟶ X) : Y ⨿ Z ⟶ W ⨿ X

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.

Equations

• CategoryTheory.Limits.coprod.map f g = CategoryTheory.Limits.colimMap (CategoryTheory.Limits.mapPair f g)

@[simp]

theorem CategoryTheory.Limits.prod.comp_lift {C : Type u} [Category.{v, u} C] {V W X Y : C} [HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) : CategoryStruct.comp f (lift g h) = lift (CategoryStruct.comp f g) (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Limits.coprod.desc_comp {C : Type u} [Category.{v, u} C] {V W X Y : C} [HasBinaryCoproduct X Y] (f : W ⟶ V) (g : X ⟶ W) (h : Y ⟶ W) : CategoryStruct.comp (desc g h) f = desc (CategoryStruct.comp g f) (CategoryStruct.comp h f)

theorem CategoryTheory.Limits.prod.comp_lift_assoc {C : Type u} [Category.{v, u} C] {V W X Y : C} [HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) {Z : C} (h✝ : X ⨯ Y ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (lift g h) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f g) (CategoryStruct.comp f h)) h✝

theorem CategoryTheory.Limits.coprod.desc_comp_assoc {C : Type u} [Category.{v, u} C] {V W X Y : C} [HasBinaryCoproduct X Y] (f : W ⟶ V) (g : X ⟶ W) (h : Y ⟶ W) {Z : C} (h✝ : V ⟶ Z) : CategoryStruct.comp (desc g h) (CategoryStruct.comp f h✝) = CategoryStruct.comp (desc (CategoryStruct.comp g f) (CategoryStruct.comp h f)) h✝

theorem CategoryTheory.Limits.prod.comp_diag {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct Y Y] (f : X ⟶ Y) : CategoryStruct.comp f (diag Y) = lift f f

theorem CategoryTheory.Limits.coprod.codiag_comp {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct Y Y] (f : Y ⟶ X) : CategoryStruct.comp (codiag Y) f = desc f f

@[deprecated CategoryTheory.Limits.coprod.codiag_comp (since := "2026-09-26")]

theorem CategoryTheory.Limits.coprod.diag_comp {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct Y Y] (f : Y ⟶ X) : CategoryStruct.comp (codiag Y) f = desc f f

Alias of CategoryTheory.Limits.coprod.codiag_comp.

@[simp]

theorem CategoryTheory.Limits.prod.map_fst {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (map f g) fst = CategoryStruct.comp fst f

@[simp]

theorem CategoryTheory.Limits.coprod.inl_map {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : Y ⟶ W) (g : Z ⟶ X) : CategoryStruct.comp inl (map f g) = CategoryStruct.comp f inl

@[simp]

theorem CategoryTheory.Limits.coprod.inl_map_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : Y ⟶ W) (g : Z ⟶ X) {Z✝ : C} (h : W ⨿ X ⟶ Z✝) : CategoryStruct.comp inl (CategoryStruct.comp (map f g) h) = CategoryStruct.comp f (CategoryStruct.comp inl h)

@[simp]

theorem CategoryTheory.Limits.prod.map_fst_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (map f g) (CategoryStruct.comp fst h) = CategoryStruct.comp fst (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Limits.prod.map_snd {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) : CategoryStruct.comp (map f g) snd = CategoryStruct.comp snd g

@[simp]

theorem CategoryTheory.Limits.coprod.inr_map {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : Y ⟶ W) (g : Z ⟶ X) : CategoryStruct.comp inr (map f g) = CategoryStruct.comp g inr

@[simp]

theorem CategoryTheory.Limits.coprod.inr_map_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : Y ⟶ W) (g : Z ⟶ X) {Z✝ : C} (h : W ⨿ X ⟶ Z✝) : CategoryStruct.comp inr (CategoryStruct.comp (map f g) h) = CategoryStruct.comp g (CategoryStruct.comp inr h)

@[simp]

theorem CategoryTheory.Limits.prod.map_snd_assoc {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (map f g) (CategoryStruct.comp snd h) = CategoryStruct.comp snd (CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.Limits.prod.map_id_id {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] : map (CategoryStruct.id X) (CategoryStruct.id Y) = CategoryStruct.id (X ⨯ Y)

@[simp]

theorem CategoryTheory.Limits.coprod.map_id_id {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] : map (CategoryStruct.id X) (CategoryStruct.id Y) = CategoryStruct.id (X ⨿ Y)

@[simp]

theorem CategoryTheory.Limits.prod.lift_fst_snd {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] : lift fst snd = CategoryStruct.id (X ⨯ Y)

@[simp]

theorem CategoryTheory.Limits.coprod.desc_inl_inr {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] : desc inl inr = CategoryStruct.id (X ⨿ Y)

@[simp]

theorem CategoryTheory.Limits.prod.lift_map {C : Type u} [Category.{v, u} C] {V W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) : CategoryStruct.comp (lift f g) (map h k) = lift (CategoryStruct.comp f h) (CategoryStruct.comp g k)

@[simp]

theorem CategoryTheory.Limits.coprod.map_desc {C : Type u} [Category.{v, u} C] {V W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ V) (g : X ⟶ V) (h : Y ⟶ W) (k : Z ⟶ X) : CategoryStruct.comp (map h k) (desc f g) = desc (CategoryStruct.comp h f) (CategoryStruct.comp k g)

@[simp]

theorem CategoryTheory.Limits.prod.lift_map_assoc {C : Type u} [Category.{v, u} C] {V W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) {Z✝ : C} (h✝ : Y ⨯ Z ⟶ Z✝) : CategoryStruct.comp (lift f g) (CategoryStruct.comp (map h k) h✝) = CategoryStruct.comp (lift (CategoryStruct.comp f h) (CategoryStruct.comp g k)) h✝

theorem CategoryTheory.Limits.coprod.map_desc_assoc {C : Type u} [Category.{v, u} C] {V W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ⟶ V) (g : X ⟶ V) (h : Y ⟶ W) (k : Z ⟶ X) {Z✝ : C} (h✝ : V ⟶ Z✝) : CategoryStruct.comp (map h k) (CategoryStruct.comp (desc f g) h✝) = CategoryStruct.comp (desc (CategoryStruct.comp h f) (CategoryStruct.comp k g)) h✝

@[simp]

theorem CategoryTheory.Limits.prod.lift_fst_comp_snd_comp {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W Y] [HasBinaryProduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) : lift (CategoryStruct.comp fst g) (CategoryStruct.comp snd g') = map g g'

@[simp]

theorem CategoryTheory.Limits.coprod.desc_comp_inl_comp_inr {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W Y] [HasBinaryCoproduct X Z] (g : X ⟶ W) (g' : Z ⟶ Y) : desc (CategoryStruct.comp g inl) (CategoryStruct.comp g' inr) = map g g'

@[simp]

theorem CategoryTheory.Limits.prod.map_map {C : Type u} [Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryProduct A₁ B₁] [HasBinaryProduct A₂ B₂] [HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) : CategoryStruct.comp (map f g) (map h k) = map (CategoryStruct.comp f h) (CategoryStruct.comp g k)

@[simp]

theorem CategoryTheory.Limits.coprod.map_map {C : Type u} [Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryCoproduct A₁ B₁] [HasBinaryCoproduct A₂ B₂] [HasBinaryCoproduct A₃ B₃] (h : A₃ ⟶ A₂) (k : B₃ ⟶ B₂) (f : A₂ ⟶ A₁) (g : B₂ ⟶ B₁) : CategoryStruct.comp (map h k) (map f g) = map (CategoryStruct.comp h f) (CategoryStruct.comp k g)

@[simp]

theorem CategoryTheory.Limits.coprod.map_map_assoc {C : Type u} [Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryCoproduct A₁ B₁] [HasBinaryCoproduct A₂ B₂] [HasBinaryCoproduct A₃ B₃] (h : A₃ ⟶ A₂) (k : B₃ ⟶ B₂) (f : A₂ ⟶ A₁) (g : B₂ ⟶ B₁) {Z : C} (h✝ : A₁ ⨿ B₁ ⟶ Z) : CategoryStruct.comp (map h k) (CategoryStruct.comp (map f g) h✝) = CategoryStruct.comp (map (CategoryStruct.comp h f) (CategoryStruct.comp k g)) h✝

@[simp]

theorem CategoryTheory.Limits.prod.map_map_assoc {C : Type u} [Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryProduct A₁ B₁] [HasBinaryProduct A₂ B₂] [HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) {Z : C} (h✝ : A₃ ⨯ B₃ ⟶ Z) : CategoryStruct.comp (map f g) (CategoryStruct.comp (map h k) h✝) = CategoryStruct.comp (map (CategoryStruct.comp f h) (CategoryStruct.comp g k)) h✝

theorem CategoryTheory.Limits.prod.map_swap {C : Type u} [Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasLimitsOfShape (Discrete WalkingPair) C] : CategoryStruct.comp (map (CategoryStruct.id X) f) (map g (CategoryStruct.id B)) = CategoryStruct.comp (map g (CategoryStruct.id A)) (map (CategoryStruct.id Y) f)

theorem CategoryTheory.Limits.coprod.map_swap {C : Type u} [Category.{v, u} C] {A B X Y : C} (f : B ⟶ A) (g : Y ⟶ X) [HasColimitsOfShape (Discrete WalkingPair) C] : CategoryStruct.comp (map g (CategoryStruct.id B)) (map (CategoryStruct.id X) f) = CategoryStruct.comp (map (CategoryStruct.id Y) f) (map g (CategoryStruct.id A))

theorem CategoryTheory.Limits.coprod.map_swap_assoc {C : Type u} [Category.{v, u} C] {A B X Y : C} (f : B ⟶ A) (g : Y ⟶ X) [HasColimitsOfShape (Discrete WalkingPair) C] {Z : C} (h : X ⨿ A ⟶ Z) : CategoryStruct.comp (map g (CategoryStruct.id B)) (CategoryStruct.comp (map (CategoryStruct.id X) f) h) = CategoryStruct.comp (map (CategoryStruct.id Y) f) (CategoryStruct.comp (map g (CategoryStruct.id A)) h)

theorem CategoryTheory.Limits.prod.map_swap_assoc {C : Type u} [Category.{v, u} C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [HasLimitsOfShape (Discrete WalkingPair) C] {Z : C} (h : Y ⨯ B ⟶ Z) : CategoryStruct.comp (map (CategoryStruct.id X) f) (CategoryStruct.comp (map g (CategoryStruct.id B)) h) = CategoryStruct.comp (map g (CategoryStruct.id A)) (CategoryStruct.comp (map (CategoryStruct.id Y) f) h)

theorem CategoryTheory.Limits.prod.map_comp_id {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct X W] [HasBinaryProduct Z W] [HasBinaryProduct Y W] : map (CategoryStruct.comp f g) (CategoryStruct.id W) = CategoryStruct.comp (map f (CategoryStruct.id W)) (map g (CategoryStruct.id W))

theorem CategoryTheory.Limits.coprod.map_comp_id {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : Y ⟶ X) (g : Z ⟶ Y) [HasBinaryCoproduct X W] [HasBinaryCoproduct Z W] [HasBinaryCoproduct Y W] : map (CategoryStruct.comp g f) (CategoryStruct.id W) = CategoryStruct.comp (map g (CategoryStruct.id W)) (map f (CategoryStruct.id W))

theorem CategoryTheory.Limits.coprod.map_comp_id_assoc {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : Y ⟶ X) (g : Z ⟶ Y) [HasBinaryCoproduct X W] [HasBinaryCoproduct Z W] [HasBinaryCoproduct Y W] {Z✝ : C} (h : X ⨿ W ⟶ Z✝) : CategoryStruct.comp (map (CategoryStruct.comp g f) (CategoryStruct.id W)) h = CategoryStruct.comp (map g (CategoryStruct.id W)) (CategoryStruct.comp (map f (CategoryStruct.id W)) h)

theorem CategoryTheory.Limits.prod.map_comp_id_assoc {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct X W] [HasBinaryProduct Z W] [HasBinaryProduct Y W] {Z✝ : C} (h : Z ⨯ W ⟶ Z✝) : CategoryStruct.comp (map (CategoryStruct.comp f g) (CategoryStruct.id W)) h = CategoryStruct.comp (map f (CategoryStruct.id W)) (CategoryStruct.comp (map g (CategoryStruct.id W)) h)

theorem CategoryTheory.Limits.prod.map_id_comp {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct W X] [HasBinaryProduct W Y] [HasBinaryProduct W Z] : map (CategoryStruct.id W) (CategoryStruct.comp f g) = CategoryStruct.comp (map (CategoryStruct.id W) f) (map (CategoryStruct.id W) g)

theorem CategoryTheory.Limits.coprod.map_id_comp {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : Y ⟶ X) (g : Z ⟶ Y) [HasBinaryCoproduct W X] [HasBinaryCoproduct W Y] [HasBinaryCoproduct W Z] : map (CategoryStruct.id W) (CategoryStruct.comp g f) = CategoryStruct.comp (map (CategoryStruct.id W) g) (map (CategoryStruct.id W) f)

theorem CategoryTheory.Limits.prod.map_id_comp_assoc {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasBinaryProduct W X] [HasBinaryProduct W Y] [HasBinaryProduct W Z] {Z✝ : C} (h : W ⨯ Z ⟶ Z✝) : CategoryStruct.comp (map (CategoryStruct.id W) (CategoryStruct.comp f g)) h = CategoryStruct.comp (map (CategoryStruct.id W) f) (CategoryStruct.comp (map (CategoryStruct.id W) g) h)

theorem CategoryTheory.Limits.coprod.map_id_comp_assoc {C : Type u} [Category.{v, u} C] {X Y Z W : C} (f : Y ⟶ X) (g : Z ⟶ Y) [HasBinaryCoproduct W X] [HasBinaryCoproduct W Y] [HasBinaryCoproduct W Z] {Z✝ : C} (h : W ⨿ X ⟶ Z✝) : CategoryStruct.comp (map (CategoryStruct.id W) (CategoryStruct.comp g f)) h = CategoryStruct.comp (map (CategoryStruct.id W) g) (CategoryStruct.comp (map (CategoryStruct.id W) f) h)

noncomputable def CategoryTheory.Limits.prod.mapIso {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : 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.mapIso f g : W ⨯ X ≅ Y ⨯ Z.

Equations

• CategoryTheory.Limits.prod.mapIso f g = { hom := CategoryTheory.Limits.prod.map f.hom g.hom, inv := CategoryTheory.Limits.prod.map f.inv g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

noncomputable def CategoryTheory.Limits.coprod.mapIso {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : W ⨿ X ≅ Y ⨿ Z

If the coproducts W ⨿ X and Y ⨿ Z exist, then every pair of isomorphisms f : W ≅ Y and g : W ≅ Z induces an isomorphism coprod.mapIso f g : W ⨿ X ≅ Y ⨿ Z.

Equations

• CategoryTheory.Limits.coprod.mapIso f g = { hom := CategoryTheory.Limits.coprod.map f.hom g.hom, inv := CategoryTheory.Limits.coprod.map f.inv g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Limits.coprod.mapIso_inv {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).inv = map f.inv g.inv

@[simp]

theorem CategoryTheory.Limits.prod.mapIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).hom = map f.hom g.hom

@[simp]

theorem CategoryTheory.Limits.coprod.mapIso_hom {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).hom = map f.hom g.hom

@[simp]

theorem CategoryTheory.Limits.prod.mapIso_inv {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ≅ Y) (g : X ≅ Z) : (mapIso f g).inv = map f.inv g.inv

instance CategoryTheory.Limits.isIso_prod {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [IsIso f] [IsIso g] : IsIso (prod.map f g)

instance CategoryTheory.Limits.isIso_coprod {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : Y ⟶ W) (g : Z ⟶ X) [IsIso f] [IsIso g] : IsIso (coprod.map f g)

instance CategoryTheory.Limits.prod.map_mono {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f] [Mono g] [HasBinaryProduct W X] [HasBinaryProduct Y Z] : Mono (map f g)

instance CategoryTheory.Limits.coprod.map_epi {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} (f : Y ⟶ W) (g : Z ⟶ X) [Epi f] [Epi g] [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] : Epi (map f g)

theorem CategoryTheory.Limits.prod.diag_map {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasBinaryProduct X X] [HasBinaryProduct Y Y] : CategoryStruct.comp (diag X) (map f f) = CategoryStruct.comp f (diag Y)

theorem CategoryTheory.Limits.coprod.map_codiag {C : Type u} [Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [HasBinaryCoproduct X X] [HasBinaryCoproduct Y Y] : CategoryStruct.comp (map f f) (codiag X) = CategoryStruct.comp (codiag Y) f

theorem CategoryTheory.Limits.coprod.map_codiag_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [HasBinaryCoproduct X X] [HasBinaryCoproduct Y Y] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (map f f) (CategoryStruct.comp (codiag X) h) = CategoryStruct.comp (codiag Y) (CategoryStruct.comp f h)

theorem CategoryTheory.Limits.prod.diag_map_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [HasBinaryProduct X X] [HasBinaryProduct Y Y] {Z : C} (h : Y ⨯ Y ⟶ Z) : CategoryStruct.comp (diag X) (CategoryStruct.comp (map f f) h) = CategoryStruct.comp f (CategoryStruct.comp (diag Y) h)

theorem CategoryTheory.Limits.prod.diag_map_fst_snd {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] [HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] : CategoryStruct.comp (diag (X ⨯ Y)) (map fst snd) = CategoryStruct.id (X ⨯ Y)

theorem CategoryTheory.Limits.coprod.map_inl_inr_codiag {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] [HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] : CategoryStruct.comp (map inl inr) (codiag (X ⨿ Y)) = CategoryStruct.id (X ⨿ Y)

theorem CategoryTheory.Limits.coprod.map_inl_inr_codiag_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryCoproduct X Y] [HasBinaryCoproduct (X ⨿ Y) (X ⨿ Y)] {Z : C} (h : X ⨿ Y ⟶ Z) : CategoryStruct.comp (map inl inr) (CategoryStruct.comp (codiag (X ⨿ Y)) h) = h

theorem CategoryTheory.Limits.prod.diag_map_fst_snd_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasBinaryProduct X Y] [HasBinaryProduct (X ⨯ Y) (X ⨯ Y)] {Z : C} (h : X ⨯ Y ⟶ Z) : CategoryStruct.comp (diag (X ⨯ Y)) (CategoryStruct.comp (map fst snd) h) = h

theorem CategoryTheory.Limits.prod.diag_map_fst_snd_comp {C : Type u} [Category.{v, u} C] [HasLimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') : CategoryStruct.comp (diag (X ⨯ X')) (map (CategoryStruct.comp fst g) (CategoryStruct.comp snd g')) = map g g'

theorem CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag {C : Type u} [Category.{v, u} C] [HasColimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : Y ⟶ X) (g' : Y' ⟶ X') : CategoryStruct.comp (map (CategoryStruct.comp g inl) (CategoryStruct.comp g' inr)) (codiag (X ⨿ X')) = map g g'

theorem CategoryTheory.Limits.prod.diag_map_fst_snd_comp_assoc {C : Type u} [Category.{v, u} C] [HasLimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') {Z : C} (h : Y ⨯ Y' ⟶ Z) : CategoryStruct.comp (diag (X ⨯ X')) (CategoryStruct.comp (map (CategoryStruct.comp fst g) (CategoryStruct.comp snd g')) h) = CategoryStruct.comp (map g g') h

theorem CategoryTheory.Limits.coprod.map_comp_inl_inr_codiag_assoc {C : Type u} [Category.{v, u} C] [HasColimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C} (g : Y ⟶ X) (g' : Y' ⟶ X') {Z : C} (h : X ⨿ X' ⟶ Z) : CategoryStruct.comp (map (CategoryStruct.comp g inl) (CategoryStruct.comp g' inr)) (CategoryStruct.comp (codiag (X ⨿ X')) h) = CategoryStruct.comp (map g g') h

instance CategoryTheory.Limits.instIsSplitMonoDiag {C : Type u} [Category.{v, u} C] {X : C} [HasBinaryProduct X X] : IsSplitMono (diag X)

instance CategoryTheory.Limits.instIsSplitEpiCodiag {C : Type u} [Category.{v, u} C] {X : C} [HasBinaryCoproduct X X] : IsSplitEpi (codiag X)

@[reducible, inline]

abbrev CategoryTheory.Limits.HasBinaryProducts (C : Type u) [Category.{v, u} C] : Prop

A category HasBinaryProducts if it has all limits of shape Discrete WalkingPair, i.e. if it has a product for every pair of objects.

Equations

• CategoryTheory.Limits.HasBinaryProducts C = CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C

@[reducible, inline]

abbrev CategoryTheory.Limits.HasBinaryCoproducts (C : Type u) [Category.{v, u} C] : Prop

A category HasBinaryCoproducts if it has all colimit of shape Discrete WalkingPair, i.e. if it has a coproduct for every pair of objects.

Equations

• CategoryTheory.Limits.HasBinaryCoproducts C = CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C

theorem CategoryTheory.Limits.hasBinaryProducts_of_hasLimit_pair (C : Type u) [Category.{v, u} C] [∀ {X Y : C}, HasLimit (pair X Y)] : HasBinaryProducts C

If C has all limits of diagrams pair X Y, then it has all binary products

theorem CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair (C : Type u) [Category.{v, u} C] [∀ {X Y : C}, HasColimit (pair X Y)] : HasBinaryCoproducts C

If C has all colimits of diagrams pair X Y, then it has all binary coproducts

noncomputable def CategoryTheory.Limits.prod.braiding {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : P ⨯ Q ≅ Q ⨯ P

The braiding isomorphism which swaps a binary product.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.coprod.braiding {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryCoproduct P Q] [HasBinaryCoproduct Q P] : P ⨿ Q ≅ Q ⨿ P

The braiding isomorphism which swaps a binary coproduct.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.coprod.braiding_inv {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryCoproduct P Q] [HasBinaryCoproduct Q P] : (braiding P Q).inv = desc inr inl

@[simp]

theorem CategoryTheory.Limits.coprod.braiding_hom {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryCoproduct P Q] [HasBinaryCoproduct Q P] : (braiding P Q).hom = desc inr inl

@[simp]

theorem CategoryTheory.Limits.prod.braiding_inv {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : (braiding P Q).inv = lift snd fst

@[simp]

theorem CategoryTheory.Limits.prod.braiding_hom {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : (braiding P Q).hom = lift snd fst

theorem CategoryTheory.Limits.braid_natural {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) : CategoryStruct.comp (prod.map f g) (prod.braiding Y W).hom = CategoryStruct.comp (prod.braiding X Z).hom (prod.map g f)

The braiding isomorphism can be passed through a map by swapping the order.

theorem CategoryTheory.Limits.braid_natural_assoc {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z✝ : C} (h : W ⨯ Y ⟶ Z✝) : CategoryStruct.comp (prod.map f g) (CategoryStruct.comp (prod.braiding Y W).hom h) = CategoryStruct.comp (prod.braiding X Z).hom (CategoryStruct.comp (prod.map g f) h)

The braiding isomorphism can be passed through a map by swapping the order.

theorem CategoryTheory.Limits.prod.symmetry' {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : CategoryStruct.comp (lift snd fst) (lift snd fst) = CategoryStruct.id (P ⨯ Q)

theorem CategoryTheory.Limits.coprod.symmetry' {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryCoproduct P Q] [HasBinaryCoproduct Q P] : CategoryStruct.comp (desc inr inl) (desc inr inl) = CategoryStruct.id (P ⨿ Q)

theorem CategoryTheory.Limits.prod.symmetry'_assoc {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] {Z : C} (h : P ⨯ Q ⟶ Z) : CategoryStruct.comp (lift snd fst) (CategoryStruct.comp (lift snd fst) h) = h

theorem CategoryTheory.Limits.coprod.symmetry'_assoc {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryCoproduct P Q] [HasBinaryCoproduct Q P] {Z : C} (h : P ⨿ Q ⟶ Z) : CategoryStruct.comp (desc inr inl) (CategoryStruct.comp (desc inr inl) h) = h

theorem CategoryTheory.Limits.prod.symmetry {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] : CategoryStruct.comp (braiding P Q).hom (braiding Q P).hom = CategoryStruct.id (P ⨯ Q)

The braiding isomorphism is symmetric.

theorem CategoryTheory.Limits.coprod.symmetry {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryCoproduct P Q] [HasBinaryCoproduct Q P] : CategoryStruct.comp (braiding Q P).inv (braiding P Q).inv = CategoryStruct.id (P ⨿ Q)

The braiding isomorphism is symmetric.

theorem CategoryTheory.Limits.coprod.symmetry_assoc {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryCoproduct P Q] [HasBinaryCoproduct Q P] {Z : C} (h : P ⨿ Q ⟶ Z) : CategoryStruct.comp (braiding Q P).inv (CategoryStruct.comp (braiding P Q).inv h) = h

The braiding isomorphism is symmetric.

theorem CategoryTheory.Limits.prod.symmetry_assoc {C : Type u} [Category.{v, u} C] (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] {Z : C} (h : P ⨯ Q ⟶ Z) : CategoryStruct.comp (braiding P Q).hom (CategoryStruct.comp (braiding Q P).hom h) = h

The braiding isomorphism is symmetric.

noncomputable def CategoryTheory.Limits.prod.associator {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (P Q R : C) : (P ⨯ Q) ⨯ R ≅ P ⨯ Q ⨯ R

The associator isomorphism for binary products.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.coprod.associator {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q R : C) : (P ⨿ Q) ⨿ R ≅ P ⨿ Q ⨿ R

The associator isomorphism for binary coproducts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.coprod.associator_inv {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q R : C) : (associator P Q R).inv = desc (CategoryStruct.comp inl inl) (desc (CategoryStruct.comp inr inl) inr)

@[simp]

theorem CategoryTheory.Limits.prod.associator_inv {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (P Q R : C) : (associator P Q R).inv = lift (lift fst (CategoryStruct.comp snd fst)) (CategoryStruct.comp snd snd)

@[simp]

theorem CategoryTheory.Limits.coprod.associator_hom {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (P Q R : C) : (associator P Q R).hom = desc (desc inl (CategoryStruct.comp inl inr)) (CategoryStruct.comp inr inr)

@[simp]

theorem CategoryTheory.Limits.prod.associator_hom {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (P Q R : C) : (associator P Q R).hom = lift (CategoryStruct.comp fst fst) (lift (CategoryStruct.comp fst snd) snd)

theorem CategoryTheory.Limits.prod.pentagon {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (W X Y Z : C) : CategoryStruct.comp (map (associator W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (associator W (X ⨯ Y) Z).hom (map (CategoryStruct.id W) (associator X Y Z).hom)) = CategoryStruct.comp (associator (W ⨯ X) Y Z).hom (associator W X (Y ⨯ Z)).hom

theorem CategoryTheory.Limits.prod.pentagon_assoc {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (W X Y Z : C) {Z✝ : C} (h : W ⨯ X ⨯ Y ⨯ Z ⟶ Z✝) : CategoryStruct.comp (map (associator W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (associator W (X ⨯ Y) Z).hom (CategoryStruct.comp (map (CategoryStruct.id W) (associator X Y Z).hom) h)) = CategoryStruct.comp (associator (W ⨯ X) Y Z).hom (CategoryStruct.comp (associator W X (Y ⨯ Z)).hom h)

theorem CategoryTheory.Limits.prod.associator_naturality {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (map (map f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (map f₁ (map f₂ f₃))

theorem CategoryTheory.Limits.prod.associator_naturality_assoc {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {Z : C} (h : Y₁ ⨯ Y₂ ⨯ Y₃ ⟶ Z) : CategoryStruct.comp (map (map f₁ f₂) f₃) (CategoryStruct.comp (associator Y₁ Y₂ Y₃).hom h) = CategoryStruct.comp (associator X₁ X₂ X₃).hom (CategoryStruct.comp (map f₁ (map f₂ f₃)) h)

noncomputable def CategoryTheory.Limits.prod.leftUnitor {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct (⊤_ C) P] : (⊤_ C) ⨯ P ≅ P

The left unitor isomorphism for binary products with the terminal object.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.coprod.leftUnitor {C : Type u} [Category.{v, u} C] [HasInitial C] (P : C) [HasBinaryCoproduct (⊥_ C) P] : (⊥_ C) ⨿ P ≅ P

The left unitor isomorphism for binary coproducts with the initial object.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.coprod.leftUnitor_inv {C : Type u} [Category.{v, u} C] [HasInitial C] (P : C) [HasBinaryCoproduct (⊥_ C) P] : (leftUnitor P).inv = inr

@[simp]

theorem CategoryTheory.Limits.prod.leftUnitor_hom {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct (⊤_ C) P] : (leftUnitor P).hom = snd

@[simp]

theorem CategoryTheory.Limits.coprod.leftUnitor_hom {C : Type u} [Category.{v, u} C] [HasInitial C] (P : C) [HasBinaryCoproduct (⊥_ C) P] : (leftUnitor P).hom = desc (initial.to P) (CategoryStruct.id P)

@[simp]

theorem CategoryTheory.Limits.prod.leftUnitor_inv {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct (⊤_ C) P] : (leftUnitor P).inv = lift (terminal.from P) (CategoryStruct.id P)

noncomputable def CategoryTheory.Limits.prod.rightUnitor {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct P (⊤_ C)] : P ⨯ ⊤_ C ≅ P

The right unitor isomorphism for binary products with the terminal object.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.coprod.rightUnitor {C : Type u} [Category.{v, u} C] [HasInitial C] (P : C) [HasBinaryCoproduct P (⊥_ C)] : P ⨿ ⊥_ C ≅ P

The right unitor isomorphism for binary coproducts with the initial object.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.prod.rightUnitor_hom {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct P (⊤_ C)] : (rightUnitor P).hom = fst

@[simp]

theorem CategoryTheory.Limits.coprod.rightUnitor_inv {C : Type u} [Category.{v, u} C] [HasInitial C] (P : C) [HasBinaryCoproduct P (⊥_ C)] : (rightUnitor P).inv = inl

@[simp]

theorem CategoryTheory.Limits.coprod.rightUnitor_hom {C : Type u} [Category.{v, u} C] [HasInitial C] (P : C) [HasBinaryCoproduct P (⊥_ C)] : (rightUnitor P).hom = desc (CategoryStruct.id P) (initial.to P)

@[simp]

theorem CategoryTheory.Limits.prod.rightUnitor_inv {C : Type u} [Category.{v, u} C] [HasTerminal C] (P : C) [HasBinaryProduct P (⊤_ C)] : (rightUnitor P).inv = lift (CategoryStruct.id P) (terminal.from P)

theorem CategoryTheory.Limits.prod.leftUnitor_hom_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) : CategoryStruct.comp (map (CategoryStruct.id (⊤_ C)) f) (leftUnitor Y).hom = CategoryStruct.comp (leftUnitor X).hom f

theorem CategoryTheory.Limits.coprod.leftUnitor_inv_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) : CategoryStruct.comp (leftUnitor Y).inv (map (CategoryStruct.id (⊥_ C)) f) = CategoryStruct.comp f (leftUnitor X).inv

theorem CategoryTheory.Limits.prod.leftUnitor_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (map (CategoryStruct.id (⊤_ C)) f) (CategoryStruct.comp (leftUnitor Y).hom h) = CategoryStruct.comp (leftUnitor X).hom (CategoryStruct.comp f h)

theorem CategoryTheory.Limits.coprod.leftUnitor_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) {Z : C} (h : (⊥_ C) ⨿ X ⟶ Z) : CategoryStruct.comp (leftUnitor Y).inv (CategoryStruct.comp (map (CategoryStruct.id (⊥_ C)) f) h) = CategoryStruct.comp f (CategoryStruct.comp (leftUnitor X).inv h)

theorem CategoryTheory.Limits.prod.leftUnitor_inv_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) : CategoryStruct.comp (leftUnitor X).inv (map (CategoryStruct.id (⊤_ C)) f) = CategoryStruct.comp f (leftUnitor Y).inv

theorem CategoryTheory.Limits.coprod.leftUnitor_hom_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) : CategoryStruct.comp (map (CategoryStruct.id (⊥_ C)) f) (leftUnitor X).hom = CategoryStruct.comp (leftUnitor Y).hom f

theorem CategoryTheory.Limits.prod.leftUnitor_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : (⊤_ C) ⨯ Y ⟶ Z) : CategoryStruct.comp (leftUnitor X).inv (CategoryStruct.comp (map (CategoryStruct.id (⊤_ C)) f) h) = CategoryStruct.comp f (CategoryStruct.comp (leftUnitor Y).inv h)

theorem CategoryTheory.Limits.coprod.leftUnitor_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (map (CategoryStruct.id (⊥_ C)) f) (CategoryStruct.comp (leftUnitor X).hom h) = CategoryStruct.comp (leftUnitor Y).hom (CategoryStruct.comp f h)

@[deprecated CategoryTheory.Limits.coprod.leftUnitor_hom_naturality (since := "2026-09-26")]

theorem CategoryTheory.Limits.coprod.leftUnitor_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) : CategoryStruct.comp (map (CategoryStruct.id (⊥_ C)) f) (leftUnitor X).hom = CategoryStruct.comp (leftUnitor Y).hom f

Alias of CategoryTheory.Limits.coprod.leftUnitor_hom_naturality.

theorem CategoryTheory.Limits.prod.rightUnitor_hom_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) : CategoryStruct.comp (map f (CategoryStruct.id (⊤_ C))) (rightUnitor Y).hom = CategoryStruct.comp (rightUnitor X).hom f

theorem CategoryTheory.Limits.coprod.rightUnitor_inv_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) : CategoryStruct.comp (rightUnitor Y).inv (map f (CategoryStruct.id (⊥_ C))) = CategoryStruct.comp f (rightUnitor X).inv

theorem CategoryTheory.Limits.coprod.rightUnitor_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) {Z : C} (h : X ⨿ ⊥_ C ⟶ Z) : CategoryStruct.comp (rightUnitor Y).inv (CategoryStruct.comp (map f (CategoryStruct.id (⊥_ C))) h) = CategoryStruct.comp f (CategoryStruct.comp (rightUnitor X).inv h)

theorem CategoryTheory.Limits.prod.rightUnitor_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (map f (CategoryStruct.id (⊤_ C))) (CategoryStruct.comp (rightUnitor Y).hom h) = CategoryStruct.comp (rightUnitor X).hom (CategoryStruct.comp f h)

theorem CategoryTheory.Limits.prod.rightUnitor_inv_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) : CategoryStruct.comp (rightUnitor X).inv (map f (CategoryStruct.id (⊤_ C))) = CategoryStruct.comp f (rightUnitor Y).inv

theorem CategoryTheory.Limits.coprod.rightUnitor_hom_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) : CategoryStruct.comp (map f (CategoryStruct.id (⊥_ C))) (rightUnitor X).hom = CategoryStruct.comp (rightUnitor Y).hom f

theorem CategoryTheory.Limits.prod.rightUnitor_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⨯ ⊤_ C ⟶ Z) : CategoryStruct.comp (rightUnitor X).inv (CategoryStruct.comp (map f (CategoryStruct.id (⊤_ C))) h) = CategoryStruct.comp f (CategoryStruct.comp (rightUnitor Y).inv h)

theorem CategoryTheory.Limits.coprod.rightUnitor_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (map f (CategoryStruct.id (⊥_ C))) (CategoryStruct.comp (rightUnitor X).hom h) = CategoryStruct.comp (rightUnitor Y).hom (CategoryStruct.comp f h)

@[deprecated CategoryTheory.Limits.coprod.rightUnitor_hom_naturality (since := "2026-09-26")]

theorem CategoryTheory.Limits.coprod.rightUnitor_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasInitial C] [HasBinaryCoproducts C] (f : Y ⟶ X) : CategoryStruct.comp (map f (CategoryStruct.id (⊥_ C))) (rightUnitor X).hom = CategoryStruct.comp (rightUnitor Y).hom f

Alias of CategoryTheory.Limits.coprod.rightUnitor_hom_naturality.

@[deprecated CategoryTheory.Limits.prod.rightUnitor_inv_naturality (since := "2026-09-26")]

theorem CategoryTheory.Limits.prod_rightUnitor_inv_naturality {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) : CategoryStruct.comp (prod.rightUnitor X).inv (prod.map f (CategoryStruct.id (⊤_ C))) = CategoryStruct.comp f (prod.rightUnitor Y).inv

Alias of CategoryTheory.Limits.prod.rightUnitor_inv_naturality.

@[deprecated CategoryTheory.Limits.prod.rightUnitor_inv_naturality_assoc (since := "2026-09-26")]

theorem CategoryTheory.Limits.prod_rightUnitor_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {X Y : C} [HasTerminal C] [HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⨯ ⊤_ C ⟶ Z) : CategoryStruct.comp (prod.rightUnitor X).inv (CategoryStruct.comp (prod.map f (CategoryStruct.id (⊤_ C))) h) = CategoryStruct.comp f (CategoryStruct.comp (prod.rightUnitor Y).inv h)

Alias of CategoryTheory.Limits.prod.rightUnitor_inv_naturality_assoc.

theorem CategoryTheory.Limits.prod.triangle {C : Type u} [Category.{v, u} C] [HasTerminal C] [HasBinaryProducts C] (X Y : C) : CategoryStruct.comp (associator X (⊤_ C) Y).hom (map (CategoryStruct.id X) (leftUnitor Y).hom) = map (rightUnitor X).hom (CategoryStruct.id Y)

theorem CategoryTheory.Limits.coprod.pentagon {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (W X Y Z : C) : CategoryStruct.comp (map (associator W X Y).hom (CategoryStruct.id Z)) (CategoryStruct.comp (associator W (X ⨿ Y) Z).hom (map (CategoryStruct.id W) (associator X Y Z).hom)) = CategoryStruct.comp (associator (W ⨿ X) Y Z).hom (associator W X (Y ⨿ Z)).hom

theorem CategoryTheory.Limits.coprod.associator_naturality {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryStruct.comp (map (map f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryStruct.comp (associator X₁ X₂ X₃).hom (map f₁ (map f₂ f₃))

theorem CategoryTheory.Limits.coprod.triangle {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] [HasInitial C] (X Y : C) : CategoryStruct.comp (associator X (⊥_ C) Y).hom (map (CategoryStruct.id X) (leftUnitor Y).hom) = map (rightUnitor X).hom (CategoryStruct.id Y)

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.prod.functor {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] : Functor C (Functor C C)

The binary product functor.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.coprod.functor {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] : Functor C (Functor C C)

The binary coproduct functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.prod.functor_obj_obj {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (X Y : C) : (functor.obj X).obj Y = (X ⨯ Y)

@[simp]

theorem CategoryTheory.Limits.coprod.functor_map_app {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] {Y✝ X✝ : C} (f : Y✝ ⟶ X✝) (T : C) : (functor.map f).app T = map f (CategoryStruct.id T)

@[simp]

theorem CategoryTheory.Limits.coprod.functor_obj_obj {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (X Y : C) : (functor.obj X).obj Y = (X ⨿ Y)

@[simp]

theorem CategoryTheory.Limits.prod.functor_map_app {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : C) : (functor.map f).app T = map f (CategoryStruct.id T)

@[simp]

theorem CategoryTheory.Limits.prod.functor_obj_map {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (X : C) {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (functor.obj X).map g = map (CategoryStruct.id X) g

@[simp]

theorem CategoryTheory.Limits.coprod.functor_obj_map {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (X : C) {x✝ x✝¹ : C} (g : x✝ ⟶ x✝¹) : (functor.obj X).map g = map (CategoryStruct.id X) g

noncomputable def CategoryTheory.Limits.prod.functorLeftComp {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] (X Y : C) : functor.obj (X ⨯ Y) ≅ (functor.obj Y).comp (functor.obj X)

The product functor can be decomposed.

Equations

• CategoryTheory.Limits.prod.functorLeftComp X Y = CategoryTheory.NatIso.ofComponents (CategoryTheory.Limits.prod.associator X Y) ⋯

noncomputable def CategoryTheory.Limits.coprod.functorLeftComp {C : Type u} [Category.{v, u} C] [HasBinaryCoproducts C] (X Y : C) : functor.obj (X ⨿ Y) ≅ (functor.obj Y).comp (functor.obj X)

The coproduct functor can be decomposed.

Equations

• CategoryTheory.Limits.coprod.functorLeftComp X Y = CategoryTheory.NatIso.ofComponents' (CategoryTheory.Limits.coprod.associator X Y) ⋯

theorem CategoryTheory.Limits.HasBinaryProduct.swap {C : Type u} [Category.{v, u} C] (X Y : C) [HasBinaryProduct X Y] : HasBinaryProduct Y X

Construct HasBinaryProduct Y X from HasBinaryProduct X Y. This can't be an instance, as it would cause a loop in typeclass search.

@[implicit_reducible]

noncomputable def CategoryTheory.Over.coprodObj {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} : Over A → Functor (Over A) (Over A)

Auxiliary definition for Over.coprod.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Over.coprodObj_obj {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} (a✝ g : Over A) : a✝.coprodObj.obj g = mk (Limits.coprod.desc a✝.hom g.hom)

@[simp]

theorem CategoryTheory.Over.coprodObj_map {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} (a✝ : Over A) {X✝ Y✝ : Over A} (k : X✝ ⟶ Y✝) : a✝.coprodObj.map k = homMk (Limits.coprod.map (CategoryStruct.id a✝.left) (Hom.left k)) ⋯

@[implicit_reducible]

noncomputable def CategoryTheory.Over.coprod {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} : Functor (Over A) (Functor (Over A) (Over A))

A category with binary coproducts has a functorial sup operation on over categories.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Over.coprod_obj {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} (f : Over A) : coprod.obj f = f.coprodObj

@[simp]

theorem CategoryTheory.Over.coprod_map_app {C : Type u} [Category.{v, u} C] [Limits.HasBinaryCoproducts C] {A : C} {X✝ Y✝ : Over A} (k : X✝ ⟶ Y✝) (g : Over A) : (coprod.map k).app g = homMk (Limits.coprod.map (Hom.left k) (CategoryStruct.id g.left)) ⋯