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 #
@[protected, instance]
The type of objects for the diagram indexing a binary (co)product.
Instances for category_theory.limits.walking_pair
- category_theory.limits.walking_pair.has_sizeof_inst
- category_theory.limits.walking_pair.inhabited
- category_theory.limits.fintype_walking_pair
@[protected, instance]
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 function on the walking pair, sending the two points to X and Y.
Equations
- category_theory.limits.pair_function X Y = λ (j : category_theory.limits.walking_pair), j.cases_on X Y
@[simp]
@[simp]
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)
Instances for category_theory.limits.pair
- category_theory.limits.has_binary_biproduct.has_limit_pair
- category_theory.limits.has_binary_biproduct.has_colimit_pair
- category_theory.limits.has_binary_product_zero_left
- category_theory.limits.has_binary_product_zero_right
- category_theory.limits.has_binary_coproduct_zero_left
- category_theory.limits.has_binary_coproduct_zero_right
@[simp]
@[simp]
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
- category_theory.limits.map_pair f g = {app := λ (j : category_theory.discrete category_theory.limits.walking_pair), j.rec_on (λ (j : category_theory.limits.walking_pair), j.cases_on f g), naturality' := _}
@[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}) :
@[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}) :
@[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
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
- category_theory.limits.map_pair_iso f g = category_theory.nat_iso.of_components (λ (j : category_theory.discrete category_theory.limits.walking_pair), j.rec_on (λ (j : category_theory.limits.walking_pair), j.cases_on f g)) _
@[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
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
@[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
@[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
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
@[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.
@[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) :
The first projection of a binary fan.
@[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) :
The second projection of a binary fan.
@[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) :
@[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) :
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) :
A convenient way to show that a binary fan is a limit.
Equations
- category_theory.limits.binary_fan.is_limit.mk s lift hl₁ hl₂ uniq = {lift := λ (t : category_theory.limits.cone (category_theory.limits.pair X Y)), lift (category_theory.limits.binary_fan.fst t) (category_theory.limits.binary_fan.snd t), fac' := _, uniq' := _}
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
@[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.
@[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) :
The first inclusion of a binary cofan.
@[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) :
The second inclusion of a binary cofan.
@[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) :
@[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) :
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) :
A convenient way to show that a binary cofan is a colimit.
Equations
- category_theory.limits.binary_cofan.is_colimit.mk s desc hd₁ hd₂ uniq = {desc := λ (t : category_theory.limits.cocone (category_theory.limits.pair X Y)), desc (category_theory.limits.binary_cofan.inl t) (category_theory.limits.binary_cofan.inr t), fac' := _, uniq' := _}
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
@[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
def
category_theory.limits.binary_fan.mk
{C : Type u}
[category_theory.category C]
{X Y P : C}
(π₁ : P ⟶ X)
(π₂ : P ⟶ 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), j.rec_on (λ (j : category_theory.limits.walking_pair), j.cases_on π₁ π₂), naturality' := _}}
@[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
def
category_theory.limits.binary_cofan.mk
{C : Type u}
[category_theory.category C]
{X Y P : C}
(ι₁ : X ⟶ P)
(ι₂ : Y ⟶ P) :
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), j.rec_on (λ (j : category_theory.limits.walking_pair), j.cases_on ι₁ ι₂), naturality' := _}}
@[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 = π₁
@[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 = π₂
@[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 = ι₁
@[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 = ι₂
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) :
Every binary_fan is isomorphic to an application of binary_fan.mk.
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) :
Every binary_fan is isomorphic to an application of binary_fan.mk.
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) :
This is a more convenient formulation to show that a binary_fan constructed using
binary_fan.mk is a limit cone.
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) :
This is a more convenient formulation to show that a binary_cofan constructed using
binary_cofan.mk is a colimit cocone.
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
@[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) :
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
@[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) :
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) :
Binary products are symmetric.
Equations
- category_theory.limits.binary_fan.is_limit_flip hc = category_theory.limits.binary_fan.is_limit_mk (λ (s : category_theory.limits.binary_fan ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.right}) ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.left})), hc.lift (category_theory.limits.binary_fan.mk s.snd s.fst)) _ _ _
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) :
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) :
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) :
If X' ≅ X, then X × Y also is the product of X' and Y.
Equations
- c.is_limit_comp_left_iso f h = category_theory.limits.binary_fan.is_limit_mk (λ (s : category_theory.limits.binary_fan X' ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.right})), h.lift (category_theory.limits.binary_fan.mk (s.fst ≫ category_theory.inv f) s.snd)) _ _ _
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) :
If Y' ≅ Y, then X x Y also is the product of X and Y'.
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) :
Binary coproducts are symmetric.
Equations
- category_theory.limits.binary_cofan.is_colimit_flip hc = category_theory.limits.binary_cofan.is_colimit_mk (λ (s : category_theory.limits.binary_cofan ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.right}) ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.left})), hc.desc (category_theory.limits.binary_cofan.mk s.inr s.inl)) _ _ _
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) :
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) :
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) :
If X' ≅ X, then X ⨿ Y also is the coproduct of X' and Y.
Equations
- c.is_colimit_comp_left_iso f h = category_theory.limits.binary_cofan.is_colimit_mk (λ (s : category_theory.limits.binary_cofan X' ((category_theory.limits.pair X Y).obj {as := category_theory.limits.walking_pair.right})), h.desc (category_theory.limits.binary_cofan.mk (category_theory.inv f ≫ s.inl) s.inr)) _ _ _
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) :
If Y' ≅ Y, then X ⨿ Y also is the coproduct of X and Y'.
@[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).
@[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).
@[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.
@[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.
@[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] :
The projection map to the first component of the product.
@[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] :
The projecton map to the second component of the product.
@[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] :
The inclusion map from the first component of the coproduct.
@[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] :
The inclusion map from the second component of the coproduct.
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] :
The binary fan constructed from the projection maps is a limit.
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] :
The binary cofan constructed from the coprojection maps is a colimit.
@[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
@[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
@[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) :
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.
@[reducible]
noncomputable
def
category_theory.limits.diag
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_product X X] :
diagonal arrow of the binary product in the category fam I
@[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) :
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.
@[reducible]
noncomputable
def
category_theory.limits.codiag
{C : Type u}
[category_theory.category C]
(X : C)
[category_theory.limits.has_binary_coproduct X X] :
codiagonal arrow of the binary coproduct
@[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
{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.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) :
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') :
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.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) :
@[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] :
@[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] :
@[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] :
@[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] :
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
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
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) :
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
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) :
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
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'
@[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)
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) :
@[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) :
@[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') :
@[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') :
@[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) :
@[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] :
@[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] :
@[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'
@[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)
@[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) :
@[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'
@[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)
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
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'
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'
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)
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
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'
@[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) :
@[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) :
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) :
If the products W ⨯ X and Y ⨯ Z exist, then every pair of isomorphisms f : W ≅ Y and
g : X ≅ Z induces an isomorphism prod.map_iso f g : W ⨯ X ≅ Y ⨯ Z.
Equations
- category_theory.limits.prod.map_iso f g = {hom := category_theory.limits.prod.map f.hom g.hom, inv := category_theory.limits.prod.map f.inv g.inv, hom_inv_id' := _, inv_hom_id' := _}
@[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] :
@[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] :
@[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] :
@[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'
@[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') :
@[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)] :
@[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') :
@[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) :
@[protected, instance]
@[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)
@[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'
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) :
@[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) :
@[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') :
@[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') :
@[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) :
@[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] :
@[simp]
@[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) :
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'
@[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) :
@[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'
@[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)
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] :
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'
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)
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'
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'
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
@[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) :
@[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) :
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) :
If the coproducts W ⨿ X and Y ⨿ Z exist, then every pair of isomorphisms f : W ≅ Y and
g : W ≅ Z induces a isomorphism coprod.map_iso f g : W ⨿ X ≅ Y ⨿ Z.
Equations
- category_theory.limits.coprod.map_iso f g = {hom := category_theory.limits.coprod.map f.hom g.hom, inv := category_theory.limits.coprod.map f.inv g.inv, hom_inv_id' := _, inv_hom_id' := _}
@[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] :
@[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] :
@[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] :
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') :
@[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)] :
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') :
@[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') :
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) :
@[reducible]
has_binary_products represents a choice of product for every pair of objects.
@[reducible]
has_binary_coproducts represents a choice of coproduct for every pair of objects.
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)] :
If C has all limits of diagrams pair X Y, then it has all binary products
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)] :
If C has all colimits of diagrams pair X Y, then it has all binary coproducts
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] :
The braiding isomorphism which swaps a binary product.
@[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] :
@[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] :
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') :
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) :
The braiding isomorphism can be passed through a map by swapping the order.
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') :
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] :
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'
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.
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) :
The associator isomorphism for binary products.
Equations
- category_theory.limits.prod.associator P Q R = {hom := category_theory.limits.prod.lift (category_theory.limits.prod.fst ≫ category_theory.limits.prod.fst) (category_theory.limits.prod.lift (category_theory.limits.prod.fst ≫ category_theory.limits.prod.snd) category_theory.limits.prod.snd), inv := category_theory.limits.prod.lift (category_theory.limits.prod.lift category_theory.limits.prod.fst (category_theory.limits.prod.snd ≫ category_theory.limits.prod.fst)) (category_theory.limits.prod.snd ≫ category_theory.limits.prod.snd), hom_inv_id' := _, inv_hom_id' := _}
@[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) :
@[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) :
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
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'
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'
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₃)
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] :
The left unitor isomorphism for binary products with the terminal object.
Equations
- category_theory.limits.prod.left_unitor P = {hom := category_theory.limits.prod.snd _inst_3, inv := category_theory.limits.prod.lift (category_theory.limits.terminal.from P) (𝟙 P), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
@[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] :
@[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)] :
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)] :
The right unitor isomorphism for binary products with the terminal object.
Equations
- category_theory.limits.prod.right_unitor P = {hom := category_theory.limits.prod.fst _inst_3, inv := category_theory.limits.prod.lift (𝟙 P) (category_theory.limits.terminal.from P), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
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'
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) :
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) :
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'
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) :
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'
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'
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) :
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) :
@[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) :
@[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) :
noncomputable
def
category_theory.limits.coprod.braiding
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q : C) :
The braiding isomorphism which swaps a binary coproduct.
Equations
- category_theory.limits.coprod.braiding P Q = {hom := category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl, inv := category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl, hom_inv_id' := _, inv_hom_id' := _}
theorem
category_theory.limits.coprod.symmetry'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q : C) :
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') :
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.
@[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)
@[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)
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) :
The associator isomorphism for binary coproducts.
Equations
- category_theory.limits.coprod.associator P Q R = {hom := category_theory.limits.coprod.desc (category_theory.limits.coprod.desc category_theory.limits.coprod.inl (category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.inr)) (category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.inr), inv := category_theory.limits.coprod.desc (category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.inl) (category_theory.limits.coprod.desc (category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.inl) category_theory.limits.coprod.inr), hom_inv_id' := _, inv_hom_id' := _}
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
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₃) :
@[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) :
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) :
The left unitor isomorphism for binary coproducts with the initial object.
Equations
@[simp]
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) :
The right unitor isomorphism for binary coproducts with the initial object.
Equations
@[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) :
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) :
@[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)
@[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) :
@[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) :
noncomputable
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' := _}
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) :
The product functor can be decomposed.
@[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)
noncomputable
def
category_theory.limits.coprod.functor
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C] :
The binary coproduct functor.
Equations
- category_theory.limits.coprod.functor = {obj := λ (X : C), {obj := λ (Y : C), X ⨿ Y, map := λ (Y Z : C), category_theory.limits.coprod.map (𝟙 X), map_id' := _, map_comp' := _}, map := λ (Y Z : C) (f : Y ⟶ Z), {app := λ (T : C), category_theory.limits.coprod.map f (𝟙 T), naturality' := _}, map_id' := _, map_comp' := _}
@[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) :
@[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) :
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) :
The coproduct functor can be decomposed.
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)] :
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
@[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') :
@[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)] :
@[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') :
@[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)] :
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'
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.
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]
(F : C ⥤ D)
(A : C) :
The product comparison morphism from F(A ⨯ -) to FA ⨯ F-, whose components are given by
prod_comparison.
Equations
- category_theory.limits.prod_comparison_nat_trans F A = {app := λ (B : C), category_theory.limits.prod_comparison F A B, naturality' := _}
@[simp]
theorem
category_theory.limits.prod_comparison_nat_trans_app
{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]
(F : C ⥤ D)
(A B : C) :
theorem
category_theory.limits.inv_prod_comparison_map_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)]
[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_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.is_iso (category_theory.limits.prod_comparison F A B)] :
theorem
category_theory.limits.inv_prod_comparison_map_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.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]
{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.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]
{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')
[category_theory.is_iso (category_theory.limits.prod_comparison F A B)]
[category_theory.is_iso (category_theory.limits.prod_comparison F A' B')] :
category_theory.inv (category_theory.limits.prod_comparison F A B) ≫ F.map (category_theory.limits.prod.map f g) = category_theory.limits.prod.map (F.map f) (F.map g) ≫ category_theory.inv (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]
{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')
[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.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.inv (category_theory.limits.prod_comparison F A' B') ≫ f'
@[simp]
theorem
category_theory.limits.prod_comparison_nat_iso_hom_app
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_binary_products D]
(A : C)
[∀ (B : C), category_theory.is_iso (category_theory.limits.prod_comparison F A B)]
(B : C) :
noncomputable
def
category_theory.limits.prod_comparison_nat_iso
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_binary_products D]
(A : C)
[∀ (B : C), category_theory.is_iso (category_theory.limits.prod_comparison F A B)] :
The natural isomorphism F(A ⨯ -) ≅ FA ⨯ F-, provided each prod_comparison F A B is an
isomorphism (as B changes).
Equations
- category_theory.limits.prod_comparison_nat_iso F A = {hom := category_theory.limits.prod_comparison_nat_trans F A, inv := (category_theory.as_iso {app := λ (B : C), category_theory.limits.prod_comparison F A B, naturality' := _}).inv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.prod_comparison_nat_iso_inv
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_binary_products D]
(A : C)
[∀ (B : C), category_theory.is_iso (category_theory.limits.prod_comparison F A B)] :
(category_theory.limits.prod_comparison_nat_iso F A).inv = (category_theory.as_iso {app := λ (B : C), category_theory.limits.prod_comparison F A B, naturality' := _}).inv
noncomputable
def
category_theory.limits.coprod_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_coproduct A B]
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)] :
The coproduct comparison morphism.
In category_theory/limits/preserves we show
this is always an iso iff F preserves binary coproducts.
Equations
Instances for category_theory.limits.coprod_comparison
@[simp]
theorem
category_theory.limits.coprod_comparison_inl
{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_coproduct A B]
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)] :
@[simp]
theorem
category_theory.limits.coprod_comparison_inl_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_coproduct A B]
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
{X' : D}
(f' : F.obj (A ⨿ B) ⟶ X') :
@[simp]
theorem
category_theory.limits.coprod_comparison_inr_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_coproduct A B]
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
{X' : D}
(f' : F.obj (A ⨿ B) ⟶ X') :
@[simp]
theorem
category_theory.limits.coprod_comparison_inr
{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_coproduct A B]
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)] :
theorem
category_theory.limits.coprod_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_coproduct A B]
[category_theory.limits.has_binary_coproduct A' B']
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
[category_theory.limits.has_binary_coproduct (F.obj A') (F.obj B')]
(f : A ⟶ A')
(g : B ⟶ B')
{X' : D}
(f' : F.obj (A' ⨿ B') ⟶ X') :
category_theory.limits.coprod_comparison F A B ≫ F.map (category_theory.limits.coprod.map f g) ≫ f' = category_theory.limits.coprod.map (F.map f) (F.map g) ≫ category_theory.limits.coprod_comparison F A' B' ≫ f'
theorem
category_theory.limits.coprod_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_coproduct A B]
[category_theory.limits.has_binary_coproduct A' B']
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
[category_theory.limits.has_binary_coproduct (F.obj A') (F.obj B')]
(f : A ⟶ A')
(g : B ⟶ B') :
category_theory.limits.coprod_comparison F A B ≫ F.map (category_theory.limits.coprod.map f g) = category_theory.limits.coprod.map (F.map f) (F.map g) ≫ category_theory.limits.coprod_comparison F A' B'
Naturality of the coprod_comparison morphism in both arguments.
@[simp]
theorem
category_theory.limits.coprod_comparison_nat_trans_app
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_binary_coproducts D]
(F : C ⥤ D)
(A B : C) :
noncomputable
def
category_theory.limits.coprod_comparison_nat_trans
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_binary_coproducts D]
(F : C ⥤ D)
(A : C) :
The coproduct comparison morphism from FA ⨿ F- to F(A ⨿ -), whose components are given by
coprod_comparison.
Equations
- category_theory.limits.coprod_comparison_nat_trans F A = {app := λ (B : C), category_theory.limits.coprod_comparison F A B, naturality' := _}
theorem
category_theory.limits.map_inl_inv_coprod_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_coproduct A B]
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
[category_theory.is_iso (category_theory.limits.coprod_comparison F A B)] :
theorem
category_theory.limits.map_inl_inv_coprod_comparison_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_coproduct A B]
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
[category_theory.is_iso (category_theory.limits.coprod_comparison F A B)]
{X' : D}
(f' : F.obj A ⨿ F.obj B ⟶ X') :
theorem
category_theory.limits.map_inr_inv_coprod_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_coproduct A B]
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
[category_theory.is_iso (category_theory.limits.coprod_comparison F A B)] :
theorem
category_theory.limits.map_inr_inv_coprod_comparison_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_coproduct A B]
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
[category_theory.is_iso (category_theory.limits.coprod_comparison F A B)]
{X' : D}
(f' : F.obj A ⨿ F.obj B ⟶ X') :
theorem
category_theory.limits.coprod_comparison_inv_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_coproduct A B]
[category_theory.limits.has_binary_coproduct A' B']
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
[category_theory.limits.has_binary_coproduct (F.obj A') (F.obj B')]
(f : A ⟶ A')
(g : B ⟶ B')
[category_theory.is_iso (category_theory.limits.coprod_comparison F A B)]
[category_theory.is_iso (category_theory.limits.coprod_comparison F A' B')] :
category_theory.inv (category_theory.limits.coprod_comparison F A B) ≫ category_theory.limits.coprod.map (F.map f) (F.map g) = F.map (category_theory.limits.coprod.map f g) ≫ category_theory.inv (category_theory.limits.coprod_comparison F A' B')
If the coproduct comparison morphism is an iso, its inverse is natural.
theorem
category_theory.limits.coprod_comparison_inv_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_coproduct A B]
[category_theory.limits.has_binary_coproduct A' B']
[category_theory.limits.has_binary_coproduct (F.obj A) (F.obj B)]
[category_theory.limits.has_binary_coproduct (F.obj A') (F.obj B')]
(f : A ⟶ A')
(g : B ⟶ B')
[category_theory.is_iso (category_theory.limits.coprod_comparison F A B)]
[category_theory.is_iso (category_theory.limits.coprod_comparison F A' B')]
{X' : D}
(f' : F.obj A' ⨿ F.obj B' ⟶ X') :
category_theory.inv (category_theory.limits.coprod_comparison F A B) ≫ category_theory.limits.coprod.map (F.map f) (F.map g) ≫ f' = F.map (category_theory.limits.coprod.map f g) ≫ category_theory.inv (category_theory.limits.coprod_comparison F A' B') ≫ f'
@[simp]
theorem
category_theory.limits.coprod_comparison_nat_iso_hom_app
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_binary_coproducts D]
(A : C)
[∀ (B : C), category_theory.is_iso (category_theory.limits.coprod_comparison F A B)]
(B : C) :
@[simp]
theorem
category_theory.limits.coprod_comparison_nat_iso_inv
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_binary_coproducts D]
(A : C)
[∀ (B : C), category_theory.is_iso (category_theory.limits.coprod_comparison F A B)] :
(category_theory.limits.coprod_comparison_nat_iso F A).inv = (category_theory.as_iso {app := λ (B : C), category_theory.limits.coprod_comparison F A B, naturality' := _}).inv
noncomputable
def
category_theory.limits.coprod_comparison_nat_iso
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_binary_coproducts D]
(A : C)
[∀ (B : C), category_theory.is_iso (category_theory.limits.coprod_comparison F A B)] :
The natural isomorphism FA ⨿ F- ≅ F(A ⨿ -), provided each coprod_comparison F A B is an
isomorphism (as B changes).
Equations
- category_theory.limits.coprod_comparison_nat_iso F A = {hom := category_theory.limits.coprod_comparison_nat_trans F A, inv := (category_theory.as_iso {app := λ (B : C), category_theory.limits.coprod_comparison F A B, naturality' := _}).inv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.over.coprod_obj_map
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
{A : C}
(ᾰ g₁ g₂ : category_theory.over A)
(k : g₁ ⟶ g₂) :
ᾰ.coprod_obj.map k = category_theory.over.hom_mk (category_theory.limits.coprod.map (𝟙 ((𝟭 C).obj ᾰ.left)) k.left) _
noncomputable
def
category_theory.over.coprod_obj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
{A : C} :
Auxiliary definition for over.coprod.
Equations
- category_theory.over.coprod_obj = λ (f : category_theory.over A), {obj := λ (g : category_theory.over A), category_theory.over.mk (category_theory.limits.coprod.desc f.hom g.hom), map := λ (g₁ g₂ : category_theory.over A) (k : g₁ ⟶ g₂), category_theory.over.hom_mk (category_theory.limits.coprod.map (𝟙 ((𝟭 C).obj f.left)) k.left) _, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.over.coprod_obj_obj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
{A : C}
(ᾰ g : category_theory.over A) :
noncomputable
def
category_theory.over.coprod
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
{A : C} :
A category with binary coproducts has a functorial sup operation on over categories.
Equations
- category_theory.over.coprod = {obj := λ (f : category_theory.over A), f.coprod_obj, map := λ (f₁ f₂ : category_theory.over A) (k : f₁ ⟶ f₂), {app := λ (g : category_theory.over A), category_theory.over.hom_mk (category_theory.limits.coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) _, naturality' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.over.coprod_obj_2
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
{A : C}
(f : category_theory.over A) :
@[simp]
theorem
category_theory.over.coprod_map_app
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
{A : C}
(f₁ f₂ : category_theory.over A)
(k : f₁ ⟶ f₂)
(g : category_theory.over A) :
(category_theory.over.coprod.map k).app g = category_theory.over.hom_mk (category_theory.limits.coprod.map k.left (𝟙 ((𝟭 C).obj g.left))) _