mathlib documentation

category_theory.limits.shapes.binary_products

Binary (co)products #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
@[protected, instance]
def category_theory.limits.walking_pair.inhabited  :
inhabited category_theory.limits.walking_pair
source
inductive category_theory.limits.walking_pair  :
Type

The type of objects for the diagram indexing a binary (co)product.

Instances for category_theory.limits.walking_pair
source
@[protected, instance]
def category_theory.limits.walking_pair.decidable_eq  :
decidable_eq category_theory.limits.walking_pair
source
def category_theory.limits.walking_pair.swap  :
category_theory.limits.walking_pair ≃ category_theory.limits.walking_pair

The equivalence swapping left and right.

Equations
source
@[simp]
theorem category_theory.limits.walking_pair.swap_apply_left  :
⇑category_theory.limits.walking_pair.swap category_theory.limits.walking_pair.left = category_theory.limits.walking_pair.right
source
@[simp]
theorem category_theory.limits.walking_pair.swap_apply_right  :
⇑category_theory.limits.walking_pair.swap category_theory.limits.walking_pair.right = category_theory.limits.walking_pair.left
source
@[simp]
theorem category_theory.limits.walking_pair.swap_symm_apply_tt  :
⇑(category_theory.limits.walking_pair.swap.symm) category_theory.limits.walking_pair.left = category_theory.limits.walking_pair.right
source
@[simp]
theorem category_theory.limits.walking_pair.swap_symm_apply_ff  :
⇑(category_theory.limits.walking_pair.swap.symm) category_theory.limits.walking_pair.right = category_theory.limits.walking_pair.left
source
def category_theory.limits.walking_pair.equiv_bool  :
category_theory.limits.walking_pair ≃ bool

An equivalence from walking_pair to bool, sometimes useful when reindexing limits.

Equations
source
@[simp]
theorem category_theory.limits.walking_pair.equiv_bool_apply_left  :
⇑category_theory.limits.walking_pair.equiv_bool category_theory.limits.walking_pair.left = bool.tt
source
@[simp]
theorem category_theory.limits.walking_pair.equiv_bool_apply_right  :
⇑category_theory.limits.walking_pair.equiv_bool category_theory.limits.walking_pair.right = bool.ff
source
@[simp]
theorem category_theory.limits.walking_pair.equiv_bool_symm_apply_tt  :
⇑(category_theory.limits.walking_pair.equiv_bool.symm) bool.tt = category_theory.limits.walking_pair.left
source
@[simp]
theorem category_theory.limits.walking_pair.equiv_bool_symm_apply_ff  :
⇑(category_theory.limits.walking_pair.equiv_bool.symm) bool.ff = category_theory.limits.walking_pair.right
source
def category_theory.limits.pair_function {C : Type u} (X Y : C) :
category_theory.limits.walking_pair → C

The function on the walking pair, sending the two points to X and Y.

Equations
source
@[simp]
theorem category_theory.limits.pair_function_left {C : Type u} (X Y : C) :
category_theory.limits.pair_function X Y category_theory.limits.walking_pair.left = X
source
@[simp]
theorem category_theory.limits.pair_function_right {C : Type u} (X Y : C) :
category_theory.limits.pair_function X Y category_theory.limits.walking_pair.right = Y
source
def category_theory.limits.pair {C : Type u} [category_theory.category C] (X Y : C) :
category_theory.discrete category_theory.limits.walking_pair ⥤ C

The diagram on the walking pair, sending the two points to X and Y.

Equations
Instances for category_theory.limits.pair
source
@[simp]
theorem category_theory.limits.pair_obj_left {C : Type u} [category_theory.category C] (X Y : C) :
(category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.left} = X
source
@[simp]
theorem category_theory.limits.pair_obj_right {C : Type u} [category_theory.category C] (X Y : C) :
(category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.right} = Y
source
def category_theory.limits.map_pair {C : Type u} [category_theory.category C] {F G : category_theory.discrete category_theory.limits.walking_pair ⥤ C} (f : F.obj {as := category_theory.limits.walking_pair.left} ⟶ G.obj {as := category_theory.limits.walking_pair.left}) (g : F.obj {as := category_theory.limits.walking_pair.right} ⟶ G.obj {as := category_theory.limits.walking_pair.right}) :
F ⟶ G

The natural transformation between two functors out of the walking pair, specified by its components.

Equations
source
@[simp]
theorem category_theory.limits.map_pair_left {C : Type u} [category_theory.category C] {F G : category_theory.discrete category_theory.limits.walking_pair ⥤ C} (f : F.obj {as := category_theory.limits.walking_pair.left} ⟶ G.obj {as := category_theory.limits.walking_pair.left}) (g : F.obj {as := category_theory.limits.walking_pair.right} ⟶ G.obj {as := category_theory.limits.walking_pair.right}) :
(category_theory.limits.map_pair f g).app {as := category_theory.limits.walking_pair.left} = f
source
@[simp]
theorem category_theory.limits.map_pair_right {C : Type u} [category_theory.category C] {F G : category_theory.discrete category_theory.limits.walking_pair ⥤ C} (f : F.obj {as := category_theory.limits.walking_pair.left} ⟶ G.obj {as := category_theory.limits.walking_pair.left}) (g : F.obj {as := category_theory.limits.walking_pair.right} ⟶ G.obj {as := category_theory.limits.walking_pair.right}) :
(category_theory.limits.map_pair f g).app {as := category_theory.limits.walking_pair.right} = g
source
@[simp]
theorem category_theory.limits.map_pair_iso_hom_app {C : Type u} [category_theory.category C] {F G : category_theory.discrete category_theory.limits.walking_pair ⥤ C} (f : F.obj {as := category_theory.limits.walking_pair.left} ≅ G.obj {as := category_theory.limits.walking_pair.left}) (g : F.obj {as := category_theory.limits.walking_pair.right} ≅ G.obj {as := category_theory.limits.walking_pair.right}) (X : category_theory.discrete category_theory.limits.walking_pair) :
(category_theory.limits.map_pair_iso f g).hom.app X = (category_theory.discrete.rec (category_theory.limits.walking_pair.rec f g) X).hom
source
def category_theory.limits.map_pair_iso {C : Type u} [category_theory.category C] {F G : category_theory.discrete category_theory.limits.walking_pair ⥤ C} (f : F.obj {as := category_theory.limits.walking_pair.left} ≅ G.obj {as := category_theory.limits.walking_pair.left}) (g : F.obj {as := category_theory.limits.walking_pair.right} ≅ G.obj {as := category_theory.limits.walking_pair.right}) :
F ≅ G

The natural isomorphism between two functors out of the walking pair, specified by its components.

Equations
source
@[simp]
theorem category_theory.limits.map_pair_iso_inv_app {C : Type u} [category_theory.category C] {F G : category_theory.discrete category_theory.limits.walking_pair ⥤ C} (f : F.obj {as := category_theory.limits.walking_pair.left} ≅ G.obj {as := category_theory.limits.walking_pair.left}) (g : F.obj {as := category_theory.limits.walking_pair.right} ≅ G.obj {as := category_theory.limits.walking_pair.right}) (X : category_theory.discrete category_theory.limits.walking_pair) :
(category_theory.limits.map_pair_iso f g).inv.app X = (category_theory.discrete.rec (category_theory.limits.walking_pair.rec f g) X).inv
source
def category_theory.limits.diagram_iso_pair {C : Type u} [category_theory.category C] (F : category_theory.discrete category_theory.limits.walking_pair ⥤ C) :
F ≅ category_theory.limits.pair (F.obj {as := category_theory.limits.walking_pair.left}) (F.obj {as := category_theory.limits.walking_pair.right})

Every functor out of the walking pair is naturally isomorphic (actually, equal) to a pair

Equations
source
@[simp]
theorem category_theory.limits.diagram_iso_pair_hom_app {C : Type u} [category_theory.category C] (F : category_theory.discrete category_theory.limits.walking_pair ⥤ C) (X : category_theory.discrete category_theory.limits.walking_pair) :
(category_theory.limits.diagram_iso_pair F).hom.app X = (category_theory.discrete.rec (category_theory.limits.walking_pair.rec (category_theory.iso.refl (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.iso.refl (F.obj {as := category_theory.limits.walking_pair.right}))) X).hom
source
@[simp]
theorem category_theory.limits.diagram_iso_pair_inv_app {C : Type u} [category_theory.category C] (F : category_theory.discrete category_theory.limits.walking_pair ⥤ C) (X : category_theory.discrete category_theory.limits.walking_pair) :
(category_theory.limits.diagram_iso_pair F).inv.app X = (category_theory.discrete.rec (category_theory.limits.walking_pair.rec (category_theory.iso.refl (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.iso.refl (F.obj {as := category_theory.limits.walking_pair.right}))) X).inv
source
def category_theory.limits.pair_comp {C : Type u} [category_theory.category C] {D : Type u} [category_theory.category D] (X Y : C) (F : C ⥤ D) :
category_theory.limits.pair X Y ⋙ F ≅ category_theory.limits.pair (F.obj X) (F.obj Y)

The natural isomorphism between pair X Y ⋙ F and pair (F.obj X) (F.obj Y).

Equations
source
@[reducible]
def category_theory.limits.binary_fan {C : Type u} [category_theory.category C] (X Y : C) :
Type (max u v)

A binary fan is just a cone on a diagram indexing a product.

source
@[reducible]
def category_theory.limits.binary_fan.fst {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_fan X Y) :
((category_theory.functor.const (category_theory.discrete category_theory.limits.walking_pair)).obj s.X).obj {as := category_theory.limits.walking_pair.left} ⟶ (category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.left}

The first projection of a binary fan.

source
@[reducible]
def category_theory.limits.binary_fan.snd {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_fan X Y) :
((category_theory.functor.const (category_theory.discrete category_theory.limits.walking_pair)).obj s.X).obj {as := category_theory.limits.walking_pair.right} ⟶ (category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.right}

The second projection of a binary fan.

source
@[simp]
theorem category_theory.limits.binary_fan.π_app_left {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_fan X Y) :
s.π.app {as := category_theory.limits.walking_pair.left} = s.fst
source
@[simp]
theorem category_theory.limits.binary_fan.π_app_right {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_fan X Y) :
s.π.app {as := category_theory.limits.walking_pair.right} = s.snd
source
def category_theory.limits.binary_fan.is_limit.mk {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_fan X Y) (lift : Π {T : C}, (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.X)) (hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f) (hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g) (uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.X), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g) :
category_theory.limits.is_limit s

A convenient way to show that a binary fan is a limit.

Equations
source
theorem category_theory.limits.binary_fan.is_limit.hom_ext {C : Type u} [category_theory.category C] {W X Y : C} {s : category_theory.limits.binary_fan X Y} (h : category_theory.limits.is_limit s) {f g : W ⟶ s.X} (h₁ : f ≫ s.fst = g ≫ s.fst) (h₂ : f ≫ s.snd = g ≫ s.snd) :
f = g
source
@[reducible]
def category_theory.limits.binary_cofan {C : Type u} [category_theory.category C] (X Y : C) :
Type (max u v)

A binary cofan is just a cocone on a diagram indexing a coproduct.

source
@[reducible]
def category_theory.limits.binary_cofan.inl {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_cofan X Y) :
(category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.left} ⟶ ((category_theory.functor.const (category_theory.discrete category_theory.limits.walking_pair)).obj s.X).obj {as := category_theory.limits.walking_pair.left}

The first inclusion of a binary cofan.

source
@[reducible]
def category_theory.limits.binary_cofan.inr {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_cofan X Y) :
(category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.right} ⟶ ((category_theory.functor.const (category_theory.discrete category_theory.limits.walking_pair)).obj s.X).obj {as := category_theory.limits.walking_pair.right}

The second inclusion of a binary cofan.

source
@[simp]
theorem category_theory.limits.binary_cofan.ι_app_left {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_cofan X Y) :
s.ι.app {as := category_theory.limits.walking_pair.left} = s.inl
source
@[simp]
theorem category_theory.limits.binary_cofan.ι_app_right {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_cofan X Y) :
s.ι.app {as := category_theory.limits.walking_pair.right} = s.inr
source
def category_theory.limits.binary_cofan.is_colimit.mk {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_cofan X Y) (desc : Π {T : C}, (X ⟶ T) → (Y ⟶ T) → (s.X ⟶ T)) (hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f) (hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g) (uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.X ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g) :
category_theory.limits.is_colimit s

A convenient way to show that a binary cofan is a colimit.

Equations
source
theorem category_theory.limits.binary_cofan.is_colimit.hom_ext {C : Type u} [category_theory.category C] {W X Y : C} {s : category_theory.limits.binary_cofan X Y} (h : category_theory.limits.is_colimit s) {f g : s.X ⟶ W} (h₁ : s.inl ≫ f = s.inl ≫ g) (h₂ : s.inr ≫ f = s.inr ≫ g) :
f = g
source
@[simp]
theorem category_theory.limits.binary_fan.mk_X {C : Type u} [category_theory.category C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) :
(category_theory.limits.binary_fan.mk π₁ π₂).X = P
source
def category_theory.limits.binary_fan.mk {C : Type u} [category_theory.category C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) :
category_theory.limits.binary_fan X Y

A binary fan with vertex P consists of the two projections π₁ : P ⟶ X and π₂ : P ⟶ Y.

Equations
source
@[simp]
theorem category_theory.limits.binary_cofan.mk_X {C : Type u} [category_theory.category C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) :
(category_theory.limits.binary_cofan.mk ι₁ ι₂).X = P
source
def category_theory.limits.binary_cofan.mk {C : Type u} [category_theory.category C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) :
category_theory.limits.binary_cofan X Y

A binary cofan with vertex P consists of the two inclusions ι₁ : X ⟶ P and ι₂ : Y ⟶ P.

Equations
source
@[simp]
theorem category_theory.limits.binary_fan.mk_fst {C : Type u} [category_theory.category C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) :
(category_theory.limits.binary_fan.mk π₁ π₂).fst = π₁
source
@[simp]
theorem category_theory.limits.binary_fan.mk_snd {C : Type u} [category_theory.category C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) :
(category_theory.limits.binary_fan.mk π₁ π₂).snd = π₂
source
@[simp]
theorem category_theory.limits.binary_cofan.mk_inl {C : Type u} [category_theory.category C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) :
(category_theory.limits.binary_cofan.mk ι₁ ι₂).inl = ι₁
source
@[simp]
theorem category_theory.limits.binary_cofan.mk_inr {C : Type u} [category_theory.category C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) :
(category_theory.limits.binary_cofan.mk ι₁ ι₂).inr = ι₂
source
def category_theory.limits.iso_binary_fan_mk {C : Type u} [category_theory.category C] {X Y : C} (c : category_theory.limits.binary_fan X Y) :
c ≅ category_theory.limits.binary_fan.mk c.fst c.snd

Every binary_fan is isomorphic to an application of binary_fan.mk.

Equations
source
def category_theory.limits.iso_binary_cofan_mk {C : Type u} [category_theory.category C] {X Y : C} (c : category_theory.limits.binary_cofan X Y) :
c ≅ category_theory.limits.binary_cofan.mk c.inl c.inr

Every binary_fan is isomorphic to an application of binary_fan.mk.

Equations
source
def category_theory.limits.binary_fan.is_limit_mk {C : Type u} [category_theory.category C] {X Y W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : Π (s : category_theory.limits.binary_fan X Y), s.X ⟶ W) (fac_left : ∀ (s : category_theory.limits.binary_fan X Y), lift s ≫ fst = s.fst) (fac_right : ∀ (s : category_theory.limits.binary_fan X Y), lift s ≫ snd = s.snd) (uniq : ∀ (s : category_theory.limits.binary_fan X Y) (m : s.X ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s) :
category_theory.limits.is_limit (category_theory.limits.binary_fan.mk fst snd)

This is a more convenient formulation to show that a binary_fan constructed using binary_fan.mk is a limit cone.

Equations
source
def category_theory.limits.binary_cofan.is_colimit_mk {C : Type u} [category_theory.category C] {X Y W : C} {inl : X ⟶ W} {inr : Y ⟶ W} (desc : Π (s : category_theory.limits.binary_cofan X Y), W ⟶ s.X) (fac_left : ∀ (s : category_theory.limits.binary_cofan X Y), inl ≫ desc s = s.inl) (fac_right : ∀ (s : category_theory.limits.binary_cofan X Y), inr ≫ desc s = s.inr) (uniq : ∀ (s : category_theory.limits.binary_cofan X Y) (m : W ⟶ s.X), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s) :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk inl inr)

This is a more convenient formulation to show that a binary_cofan constructed using binary_cofan.mk is a colimit cocone.

Equations
source
def category_theory.limits.binary_fan.is_limit.lift' {C : Type u} [category_theory.category C] {W X Y : C} {s : category_theory.limits.binary_fan X Y} (h : category_theory.limits.is_limit s) (f : W ⟶ X) (g : W ⟶ Y) :
{l // l ≫ s.fst = f ∧ l ≫ s.snd = g}

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
source
@[simp]
theorem category_theory.limits.binary_fan.is_limit.lift'_coe {C : Type u} [category_theory.category C] {W X Y : C} {s : category_theory.limits.binary_fan X Y} (h : category_theory.limits.is_limit s) (f : W ⟶ X) (g : W ⟶ Y) :
↑(category_theory.limits.binary_fan.is_limit.lift' h f g) = h.lift (category_theory.limits.binary_fan.mk f g)
source
def category_theory.limits.binary_cofan.is_colimit.desc' {C : Type u} [category_theory.category C] {W X Y : C} {s : category_theory.limits.binary_cofan X Y} (h : category_theory.limits.is_colimit s) (f : X ⟶ W) (g : Y ⟶ W) :
{l // s.inl ≫ l = f ∧ s.inr ≫ l = g}

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
source
@[simp]
theorem category_theory.limits.binary_cofan.is_colimit.desc'_coe {C : Type u} [category_theory.category C] {W X Y : C} {s : category_theory.limits.binary_cofan X Y} (h : category_theory.limits.is_colimit s) (f : X ⟶ W) (g : Y ⟶ W) :
↑(category_theory.limits.binary_cofan.is_colimit.desc' h f g) = h.desc (category_theory.limits.binary_cofan.mk f g)
source
def category_theory.limits.binary_fan.is_limit_flip {C : Type u} [category_theory.category C] {X Y : C} {c : category_theory.limits.binary_fan X Y} (hc : category_theory.limits.is_limit c) :
category_theory.limits.is_limit (category_theory.limits.binary_fan.mk c.snd c.fst)

Binary products are symmetric.

Equations
source
theorem category_theory.limits.binary_fan.is_limit_iff_is_iso_fst {C : Type u} [category_theory.category C] {X Y : C} (h : category_theory.limits.is_terminal Y) (c : category_theory.limits.binary_fan X Y) :
nonempty (category_theory.limits.is_limit c) ↔ category_theory.is_iso c.fst
source
theorem category_theory.limits.binary_fan.is_limit_iff_is_iso_snd {C : Type u} [category_theory.category C] {X Y : C} (h : category_theory.limits.is_terminal X) (c : category_theory.limits.binary_fan X Y) :
nonempty (category_theory.limits.is_limit c) ↔ category_theory.is_iso c.snd
source
noncomputable def category_theory.limits.binary_fan.is_limit_comp_left_iso {C : Type u} [category_theory.category C] {X Y X' : C} (c : category_theory.limits.binary_fan X Y) (f : X ⟶ X') [category_theory.is_iso f] (h : category_theory.limits.is_limit c) :
category_theory.limits.is_limit (category_theory.limits.binary_fan.mk (c.fst ≫ f) c.snd)

If X' ≅ X, then X × Y also is the product of X' and Y.

Equations
source
noncomputable def category_theory.limits.binary_fan.is_limit_comp_right_iso {C : Type u} [category_theory.category C] {X Y Y' : C} (c : category_theory.limits.binary_fan X Y) (f : Y ⟶ Y') [category_theory.is_iso f] (h : category_theory.limits.is_limit c) :
category_theory.limits.is_limit (category_theory.limits.binary_fan.mk c.fst (c.snd ≫ f))

If Y' ≅ Y, then X x Y also is the product of X and Y'.

Equations
source
def category_theory.limits.binary_cofan.is_colimit_flip {C : Type u} [category_theory.category C] {X Y : C} {c : category_theory.limits.binary_cofan X Y} (hc : category_theory.limits.is_colimit c) :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk c.inr c.inl)

Binary coproducts are symmetric.

Equations
source
theorem category_theory.limits.binary_cofan.is_colimit_iff_is_iso_inl {C : Type u} [category_theory.category C] {X Y : C} (h : category_theory.limits.is_initial Y) (c : category_theory.limits.binary_cofan X Y) :
nonempty (category_theory.limits.is_colimit c) ↔ category_theory.is_iso c.inl
source
theorem category_theory.limits.binary_cofan.is_colimit_iff_is_iso_inr {C : Type u} [category_theory.category C] {X Y : C} (h : category_theory.limits.is_initial X) (c : category_theory.limits.binary_cofan X Y) :
nonempty (category_theory.limits.is_colimit c) ↔ category_theory.is_iso c.inr
source
noncomputable def category_theory.limits.binary_cofan.is_colimit_comp_left_iso {C : Type u} [category_theory.category C] {X Y X' : C} (c : category_theory.limits.binary_cofan X Y) (f : X' ⟶ X) [category_theory.is_iso f] (h : category_theory.limits.is_colimit c) :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk (f ≫ c.inl) c.inr)

If X' ≅ X, then X ⨿ Y also is the coproduct of X' and Y.

Equations
source
noncomputable def category_theory.limits.binary_cofan.is_colimit_comp_right_iso {C : Type u} [category_theory.category C] {X Y Y' : C} (c : category_theory.limits.binary_cofan X Y) (f : Y' ⟶ Y) [category_theory.is_iso f] (h : category_theory.limits.is_colimit c) :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk c.inl (f ≫ c.inr))

If Y' ≅ Y, then X ⨿ Y also is the coproduct of X and Y'.

Equations
source
@[reducible]
def category_theory.limits.has_binary_product {C : Type u} [category_theory.category C] (X Y : C) :
Prop

An abbreviation for has_limit (pair X Y).

source
@[reducible]
def category_theory.limits.has_binary_coproduct {C : Type u} [category_theory.category C] (X Y : C) :
Prop

An abbreviation for has_colimit (pair X Y).

source
@[reducible]
noncomputable def category_theory.limits.prod {C : Type u} [category_theory.category C] (X Y : C) [category_theory.limits.has_binary_product X Y] :
C

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

source
@[reducible]
noncomputable def category_theory.limits.coprod {C : Type u} [category_theory.category C] (X Y : C) [category_theory.limits.has_binary_coproduct X Y] :
C

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

source
@[reducible]
noncomputable def category_theory.limits.prod.fst {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_product X Y] :
X ⨯ Y ⟶ X

The projection map to the first component of the product.

source
@[reducible]
noncomputable def category_theory.limits.prod.snd {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_product X Y] :
X ⨯ Y ⟶ Y

The projecton map to the second component of the product.

source
@[reducible]
noncomputable def category_theory.limits.coprod.inl {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_coproduct X Y] :
X ⟶ X ⨿ Y

The inclusion map from the first component of the coproduct.

source
@[reducible]
noncomputable def category_theory.limits.coprod.inr {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_coproduct X Y] :
Y ⟶ X ⨿ Y

The inclusion map from the second component of the coproduct.

source
noncomputable def category_theory.limits.prod_is_prod {C : Type u} [category_theory.category C] (X Y : C) [category_theory.limits.has_binary_product X Y] :
category_theory.limits.is_limit (category_theory.limits.binary_fan.mk category_theory.limits.prod.fst category_theory.limits.prod.snd)

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

Equations
source
noncomputable def category_theory.limits.coprod_is_coprod {C : Type u} [category_theory.category C] (X Y : C) [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk category_theory.limits.coprod.inl category_theory.limits.coprod.inr)

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

Equations
source
@[ext]
theorem category_theory.limits.prod.hom_ext {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product X Y] {f g : W ⟶ X ⨯ Y} (h₁ : f ≫ category_theory.limits.prod.fst = g ≫ category_theory.limits.prod.fst) (h₂ : f ≫ category_theory.limits.prod.snd = g ≫ category_theory.limits.prod.snd) :
f = g
source
@[ext]
theorem category_theory.limits.coprod.hom_ext {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct X Y] {f g : X ⨿ Y ⟶ W} (h₁ : category_theory.limits.coprod.inl ≫ f = category_theory.limits.coprod.inl ≫ g) (h₂ : category_theory.limits.coprod.inr ≫ f = category_theory.limits.coprod.inr ≫ g) :
f = g
source
@[reducible]
noncomputable def category_theory.limits.prod.lift {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product 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.

source
@[reducible]
noncomputable def category_theory.limits.diag {C : Type u} [category_theory.category C] (X : C) [category_theory.limits.has_binary_product X X] :
X ⟶ X ⨯ X

diagonal arrow of the binary product in the category fam I

source
@[reducible]
noncomputable def category_theory.limits.coprod.desc {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct 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.

source
@[reducible]
noncomputable def category_theory.limits.codiag {C : Type u} [category_theory.category C] (X : C) [category_theory.limits.has_binary_coproduct X X] :
X ⨿ X ⟶ X

codiagonal arrow of the binary coproduct

source
@[simp]
theorem category_theory.limits.prod.lift_fst_assoc {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) {X' : C} (f' : X ⟶ X') :
category_theory.limits.prod.lift f g ≫ category_theory.limits.prod.fst ≫ f' = f ≫ f'
source
@[simp]
theorem category_theory.limits.prod.lift_fst {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) :
category_theory.limits.prod.lift f g ≫ category_theory.limits.prod.fst = f
source
@[simp]
theorem category_theory.limits.prod.lift_snd {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) :
category_theory.limits.prod.lift f g ≫ category_theory.limits.prod.snd = g
source
@[simp]
theorem category_theory.limits.prod.lift_snd_assoc {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) {X' : C} (f' : Y ⟶ X') :
category_theory.limits.prod.lift f g ≫ category_theory.limits.prod.snd ≫ f' = g ≫ f'
source
@[simp]
theorem category_theory.limits.coprod.inl_desc {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.desc f g = f
source
theorem category_theory.limits.coprod.inl_desc_assoc {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {X' : C} (f' : W ⟶ X') :
category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.desc f g ≫ f' = f ≫ f'
source
theorem category_theory.limits.coprod.inr_desc_assoc {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {X' : C} (f' : W ⟶ X') :
category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.desc f g ≫ f' = g ≫ f'
source
@[simp]
theorem category_theory.limits.coprod.inr_desc {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.desc f g = g
source
@[protected, instance]
def category_theory.limits.prod.mono_lift_of_mono_left {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) [category_theory.mono f] :
category_theory.mono (category_theory.limits.prod.lift f g)
source
@[protected, instance]
def category_theory.limits.prod.mono_lift_of_mono_right {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) [category_theory.mono g] :
category_theory.mono (category_theory.limits.prod.lift f g)
source
@[protected, instance]
def category_theory.limits.coprod.epi_desc_of_epi_left {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [category_theory.epi f] :
category_theory.epi (category_theory.limits.coprod.desc f g)
source
@[protected, instance]
def category_theory.limits.coprod.epi_desc_of_epi_right {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [category_theory.epi g] :
category_theory.epi (category_theory.limits.coprod.desc f g)
source
noncomputable def category_theory.limits.prod.lift' {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product X Y] (f : W ⟶ X) (g : W ⟶ Y) :
{l // l ≫ category_theory.limits.prod.fst = f ∧ l ≫ category_theory.limits.prod.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
source
noncomputable def category_theory.limits.coprod.desc' {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) :
{l // category_theory.limits.coprod.inl ≫ l = f ∧ category_theory.limits.coprod.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
source
noncomputable def category_theory.limits.prod.map {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product 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
Instances for category_theory.limits.prod.map
source
noncomputable def category_theory.limits.coprod.map {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct 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 morphisms f : W ⟶ Y and g : W ⟶ Z induces a morphism coprod.map f g : W ⨿ X ⟶ Y ⨿ Z.

Equations
Instances for category_theory.limits.coprod.map
source
theorem category_theory.limits.prod.comp_lift_assoc {C : Type u} [category_theory.category C] {V W X Y : C} [category_theory.limits.has_binary_product X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) {X' : C} (f' : X ⨯ Y ⟶ X') :
f ≫ category_theory.limits.prod.lift g h ≫ f' = category_theory.limits.prod.lift (f ≫ g) (f ≫ h) ≫ f'
source
@[simp]
theorem category_theory.limits.prod.comp_lift {C : Type u} [category_theory.category C] {V W X Y : C} [category_theory.limits.has_binary_product X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
f ≫ category_theory.limits.prod.lift g h = category_theory.limits.prod.lift (f ≫ g) (f ≫ h)
source
theorem category_theory.limits.prod.comp_diag {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_product Y Y] (f : X ⟶ Y) :
f ≫ category_theory.limits.diag Y = category_theory.limits.prod.lift f f
source
@[simp]
theorem category_theory.limits.prod.map_fst {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
category_theory.limits.prod.map f g ≫ category_theory.limits.prod.fst = category_theory.limits.prod.fst ≫ f
source
@[simp]
theorem category_theory.limits.prod.map_fst_assoc {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {X' : C} (f' : Y ⟶ X') :
category_theory.limits.prod.map f g ≫ category_theory.limits.prod.fst ≫ f' = category_theory.limits.prod.fst ≫ f ≫ f'
source
@[simp]
theorem category_theory.limits.prod.map_snd_assoc {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {X' : C} (f' : Z ⟶ X') :
category_theory.limits.prod.map f g ≫ category_theory.limits.prod.snd ≫ f' = category_theory.limits.prod.snd ≫ g ≫ f'
source
@[simp]
theorem category_theory.limits.prod.map_snd {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
category_theory.limits.prod.map f g ≫ category_theory.limits.prod.snd = category_theory.limits.prod.snd ≫ g
source
@[simp]
theorem category_theory.limits.prod.map_id_id {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_product X Y] :
category_theory.limits.prod.map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨯ Y)
source
@[simp]
theorem category_theory.limits.prod.lift_fst_snd {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_product X Y] :
category_theory.limits.prod.lift category_theory.limits.prod.fst category_theory.limits.prod.snd = 𝟙 (X ⨯ Y)
source
@[simp]
theorem category_theory.limits.prod.lift_map_assoc {C : Type u} [category_theory.category C] {V W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) {X' : C} (f' : Y ⨯ Z ⟶ X') :
category_theory.limits.prod.lift f g ≫ category_theory.limits.prod.map h k ≫ f' = category_theory.limits.prod.lift (f ≫ h) (g ≫ k) ≫ f'
source
@[simp]
theorem category_theory.limits.prod.lift_map {C : Type u} [category_theory.category C] {V W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) :
category_theory.limits.prod.lift f g ≫ category_theory.limits.prod.map h k = category_theory.limits.prod.lift (f ≫ h) (g ≫ k)
source
@[simp]
theorem category_theory.limits.prod.lift_fst_comp_snd_comp {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W Y] [category_theory.limits.has_binary_product X Z] (g : W ⟶ X) (g' : Y ⟶ Z) :
category_theory.limits.prod.lift (category_theory.limits.prod.fst ≫ g) (category_theory.limits.prod.snd ≫ g') = category_theory.limits.prod.map g g'
source
@[simp]
theorem category_theory.limits.prod.map_map_assoc {C : Type u} [category_theory.category C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [category_theory.limits.has_binary_product A₁ B₁] [category_theory.limits.has_binary_product A₂ B₂] [category_theory.limits.has_binary_product A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) {X' : C} (f' : A₃ ⨯ B₃ ⟶ X') :
category_theory.limits.prod.map f g ≫ category_theory.limits.prod.map h k ≫ f' = category_theory.limits.prod.map (f ≫ h) (g ≫ k) ≫ f'
source
@[simp]
theorem category_theory.limits.prod.map_map {C : Type u} [category_theory.category C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [category_theory.limits.has_binary_product A₁ B₁] [category_theory.limits.has_binary_product A₂ B₂] [category_theory.limits.has_binary_product A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) :
category_theory.limits.prod.map f g ≫ category_theory.limits.prod.map h k = category_theory.limits.prod.map (f ≫ h) (g ≫ k)
source
theorem category_theory.limits.prod.map_swap {C : Type u} [category_theory.category C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] :
category_theory.limits.prod.map (𝟙 X) f ≫ category_theory.limits.prod.map g (𝟙 B) = category_theory.limits.prod.map g (𝟙 A) ≫ category_theory.limits.prod.map (𝟙 Y) f
source
theorem category_theory.limits.prod.map_swap_assoc {C : Type u} [category_theory.category C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] {X' : C} (f' : Y ⨯ B ⟶ X') :
category_theory.limits.prod.map (𝟙 X) f ≫ category_theory.limits.prod.map g (𝟙 B) ≫ f' = category_theory.limits.prod.map g (𝟙 A) ≫ category_theory.limits.prod.map (𝟙 Y) f ≫ f'
source
theorem category_theory.limits.prod.map_comp_id_assoc {C : Type u} [category_theory.category C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.limits.has_binary_product X W] [category_theory.limits.has_binary_product Z W] [category_theory.limits.has_binary_product Y W] {X' : C} (f' : Z ⨯ W ⟶ X') :
category_theory.limits.prod.map (f ≫ g) (𝟙 W) ≫ f' = category_theory.limits.prod.map f (𝟙 W) ≫ category_theory.limits.prod.map g (𝟙 W) ≫ f'
source
theorem category_theory.limits.prod.map_comp_id {C : Type u} [category_theory.category C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.limits.has_binary_product X W] [category_theory.limits.has_binary_product Z W] [category_theory.limits.has_binary_product Y W] :
category_theory.limits.prod.map (f ≫ g) (𝟙 W) = category_theory.limits.prod.map f (𝟙 W) ≫ category_theory.limits.prod.map g (𝟙 W)
source
theorem category_theory.limits.prod.map_id_comp {C : Type u} [category_theory.category C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product W Y] [category_theory.limits.has_binary_product W Z] :
category_theory.limits.prod.map (𝟙 W) (f ≫ g) = category_theory.limits.prod.map (𝟙 W) f ≫ category_theory.limits.prod.map (𝟙 W) g
source
theorem category_theory.limits.prod.map_id_comp_assoc {C : Type u} [category_theory.category C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product W Y] [category_theory.limits.has_binary_product W Z] {X' : C} (f' : W ⨯ Z ⟶ X') :
category_theory.limits.prod.map (𝟙 W) (f ≫ g) ≫ f' = category_theory.limits.prod.map (𝟙 W) f ≫ category_theory.limits.prod.map (𝟙 W) g ≫ f'
source
@[simp]
theorem category_theory.limits.prod.map_iso_hom {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] (f : W ≅ Y) (g : X ≅ Z) :
(category_theory.limits.prod.map_iso f g).hom = category_theory.limits.prod.map f.hom g.hom
source
@[simp]
theorem category_theory.limits.prod.map_iso_inv {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] (f : W ≅ Y) (g : X ≅ Z) :
(category_theory.limits.prod.map_iso f g).inv = category_theory.limits.prod.map f.inv g.inv
source
noncomputable def category_theory.limits.prod.map_iso {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product 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.map_iso f g : W ⨯ X ≅ Y ⨯ Z.

Equations
source
@[protected, instance]
def category_theory.limits.is_iso_prod {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [category_theory.is_iso f] [category_theory.is_iso g] :
category_theory.is_iso (category_theory.limits.prod.map f g)
source
@[protected, instance]
def category_theory.limits.prod.map_mono {C : Type u_1} [category_theory.category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [category_theory.mono f] [category_theory.mono g] [category_theory.limits.has_binary_product W X] [category_theory.limits.has_binary_product Y Z] :
category_theory.mono (category_theory.limits.prod.map f g)
source
@[simp]
theorem category_theory.limits.prod.diag_map {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_binary_product X X] [category_theory.limits.has_binary_product Y Y] :
category_theory.limits.diag X ≫ category_theory.limits.prod.map f f = f ≫ category_theory.limits.diag Y
source
@[simp]
theorem category_theory.limits.prod.diag_map_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_binary_product X X] [category_theory.limits.has_binary_product Y Y] {X' : C} (f' : Y ⨯ Y ⟶ X') :
category_theory.limits.diag X ≫ category_theory.limits.prod.map f f ≫ f' = f ≫ category_theory.limits.diag Y ≫ f'
source
@[simp]
theorem category_theory.limits.prod.diag_map_fst_snd_assoc {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_product X Y] [category_theory.limits.has_binary_product (X ⨯ Y) (X ⨯ Y)] {X' : C} (f' : X ⨯ Y ⟶ X') :
category_theory.limits.diag (X ⨯ Y) ≫ category_theory.limits.prod.map category_theory.limits.prod.fst category_theory.limits.prod.snd ≫ f' = f'
source
@[simp]
theorem category_theory.limits.prod.diag_map_fst_snd {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_product X Y] [category_theory.limits.has_binary_product (X ⨯ Y) (X ⨯ Y)] :
category_theory.limits.diag (X ⨯ Y) ≫ category_theory.limits.prod.map category_theory.limits.prod.fst category_theory.limits.prod.snd = 𝟙 (X ⨯ Y)
source
@[simp]
theorem category_theory.limits.prod.diag_map_fst_snd_comp {C : Type u} [category_theory.category C] [category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') :
category_theory.limits.diag (X ⨯ X') ≫ category_theory.limits.prod.map (category_theory.limits.prod.fst ≫ g) (category_theory.limits.prod.snd ≫ g') = category_theory.limits.prod.map g g'
source
@[simp]
theorem category_theory.limits.prod.diag_map_fst_snd_comp_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') {X'_1 : C} (f' : Y ⨯ Y' ⟶ X'_1) :
category_theory.limits.diag (X ⨯ X') ≫ category_theory.limits.prod.map (category_theory.limits.prod.fst ≫ g) (category_theory.limits.prod.snd ≫ g') ≫ f' = category_theory.limits.prod.map g g' ≫ f'
source
@[protected, instance]
def category_theory.limits.diag.category_theory.is_split_mono {C : Type u} [category_theory.category C] {X : C} [category_theory.limits.has_binary_product X X] :
category_theory.is_split_mono (category_theory.limits.diag X)
source
@[simp]
theorem category_theory.limits.coprod.desc_comp {C : Type u} [category_theory.category C] {V W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) :
category_theory.limits.coprod.desc g h ≫ f = category_theory.limits.coprod.desc (g ≫ f) (h ≫ f)
source
@[simp]
theorem category_theory.limits.coprod.desc_comp_assoc {C : Type u} [category_theory.category C] {V W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (f : V ⟶ W) (g : X ⟶ V) (h : Y ⟶ V) {X' : C} (f' : W ⟶ X') :
category_theory.limits.coprod.desc g h ≫ f ≫ f' = category_theory.limits.coprod.desc (g ≫ f) (h ≫ f) ≫ f'
source
theorem category_theory.limits.coprod.diag_comp {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_coproduct X X] (f : X ⟶ Y) :
category_theory.limits.codiag X ≫ f = category_theory.limits.coprod.desc f f
source
@[simp]
theorem category_theory.limits.coprod.inl_map {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.map f g = f ≫ category_theory.limits.coprod.inl
source
@[simp]
theorem category_theory.limits.coprod.inl_map_assoc {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {X' : C} (f' : Y ⨿ Z ⟶ X') :
category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.map f g ≫ f' = f ≫ category_theory.limits.coprod.inl ≫ f'
source
@[simp]
theorem category_theory.limits.coprod.inr_map_assoc {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {X' : C} (f' : Y ⨿ Z ⟶ X') :
category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.map f g ≫ f' = g ≫ category_theory.limits.coprod.inr ≫ f'
source
@[simp]
theorem category_theory.limits.coprod.inr_map {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) :
category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.map f g = g ≫ category_theory.limits.coprod.inr
source
@[simp]
theorem category_theory.limits.coprod.map_id_id {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.coprod.map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨿ Y)
source
@[simp]
theorem category_theory.limits.coprod.desc_inl_inr {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_coproduct X Y] :
category_theory.limits.coprod.desc category_theory.limits.coprod.inl category_theory.limits.coprod.inr = 𝟙 (X ⨿ Y)
source
@[simp]
theorem category_theory.limits.coprod.map_desc {C : Type u} [category_theory.category C] {S T U V W : C} [category_theory.limits.has_binary_coproduct U W] [category_theory.limits.has_binary_coproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) :
category_theory.limits.coprod.map h k ≫ category_theory.limits.coprod.desc f g = category_theory.limits.coprod.desc (h ≫ f) (k ≫ g)
source
theorem category_theory.limits.coprod.map_desc_assoc {C : Type u} [category_theory.category C] {S T U V W : C} [category_theory.limits.has_binary_coproduct U W] [category_theory.limits.has_binary_coproduct T V] (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) {X' : C} (f' : S ⟶ X') :
category_theory.limits.coprod.map h k ≫ category_theory.limits.coprod.desc f g ≫ f' = category_theory.limits.coprod.desc (h ≫ f) (k ≫ g) ≫ f'
source
@[simp]
theorem category_theory.limits.coprod.desc_comp_inl_comp_inr {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W Y] [category_theory.limits.has_binary_coproduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) :
category_theory.limits.coprod.desc (g ≫ category_theory.limits.coprod.inl) (g' ≫ category_theory.limits.coprod.inr) = category_theory.limits.coprod.map g g'
source
@[simp]
theorem category_theory.limits.coprod.map_map_assoc {C : Type u} [category_theory.category C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [category_theory.limits.has_binary_coproduct A₁ B₁] [category_theory.limits.has_binary_coproduct A₂ B₂] [category_theory.limits.has_binary_coproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) {X' : C} (f' : A₃ ⨿ B₃ ⟶ X') :
category_theory.limits.coprod.map f g ≫ category_theory.limits.coprod.map h k ≫ f' = category_theory.limits.coprod.map (f ≫ h) (g ≫ k) ≫ f'
source
@[simp]
theorem category_theory.limits.coprod.map_map {C : Type u} [category_theory.category C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [category_theory.limits.has_binary_coproduct A₁ B₁] [category_theory.limits.has_binary_coproduct A₂ B₂] [category_theory.limits.has_binary_coproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) :
category_theory.limits.coprod.map f g ≫ category_theory.limits.coprod.map h k = category_theory.limits.coprod.map (f ≫ h) (g ≫ k)
source
theorem category_theory.limits.coprod.map_swap {C : Type u} [category_theory.category C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] :
category_theory.limits.coprod.map (𝟙 X) f ≫ category_theory.limits.coprod.map g (𝟙 B) = category_theory.limits.coprod.map g (𝟙 A) ≫ category_theory.limits.coprod.map (𝟙 Y) f
source
theorem category_theory.limits.coprod.map_swap_assoc {C : Type u} [category_theory.category C] {A B X Y : C} (f : A ⟶ B) (g : X ⟶ Y) [category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] {X' : C} (f' : Y ⨿ B ⟶ X') :
category_theory.limits.coprod.map (𝟙 X) f ≫ category_theory.limits.coprod.map g (𝟙 B) ≫ f' = category_theory.limits.coprod.map g (𝟙 A) ≫ category_theory.limits.coprod.map (𝟙 Y) f ≫ f'
source
theorem category_theory.limits.coprod.map_comp_id {C : Type u} [category_theory.category C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.limits.has_binary_coproduct Z W] [category_theory.limits.has_binary_coproduct Y W] [category_theory.limits.has_binary_coproduct X W] :
category_theory.limits.coprod.map (f ≫ g) (𝟙 W) = category_theory.limits.coprod.map f (𝟙 W) ≫ category_theory.limits.coprod.map g (𝟙 W)
source
theorem category_theory.limits.coprod.map_comp_id_assoc {C : Type u} [category_theory.category C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.limits.has_binary_coproduct Z W] [category_theory.limits.has_binary_coproduct Y W] [category_theory.limits.has_binary_coproduct X W] {X' : C} (f' : Z ⨿ W ⟶ X') :
category_theory.limits.coprod.map (f ≫ g) (𝟙 W) ≫ f' = category_theory.limits.coprod.map f (𝟙 W) ≫ category_theory.limits.coprod.map g (𝟙 W) ≫ f'
source
theorem category_theory.limits.coprod.map_id_comp_assoc {C : Type u} [category_theory.category C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct W Y] [category_theory.limits.has_binary_coproduct W Z] {X' : C} (f' : W ⨿ Z ⟶ X') :
category_theory.limits.coprod.map (𝟙 W) (f ≫ g) ≫ f' = category_theory.limits.coprod.map (𝟙 W) f ≫ category_theory.limits.coprod.map (𝟙 W) g ≫ f'
source
theorem category_theory.limits.coprod.map_id_comp {C : Type u} [category_theory.category C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct W Y] [category_theory.limits.has_binary_coproduct W Z] :
category_theory.limits.coprod.map (𝟙 W) (f ≫ g) = category_theory.limits.coprod.map (𝟙 W) f ≫ category_theory.limits.coprod.map (𝟙 W) g
source
@[simp]
theorem category_theory.limits.coprod.map_iso_hom {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) :
(category_theory.limits.coprod.map_iso f g).hom = category_theory.limits.coprod.map f.hom g.hom
source
@[simp]
theorem category_theory.limits.coprod.map_iso_inv {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct Y Z] (f : W ≅ Y) (g : X ≅ Z) :
(category_theory.limits.coprod.map_iso f g).inv = category_theory.limits.coprod.map f.inv g.inv
source
noncomputable def category_theory.limits.coprod.map_iso {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct 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 a isomorphism coprod.map_iso f g : W ⨿ X ≅ Y ⨿ Z.

Equations
source
@[protected, instance]
def category_theory.limits.is_iso_coprod {C : Type u} [category_theory.category C] {W X Y Z : C} [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) [category_theory.is_iso f] [category_theory.is_iso g] :
category_theory.is_iso (category_theory.limits.coprod.map f g)
source
@[protected, instance]
def category_theory.limits.coprod.map_epi {C : Type u_1} [category_theory.category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [category_theory.epi f] [category_theory.epi g] [category_theory.limits.has_binary_coproduct W X] [category_theory.limits.has_binary_coproduct Y Z] :
category_theory.epi (category_theory.limits.coprod.map f g)
source
@[simp]
theorem category_theory.limits.coprod.map_codiag {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_binary_coproduct X X] [category_theory.limits.has_binary_coproduct Y Y] :
category_theory.limits.coprod.map f f ≫ category_theory.limits.codiag Y = category_theory.limits.codiag X ≫ f
source
theorem category_theory.limits.coprod.map_codiag_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_binary_coproduct X X] [category_theory.limits.has_binary_coproduct Y Y] {X' : C} (f' : Y ⟶ X') :
category_theory.limits.coprod.map f f ≫ category_theory.limits.codiag Y ≫ f' = category_theory.limits.codiag X ≫ f ≫ f'
source
@[simp]
theorem category_theory.limits.coprod.map_inl_inr_codiag {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_coproduct X Y] [category_theory.limits.has_binary_coproduct (X ⨿ Y) (X ⨿ Y)] :
category_theory.limits.coprod.map category_theory.limits.coprod.inl category_theory.limits.coprod.inr ≫ category_theory.limits.codiag (X ⨿ Y) = 𝟙 (X ⨿ Y)
source
theorem category_theory.limits.coprod.map_inl_inr_codiag_assoc {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_binary_coproduct X Y] [category_theory.limits.has_binary_coproduct (X ⨿ Y) (X ⨿ Y)] {X' : C} (f' : X ⨿ Y ⟶ X') :
category_theory.limits.coprod.map category_theory.limits.coprod.inl category_theory.limits.coprod.inr ≫ category_theory.limits.codiag (X ⨿ Y) ≫ f' = f'
source
@[simp]
theorem category_theory.limits.coprod.map_comp_inl_inr_codiag {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') :
category_theory.limits.coprod.map (g ≫ category_theory.limits.coprod.inl) (g' ≫ category_theory.limits.coprod.inr) ≫ category_theory.limits.codiag (Y ⨿ Y') = category_theory.limits.coprod.map g g'
source
theorem category_theory.limits.coprod.map_comp_inl_inr_codiag_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y') {X'_1 : C} (f' : Y ⨿ Y' ⟶ X'_1) :
category_theory.limits.coprod.map (g ≫ category_theory.limits.coprod.inl) (g' ≫ category_theory.limits.coprod.inr) ≫ category_theory.limits.codiag (Y ⨿ Y') ≫ f' = category_theory.limits.coprod.map g g' ≫ f'
source
@[reducible]
def category_theory.limits.has_binary_products (C : Type u) [category_theory.category C] :
Prop

has_binary_products represents a choice of product for every pair of objects.

See https://stacks.math.columbia.edu/tag/001T.

source
@[reducible]
def category_theory.limits.has_binary_coproducts (C : Type u) [category_theory.category C] :
Prop

has_binary_coproducts represents a choice of coproduct for every pair of objects.

See https://stacks.math.columbia.edu/tag/04AP.

source
theorem category_theory.limits.has_binary_products_of_has_limit_pair (C : Type u) [category_theory.category C] [∀ {X Y : C}, category_theory.limits.has_limit (category_theory.limits.pair X Y)] :
category_theory.limits.has_binary_products C

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

source
theorem category_theory.limits.has_binary_coproducts_of_has_colimit_pair (C : Type u) [category_theory.category C] [∀ {X Y : C}, category_theory.limits.has_colimit (category_theory.limits.pair X Y)] :
category_theory.limits.has_binary_coproducts C

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

source
noncomputable def category_theory.limits.prod.braiding {C : Type u} [category_theory.category C] (P Q : C) [category_theory.limits.has_binary_product P Q] [category_theory.limits.has_binary_product Q P] :
P ⨯ Q ≅ Q ⨯ P

The braiding isomorphism which swaps a binary product.

Equations
source
@[simp]
theorem category_theory.limits.prod.braiding_inv {C : Type u} [category_theory.category C] (P Q : C) [category_theory.limits.has_binary_product P Q] [category_theory.limits.has_binary_product Q P] :
(category_theory.limits.prod.braiding P Q).inv = category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst
source
@[simp]
theorem category_theory.limits.prod.braiding_hom {C : Type u} [category_theory.category C] (P Q : C) [category_theory.limits.has_binary_product P Q] [category_theory.limits.has_binary_product Q P] :
(category_theory.limits.prod.braiding P Q).hom = category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst
source
theorem category_theory.limits.braid_natural_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {X' : C} (f' : W ⨯ Y ⟶ X') :
category_theory.limits.prod.map f g ≫ (category_theory.limits.prod.braiding Y W).hom ≫ f' = (category_theory.limits.prod.braiding X Z).hom ≫ category_theory.limits.prod.map g f ≫ f'
source
theorem category_theory.limits.braid_natural {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
category_theory.limits.prod.map f g ≫ (category_theory.limits.prod.braiding Y W).hom = (category_theory.limits.prod.braiding X Z).hom ≫ category_theory.limits.prod.map g f

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

source
theorem category_theory.limits.prod.symmetry'_assoc {C : Type u} [category_theory.category C] (P Q : C) [category_theory.limits.has_binary_product P Q] [category_theory.limits.has_binary_product Q P] {X' : C} (f' : P ⨯ Q ⟶ X') :
category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst ≫ category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst ≫ f' = f'
source
theorem category_theory.limits.prod.symmetry' {C : Type u} [category_theory.category C] (P Q : C) [category_theory.limits.has_binary_product P Q] [category_theory.limits.has_binary_product Q P] :
category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst ≫ category_theory.limits.prod.lift category_theory.limits.prod.snd category_theory.limits.prod.fst = 𝟙 (P ⨯ Q)
source
theorem category_theory.limits.prod.symmetry_assoc {C : Type u} [category_theory.category C] (P Q : C) [category_theory.limits.has_binary_product P Q] [category_theory.limits.has_binary_product Q P] {X' : C} (f' : P ⨯ Q ⟶ X') :
(category_theory.limits.prod.braiding P Q).hom ≫ (category_theory.limits.prod.braiding Q P).hom ≫ f' = f'
source
theorem category_theory.limits.prod.symmetry {C : Type u} [category_theory.category C] (P Q : C) [category_theory.limits.has_binary_product P Q] [category_theory.limits.has_binary_product Q P] :
(category_theory.limits.prod.braiding P Q).hom ≫ (category_theory.limits.prod.braiding Q P).hom = 𝟙 (P ⨯ Q)

The braiding isomorphism is symmetric.

source
noncomputable def category_theory.limits.prod.associator {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] (P Q R : C) :
P ⨯ Q ⨯ R ≅ P ⨯ (Q ⨯ R)

The associator isomorphism for binary products.

Equations
source
@[simp]
theorem category_theory.limits.prod.associator_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] (P Q R : C) :
(category_theory.limits.prod.associator P Q R).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)
source
@[simp]
theorem category_theory.limits.prod.associator_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] (P Q R : C) :
(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)
source
theorem category_theory.limits.prod.pentagon {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] (W X Y Z : C) :
category_theory.limits.prod.map (category_theory.limits.prod.associator W X Y).hom (𝟙 Z) ≫ (category_theory.limits.prod.associator W (X ⨯ Y) Z).hom ≫ category_theory.limits.prod.map (𝟙 W) (category_theory.limits.prod.associator X Y Z).hom = (category_theory.limits.prod.associator (W ⨯ X) Y Z).hom ≫ (category_theory.limits.prod.associator W X (Y ⨯ Z)).hom
source
theorem category_theory.limits.prod.pentagon_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] (W X Y Z : C) {X' : C} (f' : W ⨯ (X ⨯ (Y ⨯ Z)) ⟶ X') :
category_theory.limits.prod.map (category_theory.limits.prod.associator W X Y).hom (𝟙 Z) ≫ (category_theory.limits.prod.associator W (X ⨯ Y) Z).hom ≫ category_theory.limits.prod.map (𝟙 W) (category_theory.limits.prod.associator X Y Z).hom ≫ f' = (category_theory.limits.prod.associator (W ⨯ X) Y Z).hom ≫ (category_theory.limits.prod.associator W X (Y ⨯ Z)).hom ≫ f'
source
theorem category_theory.limits.prod.associator_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) {X' : C} (f' : Y₁ ⨯ (Y₂ ⨯ Y₃) ⟶ X') :
category_theory.limits.prod.map (category_theory.limits.prod.map f₁ f₂) f₃ ≫ (category_theory.limits.prod.associator Y₁ Y₂ Y₃).hom ≫ f' = (category_theory.limits.prod.associator X₁ X₂ X₃).hom ≫ category_theory.limits.prod.map f₁ (category_theory.limits.prod.map f₂ f₃) ≫ f'
source
theorem category_theory.limits.prod.associator_naturality {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
category_theory.limits.prod.map (category_theory.limits.prod.map f₁ f₂) f₃ ≫ (category_theory.limits.prod.associator Y₁ Y₂ Y₃).hom = (category_theory.limits.prod.associator X₁ X₂ X₃).hom ≫ category_theory.limits.prod.map f₁ (category_theory.limits.prod.map f₂ f₃)
source
noncomputable def category_theory.limits.prod.left_unitor {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) [category_theory.limits.has_binary_product (⊤_ C) P] :
⊤_ C ⨯ P ≅ P

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

Equations
source
@[simp]
theorem category_theory.limits.prod.left_unitor_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) [category_theory.limits.has_binary_product (⊤_ C) P] :
(category_theory.limits.prod.left_unitor P).hom = category_theory.limits.prod.snd
source
@[simp]
theorem category_theory.limits.prod.left_unitor_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) [category_theory.limits.has_binary_product (⊤_ C) P] :
(category_theory.limits.prod.left_unitor P).inv = category_theory.limits.prod.lift (category_theory.limits.terminal.from P) (𝟙 P)
source
@[simp]
theorem category_theory.limits.prod.right_unitor_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) [category_theory.limits.has_binary_product P (⊤_ C)] :
(category_theory.limits.prod.right_unitor P).inv = category_theory.limits.prod.lift (𝟙 P) (category_theory.limits.terminal.from P)
source
noncomputable def category_theory.limits.prod.right_unitor {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) [category_theory.limits.has_binary_product P (⊤_ C)] :
P ⨯ ⊤_ C ≅ P

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

Equations
source
@[simp]
theorem category_theory.limits.prod.right_unitor_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] (P : C) [category_theory.limits.has_binary_product P (⊤_ C)] :
(category_theory.limits.prod.right_unitor P).hom = category_theory.limits.prod.fst
source
theorem category_theory.limits.prod.left_unitor_hom_naturality_assoc {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_terminal C] [category_theory.limits.has_binary_products C] (f : X ⟶ Y) {X' : C} (f' : Y ⟶ X') :
category_theory.limits.prod.map (𝟙 (⊤_ C)) f ≫ (category_theory.limits.prod.left_unitor Y).hom ≫ f' = (category_theory.limits.prod.left_unitor X).hom ≫ f ≫ f'
source
theorem category_theory.limits.prod.left_unitor_hom_naturality {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_terminal C] [category_theory.limits.has_binary_products C] (f : X ⟶ Y) :
category_theory.limits.prod.map (𝟙 (⊤_ C)) f ≫ (category_theory.limits.prod.left_unitor Y).hom = (category_theory.limits.prod.left_unitor X).hom ≫ f
source
theorem category_theory.limits.prod.left_unitor_inv_naturality {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_terminal C] [category_theory.limits.has_binary_products C] (f : X ⟶ Y) :
(category_theory.limits.prod.left_unitor X).inv ≫ category_theory.limits.prod.map (𝟙 (⊤_ C)) f = f ≫ (category_theory.limits.prod.left_unitor Y).inv
source
theorem category_theory.limits.prod.left_unitor_inv_naturality_assoc {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_terminal C] [category_theory.limits.has_binary_products C] (f : X ⟶ Y) {X' : C} (f' : ⊤_ C ⨯ Y ⟶ X') :
(category_theory.limits.prod.left_unitor X).inv ≫ category_theory.limits.prod.map (𝟙 (⊤_ C)) f ≫ f' = f ≫ (category_theory.limits.prod.left_unitor Y).inv ≫ f'
source
theorem category_theory.limits.prod.right_unitor_hom_naturality {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_terminal C] [category_theory.limits.has_binary_products C] (f : X ⟶ Y) :
category_theory.limits.prod.map f (𝟙 (⊤_ C)) ≫ (category_theory.limits.prod.right_unitor Y).hom = (category_theory.limits.prod.right_unitor X).hom ≫ f
source
theorem category_theory.limits.prod.right_unitor_hom_naturality_assoc {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_terminal C] [category_theory.limits.has_binary_products C] (f : X ⟶ Y) {X' : C} (f' : Y ⟶ X') :
category_theory.limits.prod.map f (𝟙 (⊤_ C)) ≫ (category_theory.limits.prod.right_unitor Y).hom ≫ f' = (category_theory.limits.prod.right_unitor X).hom ≫ f ≫ f'
source
theorem category_theory.limits.prod_right_unitor_inv_naturality_assoc {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_terminal C] [category_theory.limits.has_binary_products C] (f : X ⟶ Y) {X' : C} (f' : Y ⨯ ⊤_ C ⟶ X') :
(category_theory.limits.prod.right_unitor X).inv ≫ category_theory.limits.prod.map f (𝟙 (⊤_ C)) ≫ f' = f ≫ (category_theory.limits.prod.right_unitor Y).inv ≫ f'
source
theorem category_theory.limits.prod_right_unitor_inv_naturality {C : Type u} [category_theory.category C] {X Y : C} [category_theory.limits.has_terminal C] [category_theory.limits.has_binary_products C] (f : X ⟶ Y) :
(category_theory.limits.prod.right_unitor X).inv ≫ category_theory.limits.prod.map f (𝟙 (⊤_ C)) = f ≫ (category_theory.limits.prod.right_unitor Y).inv
source
theorem category_theory.limits.prod.triangle {C : Type u} [category_theory.category C] [category_theory.limits.has_terminal C] [category_theory.limits.has_binary_products C] (X Y : C) :
(category_theory.limits.prod.associator X (⊤_ C) Y).hom ≫ category_theory.limits.prod.map (𝟙 X) (category_theory.limits.prod.left_unitor Y).hom = category_theory.limits.prod.map (category_theory.limits.prod.right_unitor X).hom (𝟙 Y)
source
@[simp]
theorem category_theory.limits.coprod.braiding_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (P Q : C) :
(category_theory.limits.coprod.braiding P Q).inv = category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl
source
@[simp]
theorem category_theory.limits.coprod.braiding_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (P Q : C) :
(category_theory.limits.coprod.braiding P Q).hom = category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl
source
noncomputable def category_theory.limits.coprod.braiding {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (P Q : C) :
P ⨿ Q ≅ Q ⨿ P

The braiding isomorphism which swaps a binary coproduct.

Equations
source
theorem category_theory.limits.coprod.symmetry' {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (P Q : C) :
category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl = 𝟙 (P ⨿ Q)
source
theorem category_theory.limits.coprod.symmetry'_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (P Q : C) {X' : C} (f' : P ⨿ Q ⟶ X') :
category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl ≫ f' = f'
source
theorem category_theory.limits.coprod.symmetry {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (P Q : C) :
(category_theory.limits.coprod.braiding P Q).hom ≫ (category_theory.limits.coprod.braiding Q P).hom = 𝟙 (P ⨿ Q)

The braiding isomorphism is symmetric.

source
@[simp]
theorem category_theory.limits.coprod.associator_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (P Q R : C) :
(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)
source
@[simp]
theorem category_theory.limits.coprod.associator_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (P Q R : C) :
(category_theory.limits.coprod.associator P Q R).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)
source
noncomputable def category_theory.limits.coprod.associator {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (P Q R : C) :
P ⨿ Q ⨿ R ≅ P ⨿ (Q ⨿ R)

The associator isomorphism for binary coproducts.

Equations
source
theorem category_theory.limits.coprod.pentagon {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (W X Y Z : C) :
category_theory.limits.coprod.map (category_theory.limits.coprod.associator W X Y).hom (𝟙 Z) ≫ (category_theory.limits.coprod.associator W (X ⨿ Y) Z).hom ≫ category_theory.limits.coprod.map (𝟙 W) (category_theory.limits.coprod.associator X Y Z).hom = (category_theory.limits.coprod.associator (W ⨿ X) Y Z).hom ≫ (category_theory.limits.coprod.associator W X (Y ⨿ Z)).hom
source
theorem category_theory.limits.coprod.associator_naturality {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
category_theory.limits.coprod.map (category_theory.limits.coprod.map f₁ f₂) f₃ ≫ (category_theory.limits.coprod.associator Y₁ Y₂ Y₃).hom = (category_theory.limits.coprod.associator X₁ X₂ X₃).hom ≫ category_theory.limits.coprod.map f₁ (category_theory.limits.coprod.map f₂ f₃)
source
@[simp]
theorem category_theory.limits.coprod.left_unitor_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] [category_theory.limits.has_initial C] (P : C) :
(category_theory.limits.coprod.left_unitor P).hom = category_theory.limits.coprod.desc (category_theory.limits.initial.to P) (𝟙 P)
source
noncomputable def category_theory.limits.coprod.left_unitor {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] [category_theory.limits.has_initial C] (P : C) :
⊥_ C ⨿ P ≅ P

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

Equations
source
@[simp]
theorem category_theory.limits.coprod.left_unitor_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] [category_theory.limits.has_initial C] (P : C) :
(category_theory.limits.coprod.left_unitor P).inv = category_theory.limits.coprod.inr
source
noncomputable def category_theory.limits.coprod.right_unitor {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] [category_theory.limits.has_initial C] (P : C) :
P ⨿ ⊥_ C ≅ P

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

Equations
source
@[simp]
theorem category_theory.limits.coprod.right_unitor_hom {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] [category_theory.limits.has_initial C] (P : C) :
(category_theory.limits.coprod.right_unitor P).hom = category_theory.limits.coprod.desc (𝟙 P) (category_theory.limits.initial.to P)
source
@[simp]
theorem category_theory.limits.coprod.right_unitor_inv {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] [category_theory.limits.has_initial C] (P : C) :
(category_theory.limits.coprod.right_unitor P).inv = category_theory.limits.coprod.inl
source
theorem category_theory.limits.coprod.triangle {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] [category_theory.limits.has_initial C] (X Y : C) :
(category_theory.limits.coprod.associator X (⊥_ C) Y).hom ≫ category_theory.limits.coprod.map (𝟙 X) (category_theory.limits.coprod.left_unitor Y).hom = category_theory.limits.coprod.map (category_theory.limits.coprod.right_unitor X).hom (𝟙 Y)
source
@[simp]
theorem category_theory.limits.prod.functor_obj_obj {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] (X Y : C) :
(category_theory.limits.prod.functor.obj X).obj Y = (X ⨯ Y)
source
@[simp]
theorem category_theory.limits.prod.functor_obj_map {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] (X Y Z : C) (g : Y ⟶ Z) :
(category_theory.limits.prod.functor.obj X).map g = category_theory.limits.prod.map (𝟙 X) g
source
@[simp]
theorem category_theory.limits.prod.functor_map_app {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] (Y Z : C) (f : Y ⟶ Z) (T : C) :
(category_theory.limits.prod.functor.map f).app T = category_theory.limits.prod.map f (𝟙 T)
source
noncomputable def category_theory.limits.prod.functor {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] :
C ⥤ C ⥤ C

The binary product functor.

Equations
source
noncomputable def category_theory.limits.prod.functor_left_comp {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] (X Y : C) :
category_theory.limits.prod.functor.obj (X ⨯ Y) ≅ category_theory.limits.prod.functor.obj Y ⋙ category_theory.limits.prod.functor.obj X

The product functor can be decomposed.

Equations
source
@[simp]
theorem category_theory.limits.coprod.functor_obj_obj {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (X Y : C) :
(category_theory.limits.coprod.functor.obj X).obj Y = (X ⨿ Y)
source
noncomputable def category_theory.limits.coprod.functor {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] :
C ⥤ C ⥤ C

The binary coproduct functor.

Equations
source
@[simp]
theorem category_theory.limits.coprod.functor_obj_map {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (X Y Z : C) (g : Y ⟶ Z) :
(category_theory.limits.coprod.functor.obj X).map g = category_theory.limits.coprod.map (𝟙 X) g
source
@[simp]
theorem category_theory.limits.coprod.functor_map_app {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (Y Z : C) (f : Y ⟶ Z) (T : C) :
(category_theory.limits.coprod.functor.map f).app T = category_theory.limits.coprod.map f (𝟙 T)
source
noncomputable def category_theory.limits.coprod.functor_left_comp {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_coproducts C] (X Y : C) :
category_theory.limits.coprod.functor.obj (X ⨿ Y) ≅ category_theory.limits.coprod.functor.obj Y ⋙ category_theory.limits.coprod.functor.obj X

The coproduct functor can be decomposed.

Equations
source
noncomputable def category_theory.limits.prod_comparison {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (A B : C) [category_theory.limits.has_binary_product A B] [category_theory.limits.has_binary_product (F.obj A) (F.obj B)] :
F.obj (A ⨯ B) ⟶ F.obj A ⨯ F.obj B

The product comparison morphism.

In category_theory/limits/preserves we show this is always an iso iff F preserves binary products.

Equations
Instances for category_theory.limits.prod_comparison
source
@[simp]
theorem category_theory.limits.prod_comparison_fst_assoc {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) {A B : C} [category_theory.limits.has_binary_product A B] [category_theory.limits.has_binary_product (F.obj A) (F.obj B)] {X' : D} (f' : F.obj A ⟶ X') :
category_theory.limits.prod_comparison F A B ≫ category_theory.limits.prod.fst ≫ f' = F.map category_theory.limits.prod.fst ≫ f'
source
@[simp]
theorem category_theory.limits.prod_comparison_fst {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) {A B : C} [category_theory.limits.has_binary_product A B] [category_theory.limits.has_binary_product (F.obj A) (F.obj B)] :
category_theory.limits.prod_comparison F A B ≫ category_theory.limits.prod.fst = F.map category_theory.limits.prod.fst
source
@[simp]
theorem category_theory.limits.prod_comparison_snd_assoc {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) {A B : C} [category_theory.limits.has_binary_product A B] [category_theory.limits.has_binary_product (F.obj A) (F.obj B)] {X' : D} (f' : F.obj B ⟶ X') :
category_theory.limits.prod_comparison F A B ≫ category_theory.limits.prod.snd ≫ f' = F.map category_theory.limits.prod.snd ≫ f'
source
@[simp]
theorem category_theory.limits.prod_comparison_snd {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) {A B : C} [category_theory.limits.has_binary_product A B] [category_theory.limits.has_binary_product (F.obj A) (F.obj B)] :
category_theory.limits.prod_comparison F A B ≫ category_theory.limits.prod.snd = F.map category_theory.limits.prod.snd
source
theorem category_theory.limits.prod_comparison_natural_assoc {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) {A A' B B' : C} [category_theory.limits.has_binary_product A B] [category_theory.limits.has_binary_product A' B'] [category_theory.limits.has_binary_product (F.obj A) (F.obj B)] [category_theory.limits.has_binary_product (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {X' : D} (f' : F.obj A' ⨯ F.obj B' ⟶ X') :
F.map (category_theory.limits.prod.map f g) ≫ category_theory.limits.prod_comparison F A' B' ≫ f' = category_theory.limits.prod_comparison F A B ≫ category_theory.limits.prod.map (F.map f) (F.map g) ≫ f'
source
theorem category_theory.limits.prod_comparison_natural {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) {A A' B B' : C} [category_theory.limits.has_binary_product A B] [category_theory.limits.has_binary_product A' B'] [category_theory.limits.has_binary_product (F.obj A) (F.obj B)] [category_theory.limits.has_binary_product (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') :
F.map (category_theory.limits.prod.map f g) ≫ category_theory.limits.prod_comparison F A' B' = category_theory.limits.prod_comparison F A B ≫ category_theory.limits.prod.map (F.map f) (F.map g)

Naturality of the prod_comparison morphism in both arguments.

source
noncomputable def category_theory.limits.prod_comparison_nat_trans {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_binary_products C] [category_theory.limits.has_binary_products D]