Binary (co)products
We define a category walking_pair, which is the index category
for a binary (co)product diagram. A convenience method pair X Y
constructs the functor from the walking pair, hitting the given objects.
We define prod X Y and coprod X Y as limits and colimits of such functors.
Typeclasses has_binary_products and has_binary_coproducts assert the existence
of (co)limits shaped as walking pairs.
We include lemmas for simplifying equations involving projections and coprojections, and define braiding and associating isomorphisms, and the product comparison morphism.
The type of objects for the diagram indexing a binary (co)product.
The equivalence swapping left and right.
Equations
- category_theory.limits.walking_pair.swap = {to_fun := λ (j : category_theory.limits.walking_pair), j.rec_on category_theory.limits.walking_pair.right category_theory.limits.walking_pair.left, inv_fun := λ (j : category_theory.limits.walking_pair), j.rec_on category_theory.limits.walking_pair.right category_theory.limits.walking_pair.left, left_inv := category_theory.limits.walking_pair.swap._proof_1, right_inv := category_theory.limits.walking_pair.swap._proof_2}
An equivalence from walking_pair to bool, sometimes useful when reindexing limits.
Equations
- category_theory.limits.walking_pair.equiv_bool = {to_fun := λ (j : category_theory.limits.walking_pair), j.rec_on bool.tt bool.ff, inv_fun := λ (b : bool), b.rec_on category_theory.limits.walking_pair.right category_theory.limits.walking_pair.left, left_inv := category_theory.limits.walking_pair.equiv_bool._proof_1, right_inv := category_theory.limits.walking_pair.equiv_bool._proof_2}
The diagram on the walking pair, sending the two points to X and Y.
Equations
- category_theory.limits.pair X Y = category_theory.discrete.functor (λ (j : category_theory.limits.walking_pair), j.cases_on X Y)
@[simp]
theorem
category_theory.limits.pair_obj_left
{C : Type u}
[category_theory.category C]
(X Y : C) :
@[simp]
theorem
category_theory.limits.pair_obj_right
{C : Type u}
[category_theory.category C]
(X Y : C) :
def
category_theory.limits.map_pair
{C : Type u}
[category_theory.category C]
{F G : category_theory.discrete category_theory.limits.walking_pair ⥤ C} :
The natural transformation between two functors out of the walking pair, specified by its components.
Equations
- category_theory.limits.map_pair f g = {app := λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.map_pair._match_1 f g j, naturality' := _}
- category_theory.limits.map_pair._match_1 f g category_theory.limits.walking_pair.right = g
- category_theory.limits.map_pair._match_1 f g category_theory.limits.walking_pair.left = f
@[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 category_theory.limits.walking_pair.left ⟶ G.obj category_theory.limits.walking_pair.left)
(g : F.obj category_theory.limits.walking_pair.right ⟶ G.obj category_theory.limits.walking_pair.right) :
@[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 category_theory.limits.walking_pair.left ⟶ G.obj category_theory.limits.walking_pair.left)
(g : F.obj category_theory.limits.walking_pair.right ⟶ G.obj category_theory.limits.walking_pair.right) :
@[simp]
theorem
category_theory.limits.map_pair_iso_inv
{C : Type u}
[category_theory.category C]
{F G : category_theory.discrete category_theory.limits.walking_pair ⥤ C}
(f : F.obj category_theory.limits.walking_pair.left ≅ G.obj category_theory.limits.walking_pair.left)
(g : F.obj category_theory.limits.walking_pair.right ≅ G.obj category_theory.limits.walking_pair.right) :
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} :
The natural isomorphism between two functors out of the walking pair, specified by its components.
Equations
- category_theory.limits.map_pair_iso f g = {hom := category_theory.limits.map_pair f.hom g.hom, inv := category_theory.limits.map_pair f.inv g.inv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.map_pair_iso_hom
{C : Type u}
[category_theory.category C]
{F G : category_theory.discrete category_theory.limits.walking_pair ⥤ C}
(f : F.obj category_theory.limits.walking_pair.left ≅ G.obj category_theory.limits.walking_pair.left)
(g : F.obj category_theory.limits.walking_pair.right ≅ G.obj category_theory.limits.walking_pair.right) :
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).
def
category_theory.limits.diagram_iso_pair
{C : Type u}
[category_theory.category C]
(F : category_theory.discrete category_theory.limits.walking_pair ⥤ C) :
Every functor out of the walking pair is naturally isomorphic (actually, equal) to a pair
def
category_theory.limits.binary_fan
{C : Type u}
[category_theory.category C] :
C → C → Type (max u v)
A binary fan is just a cone on a diagram indexing a product.
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) :
The first projection of a binary fan.
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) :
The second projection of a binary fan.
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} :
def
category_theory.limits.binary_cofan
{C : Type u}
[category_theory.category C] :
C → C → Type (max u v)
A binary cofan is just a cocone on a diagram indexing a coproduct.
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) :
The first inclusion of a binary cofan.
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) :
The second inclusion of a binary cofan.
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} :
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
- category_theory.limits.binary_fan.mk π₁ π₂ = {X := P, π := {app := λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on j π₁ π₂, naturality' := _}}
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
- category_theory.limits.binary_cofan.mk ι₁ ι₂ = {X := P, ι := {app := λ (j : category_theory.discrete category_theory.limits.walking_pair), category_theory.limits.walking_pair.cases_on j ι₁ ι₂, naturality' := _}}
@[simp]
theorem
category_theory.limits.binary_fan.mk_π_app_left
{C : Type u}
[category_theory.category C]
{X Y P : C}
(π₁ : P ⟶ X)
(π₂ : P ⟶ Y) :
@[simp]
theorem
category_theory.limits.binary_fan.mk_π_app_right
{C : Type u}
[category_theory.category C]
{X Y P : C}
(π₁ : P ⟶ X)
(π₂ : P ⟶ Y) :
@[simp]
theorem
category_theory.limits.binary_cofan.mk_ι_app_left
{C : Type u}
[category_theory.category C]
{X Y P : C}
(ι₁ : X ⟶ P)
(ι₂ : Y ⟶ P) :
@[simp]
theorem
category_theory.limits.binary_cofan.mk_ι_app_right
{C : Type u}
[category_theory.category C]
{X Y P : C}
(ι₁ : X ⟶ P)
(ι₂ : Y ⟶ P) :
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) :
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
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) :
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
def
category_theory.limits.has_binary_product
{C : Type u}
[category_theory.category C] :
C → C → Type (max u v)
An abbreviation for has_limit (pair X Y).
Instances
def
category_theory.limits.has_binary_coproduct
{C : Type u}
[category_theory.category C] :
C → C → Type (max u v)
An abbreviation for has_colimit (pair X Y).
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 chosen a product of X and Y, we can access it using prod X Y or
X ⨯ Y.
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 chosen a coproduct of X and Y, we can access it using coprod X Y or
X ⨿ Y.
def
category_theory.limits.prod.fst
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_product X Y] :
The projection map to the first component of the product.
def
category_theory.limits.prod.snd
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_product X Y] :
The projecton map to the second component of the product.
def
category_theory.limits.coprod.inl
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_coproduct X Y] :
The inclusion map from the first component of the coproduct.
def
category_theory.limits.coprod.inr
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_coproduct X Y] :
The inclusion map from the second component of the coproduct.
@[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} :
@[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} :
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] :
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.
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] :
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.
@[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'
@[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) :
@[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'
@[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) :
@[simp]
theorem
category_theory.limits.prod.lift_comp_comp
{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) :
category_theory.limits.prod.lift (f ≫ g) (f ≫ h) = f ≫ category_theory.limits.prod.lift g h
theorem
category_theory.limits.prod.lift_comp_comp_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') :
category_theory.limits.prod.lift (f ≫ g) (f ≫ h) ≫ f' = f ≫ category_theory.limits.prod.lift g h ≫ f'
@[simp]
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') :
@[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) :
@[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) :
@[simp]
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') :
@[simp]
theorem
category_theory.limits.coprod.desc_comp_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 ≫ f) (h ≫ f) = category_theory.limits.coprod.desc g h ≫ f
theorem
category_theory.limits.coprod.desc_comp_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 ≫ f) (h ≫ f) ≫ f' = category_theory.limits.coprod.desc g h ≫ f ≫ f'
@[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] :
Equations
- _ = _
@[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] :
Equations
- _ = _
@[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] :
Equations
- _ = _
@[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] :
Equations
- _ = _
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
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
def
category_theory.limits.prod.map
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] :
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.
def
category_theory.limits.prod.map_iso
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] :
If the products W ⨯ X and Y ⨯ Z exist, then every pair of isomorphisms f : W ≅ Y and
g : X ≅ Z induces a isomorphism prod.map_iso f g : W ⨯ X ≅ Y ⨯ Z.
@[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_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
(f : W ≅ Y)
(g : X ≅ Z) :
@[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_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
(f : W ≅ Y)
(g : X ≅ Z) :
def
category_theory.limits.coprod.map
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] :
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.
def
category_theory.limits.coprod.map_iso
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C] :
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.
@[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_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
(f : W ≅ Y)
(g : X ≅ Z) :
@[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_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
(f : W ≅ Y)
(g : X ≅ Z) :
theorem
category_theory.limits.prod.map_fst_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z)
{X' : C}
(f' : Y ⟶ X') :
theorem
category_theory.limits.prod.map_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z) :
theorem
category_theory.limits.prod.map_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z) :
theorem
category_theory.limits.prod.map_snd_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z)
{X' : C}
(f' : Z ⟶ X') :
@[simp]
theorem
category_theory.limits.prod_map_id_id
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{X Y : C} :
@[simp]
theorem
category_theory.limits.prod_lift_fst_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{X Y : C} :
theorem
category_theory.limits.prod_map_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{A B X Y : C}
(f : A ⟶ B)
(g : X ⟶ Y) :
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
theorem
category_theory.limits.prod_map_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{A B X Y : C}
(f : A ⟶ B)
(g : X ⟶ Y)
{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'
theorem
category_theory.limits.prod_map_comp_id_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 Y Z W : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
{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'
theorem
category_theory.limits.prod_map_comp_id
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{X Y Z W : C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
category_theory.limits.prod.map (f ≫ g) (𝟙 W) = category_theory.limits.prod.map f (𝟙 W) ≫ category_theory.limits.prod.map g (𝟙 W)
theorem
category_theory.limits.prod_map_id_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 Y Z W : C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
category_theory.limits.prod.map (𝟙 W) (f ≫ g) = category_theory.limits.prod.map (𝟙 W) f ≫ category_theory.limits.prod.map (𝟙 W) g
theorem
category_theory.limits.prod_map_id_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 Y Z W : C}
(f : X ⟶ Y)
(g : Y ⟶ 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'
theorem
category_theory.limits.prod.lift_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
(V W X Y Z : C)
(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)
theorem
category_theory.limits.prod.lift_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
(V W X Y Z : C)
(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'
theorem
category_theory.limits.coprod.inl_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z) :
theorem
category_theory.limits.coprod.inl_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z)
{X' : C}
(f' : Y ⨿ Z ⟶ X') :
theorem
category_theory.limits.coprod.inr_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z)
{X' : C}
(f' : Y ⨿ Z ⟶ X') :
theorem
category_theory.limits.coprod.inr_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{W X Y Z : C}
(f : W ⟶ Y)
(g : X ⟶ Z) :
@[simp]
theorem
category_theory.limits.coprod_map_id_id
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{X Y : C} :
@[simp]
theorem
category_theory.limits.coprod_desc_inl_inr
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{X Y : C} :
theorem
category_theory.limits.coprod_map_map_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{A B X Y : C}
(f : A ⟶ B)
(g : X ⟶ Y)
{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'
theorem
category_theory.limits.coprod_map_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{A B X Y : C}
(f : A ⟶ B)
(g : X ⟶ Y) :
theorem
category_theory.limits.coprod_map_comp_id
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{X Y Z W : C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
category_theory.limits.coprod.map (f ≫ g) (𝟙 W) = category_theory.limits.coprod.map f (𝟙 W) ≫ category_theory.limits.coprod.map g (𝟙 W)
theorem
category_theory.limits.coprod_map_comp_id_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 Y Z W : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
{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'
theorem
category_theory.limits.coprod_map_id_comp_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 Y Z W : C}
(f : X ⟶ Y)
(g : Y ⟶ 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'
theorem
category_theory.limits.coprod_map_id_comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{X Y Z W : C}
(f : X ⟶ Y)
(g : Y ⟶ Z) :
category_theory.limits.coprod.map (𝟙 W) (f ≫ g) = category_theory.limits.coprod.map (𝟙 W) f ≫ category_theory.limits.coprod.map (𝟙 W) g
theorem
category_theory.limits.coprod.map_desc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{S T U V W : C}
(f : U ⟶ S)
(g : W ⟶ S)
(h : T ⟶ U)
(k : V ⟶ W) :
theorem
category_theory.limits.coprod.map_desc_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) C]
{S T U V W : C}
(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'
def
category_theory.limits.has_binary_products
(C : Type u)
[category_theory.category C] :
Type (max u v)
has_binary_products represents a choice of product for every pair of objects.
def
category_theory.limits.has_binary_coproducts
(C : Type u)
[category_theory.category C] :
Type (max u v)
has_binary_coproducts represents a choice of coproduct for every pair of objects.
def
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)] :
If C has all limits of diagrams pair X Y, then it has all binary products
def
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)] :
If C has all colimits of diagrams pair X Y, then it has all binary coproducts
@[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) :
@[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)
def
category_theory.limits.prod_functor
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C] :
The binary product functor.
Equations
- category_theory.limits.prod_functor = {obj := λ (X : C), {obj := λ (Y : C), X ⨯ Y, map := λ (Y Z : C), category_theory.limits.prod.map (𝟙 X), map_id' := _, map_comp' := _}, map := λ (Y Z : C) (f : Y ⟶ Z), {app := λ (T : C), category_theory.limits.prod.map f (𝟙 T), naturality' := _}, map_id' := _, map_comp' := _}
@[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) :
def
category_theory.limits.prod_comparison
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
(A B : C) :
The product comparison morphism.
In category_theory/limits/preserves we show this is always an iso iff F preserves binary products.
theorem
category_theory.limits.prod_comparison_natural_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
{A A' B B' : C}
(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'
theorem
category_theory.limits.prod_comparison_natural
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
{A A' B B' : C}
(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.
theorem
category_theory.limits.inv_prod_comparison_map_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
(A B : C)
[category_theory.is_iso (category_theory.limits.prod_comparison F A B)] :
theorem
category_theory.limits.inv_prod_comparison_map_fst_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
(A B : C)
[category_theory.is_iso (category_theory.limits.prod_comparison F A B)]
{X' : D}
(f' : F.obj A ⟶ X') :
theorem
category_theory.limits.inv_prod_comparison_map_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
(A B : C)
[category_theory.is_iso (category_theory.limits.prod_comparison F A B)] :
theorem
category_theory.limits.inv_prod_comparison_map_snd_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
(A B : C)
[category_theory.is_iso (category_theory.limits.prod_comparison F A B)]
{X' : D}
(f' : F.obj B ⟶ X') :
theorem
category_theory.limits.prod_comparison_inv_natural
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
{A A' B B' : C}
(f : A ⟶ A')
(g : B ⟶ B')
[category_theory.is_iso (category_theory.limits.prod_comparison F A B)]
[category_theory.is_iso (category_theory.limits.prod_comparison F A' B')] :
If the product comparison morphism is an iso, its inverse is natural.
theorem
category_theory.limits.prod_comparison_inv_natural_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_products D]
(F : C ⥤ D)
{A A' B B' : C}
(f : A ⟶ A')
(g : B ⟶ B')
[category_theory.is_iso (category_theory.limits.prod_comparison F A B)]
[category_theory.is_iso (category_theory.limits.prod_comparison F A' B')]
{X' : D}
(f' : F.obj (A' ⨯ B') ⟶ X') :
category_theory.is_iso.inv (category_theory.limits.prod_comparison F A B) ≫ F.map (category_theory.limits.prod.map f g) ≫ f' = category_theory.limits.prod.map (F.map f) (F.map g) ≫ category_theory.is_iso.inv (category_theory.limits.prod_comparison F A' B') ≫ f'