Binary (co)products

We define a category WalkingPair, 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 HasBinaryProducts and HasBinaryCoproducts assert the existence of (co)limits shaped as walking pairs.

We include lemmas for simplifying equations involving projections and coprojections, and define braiding and associating isomorphisms, and the product comparison morphism.

References

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

inductive CategoryTheory.Limits.WalkingPair : Type

• left: CategoryTheory.Limits.WalkingPair
• right: CategoryTheory.Limits.WalkingPair

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

instance CategoryTheory.Limits.instDecidableEqWalkingPair : DecidableEq CategoryTheory.Limits.WalkingPair

instance CategoryTheory.Limits.instInhabitedWalkingPair : Inhabited CategoryTheory.Limits.WalkingPair

def CategoryTheory.Limits.WalkingPair.swap : CategoryTheory.Limits.WalkingPair ≃ CategoryTheory.Limits.WalkingPair

The equivalence swapping left and right.

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_apply_left : ↑CategoryTheory.Limits.WalkingPair.swap CategoryTheory.Limits.WalkingPair.left = CategoryTheory.Limits.WalkingPair.right

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_apply_right : ↑CategoryTheory.Limits.WalkingPair.swap CategoryTheory.Limits.WalkingPair.right = CategoryTheory.Limits.WalkingPair.left

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_tt : ↑CategoryTheory.Limits.WalkingPair.swap.symm CategoryTheory.Limits.WalkingPair.left = CategoryTheory.Limits.WalkingPair.right

@[simp]

theorem CategoryTheory.Limits.WalkingPair.swap_symm_apply_ff : ↑CategoryTheory.Limits.WalkingPair.swap.symm CategoryTheory.Limits.WalkingPair.right = CategoryTheory.Limits.WalkingPair.left

def CategoryTheory.Limits.WalkingPair.equivBool : CategoryTheory.Limits.WalkingPair ≃ Bool

An equivalence from WalkingPair to Bool, sometimes useful when reindexing limits.

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_left : ↑CategoryTheory.Limits.WalkingPair.equivBool CategoryTheory.Limits.WalkingPair.left = true

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_apply_right : ↑CategoryTheory.Limits.WalkingPair.equivBool CategoryTheory.Limits.WalkingPair.right = false

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_true : ↑CategoryTheory.Limits.WalkingPair.equivBool.symm true = CategoryTheory.Limits.WalkingPair.left

@[simp]

theorem CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_false : ↑CategoryTheory.Limits.WalkingPair.equivBool.symm false = CategoryTheory.Limits.WalkingPair.right

def CategoryTheory.Limits.pairFunction {C : Type u} (X : C) (Y : C) : CategoryTheory.Limits.WalkingPair → C

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

@[simp]

theorem CategoryTheory.Limits.pairFunction_left {C : Type u} (X : C) (Y : C) : CategoryTheory.Limits.pairFunction X Y CategoryTheory.Limits.WalkingPair.left = X

@[simp]

theorem CategoryTheory.Limits.pairFunction_right {C : Type u} (X : C) (Y : C) : CategoryTheory.Limits.pairFunction X Y CategoryTheory.Limits.WalkingPair.right = Y

def CategoryTheory.Limits.pair {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C

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

@[simp]

theorem CategoryTheory.Limits.pair_obj_left {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } = X

@[simp]

theorem CategoryTheory.Limits.pair_obj_right {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } = Y

def CategoryTheory.Limits.mapPair {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} {G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.right }) : F ⟶ G

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

@[simp]

theorem CategoryTheory.Limits.mapPair_left {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} {G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.right }) : (CategoryTheory.Limits.mapPair f g).app { as := CategoryTheory.Limits.WalkingPair.left } = f

@[simp]

theorem CategoryTheory.Limits.mapPair_right {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} {G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ G.obj { as := CategoryTheory.Limits.WalkingPair.right }) : (CategoryTheory.Limits.mapPair f g).app { as := CategoryTheory.Limits.WalkingPair.right } = g

@[simp]

theorem CategoryTheory.Limits.mapPairIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} {G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.right }) (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : (CategoryTheory.Limits.mapPairIso f g).inv.app X = (CategoryTheory.Limits.WalkingPair.rec f g X.as).inv

@[simp]

theorem CategoryTheory.Limits.mapPairIso_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} {G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.right }) (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : (CategoryTheory.Limits.mapPairIso f g).hom.app X = (CategoryTheory.Limits.WalkingPair.rec f g X.as).hom

def CategoryTheory.Limits.mapPairIso {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} {G : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C} (f : F.obj { as := CategoryTheory.Limits.WalkingPair.left } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.left }) (g : F.obj { as := CategoryTheory.Limits.WalkingPair.right } ≅ G.obj { as := CategoryTheory.Limits.WalkingPair.right }) : F ≅ G

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

@[simp]

theorem CategoryTheory.Limits.diagramIsoPair_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : (CategoryTheory.Limits.diagramIsoPair F).inv.app X = (CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.right })) X.as).inv

@[simp]

theorem CategoryTheory.Limits.diagramIsoPair_hom_app {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) (X : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) : (CategoryTheory.Limits.diagramIsoPair F).hom.app X = (CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Iso.refl (F.obj { as := CategoryTheory.Limits.WalkingPair.right })) X.as).hom

def CategoryTheory.Limits.diagramIsoPair {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) : F ≅ CategoryTheory.Limits.pair (F.obj { as := CategoryTheory.Limits.WalkingPair.left }) (F.obj { as := CategoryTheory.Limits.WalkingPair.right })

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

def CategoryTheory.Limits.pairComp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u} [CategoryTheory.Category.{v, u} D] (X : C) (Y : C) (F : CategoryTheory.Functor C D) : CategoryTheory.Functor.comp (CategoryTheory.Limits.pair X Y) F ≅ CategoryTheory.Limits.pair (F.obj X) (F.obj Y)

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

@[inline, reducible]

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

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

@[inline, reducible]

abbrev CategoryTheory.Limits.BinaryFan.fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }

The first projection of a binary fan.

@[inline, reducible]

abbrev CategoryTheory.Limits.BinaryFan.snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }

The second projection of a binary fan.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.π_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.π.app { as := CategoryTheory.Limits.WalkingPair.left } = CategoryTheory.Limits.BinaryFan.fst s

@[simp]

theorem CategoryTheory.Limits.BinaryFan.π_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) : s.π.app { as := CategoryTheory.Limits.WalkingPair.right } = CategoryTheory.Limits.BinaryFan.snd s

def CategoryTheory.Limits.BinaryFan.IsLimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) (lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)) (hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift T f g) (CategoryTheory.Limits.BinaryFan.fst s) = f) (hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), CategoryTheory.CategoryStruct.comp (lift T f g) (CategoryTheory.Limits.BinaryFan.snd s) = g) (uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.BinaryFan.fst s) = f → CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.BinaryFan.snd s) = g → m = lift T f g) : CategoryTheory.Limits.IsLimit s

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

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

@[inline, reducible]

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

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

@[inline, reducible]

abbrev CategoryTheory.Limits.BinaryCofan.inl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.left }

The first inclusion of a binary cofan.

@[inline, reducible]

abbrev CategoryTheory.Limits.BinaryCofan.inr {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.right }

The second inclusion of a binary cofan.

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.ι_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : s.ι.app { as := CategoryTheory.Limits.WalkingPair.left } = CategoryTheory.Limits.BinaryCofan.inl s

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.ι_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : s.ι.app { as := CategoryTheory.Limits.WalkingPair.right } = CategoryTheory.Limits.BinaryCofan.inr s

def CategoryTheory.Limits.BinaryCofan.IsColimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) (desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)) (hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inl s) (desc T f g) = f) (hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inr s) (desc T f g) = g) (uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inl s) m = f → CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inr s) m = g → m = desc T f g) : CategoryTheory.Limits.IsColimit s

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

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

@[simp]

theorem CategoryTheory.Limits.BinaryFan.mk_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).pt = P

def CategoryTheory.Limits.BinaryFan.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : CategoryTheory.Limits.BinaryFan X Y

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

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.mk_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).pt = P

def CategoryTheory.Limits.BinaryCofan.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : CategoryTheory.Limits.BinaryCofan X Y

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

@[simp]

theorem CategoryTheory.Limits.BinaryFan.mk_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : CategoryTheory.Limits.BinaryFan.fst (CategoryTheory.Limits.BinaryFan.mk π₁ π₂) = π₁

@[simp]

theorem CategoryTheory.Limits.BinaryFan.mk_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : CategoryTheory.Limits.BinaryFan.snd (CategoryTheory.Limits.BinaryFan.mk π₁ π₂) = π₂

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.mk_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : CategoryTheory.Limits.BinaryCofan.inl (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂) = ι₁

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.mk_inr {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : CategoryTheory.Limits.BinaryCofan.inr (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂) = ι₂

def CategoryTheory.Limits.isoBinaryFanMk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (c : CategoryTheory.Limits.BinaryFan X Y) : c ≅ CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Limits.BinaryFan.fst c) (CategoryTheory.Limits.BinaryFan.snd c)

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

def CategoryTheory.Limits.isoBinaryCofanMk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) : c ≅ CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Limits.BinaryCofan.inl c) (CategoryTheory.Limits.BinaryCofan.inr c)

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

def CategoryTheory.Limits.BinaryFan.isLimitMk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : (s : CategoryTheory.Limits.BinaryFan X Y) → s.pt ⟶ W) (fac_left : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) fst = CategoryTheory.Limits.BinaryFan.fst s) (fac_right : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) snd = CategoryTheory.Limits.BinaryFan.snd s) (uniq : ∀ (s : CategoryTheory.Limits.BinaryFan X Y) (m : s.pt ⟶ W), CategoryTheory.CategoryStruct.comp m fst = CategoryTheory.Limits.BinaryFan.fst s → CategoryTheory.CategoryStruct.comp m snd = CategoryTheory.Limits.BinaryFan.snd s → m = lift s) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd)

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

def CategoryTheory.Limits.BinaryCofan.isColimitMk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {W : C} {inl : X ⟶ W} {inr : Y ⟶ W} (desc : (s : CategoryTheory.Limits.BinaryCofan X Y) → W ⟶ s.pt) (fac_left : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inl (desc s) = CategoryTheory.Limits.BinaryCofan.inl s) (fac_right : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inr (desc s) = CategoryTheory.Limits.BinaryCofan.inr s) (uniq : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y) (m : W ⟶ s.pt), CategoryTheory.CategoryStruct.comp inl m = CategoryTheory.Limits.BinaryCofan.inl s → CategoryTheory.CategoryStruct.comp inr m = CategoryTheory.Limits.BinaryCofan.inr s → m = desc s) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr)

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

@[simp]

theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift'_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {s : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y) : ↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' h f g) = CategoryTheory.Limits.IsLimit.lift h (CategoryTheory.Limits.BinaryFan.mk f g)

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

If s is a limit binary fan over X and Y, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism l : W ⟶ s.pt satisfying l ≫ s.fst = f and l ≫ s.snd = g.

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.IsColimit.desc'_coe {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : ↑(CategoryTheory.Limits.BinaryCofan.IsColimit.desc' h f g) = CategoryTheory.Limits.IsColimit.desc h (CategoryTheory.Limits.BinaryCofan.mk f g)

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

If s is a colimit binary cofan over X and Y,, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism l : s.pt ⟶ W satisfying s.inl ≫ l = f and s.inr ≫ l = g.

def CategoryTheory.Limits.BinaryFan.isLimitFlip {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {c : CategoryTheory.Limits.BinaryFan X Y} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Limits.BinaryFan.snd c) (CategoryTheory.Limits.BinaryFan.fst c))

Binary products are symmetric.

theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (h : CategoryTheory.Limits.IsTerminal Y) (c : CategoryTheory.Limits.BinaryFan X Y) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.BinaryFan.fst c)

theorem CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (h : CategoryTheory.Limits.IsTerminal X) (c : CategoryTheory.Limits.BinaryFan X Y) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.BinaryFan.snd c)

noncomputable def CategoryTheory.Limits.BinaryFan.isLimitCompLeftIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {X' : C} (c : CategoryTheory.Limits.BinaryFan X Y) (f : X ⟶ X') [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.fst c) f) (CategoryTheory.Limits.BinaryFan.snd c))

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

noncomputable def CategoryTheory.Limits.BinaryFan.isLimitCompRightIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Y' : C} (c : CategoryTheory.Limits.BinaryFan X Y) (f : Y ⟶ Y') [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Limits.BinaryFan.fst c) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.snd c) f))

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

def CategoryTheory.Limits.BinaryCofan.isColimitFlip {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Limits.BinaryCofan.inr c) (CategoryTheory.Limits.BinaryCofan.inl c))

Binary coproducts are symmetric.

theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (h : CategoryTheory.Limits.IsInitial Y) (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.BinaryCofan.inl c)

theorem CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (h : CategoryTheory.Limits.IsInitial X) (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.BinaryCofan.inr c)

noncomputable def CategoryTheory.Limits.BinaryCofan.isColimitCompLeftIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {X' : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (f : X' ⟶ X) [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.BinaryCofan.inl c)) (CategoryTheory.Limits.BinaryCofan.inr c))

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

noncomputable def CategoryTheory.Limits.BinaryCofan.isColimitCompRightIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Y' : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (f : Y' ⟶ Y) [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Limits.BinaryCofan.inl c) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.BinaryCofan.inr c)))

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

@[inline, reducible]

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

An abbreviation for HasLimit (pair X Y).

@[inline, reducible]

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

An abbreviation for HasColimit (pair X Y).

@[inline, reducible]

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

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

@[inline, reducible]

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

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

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

Notation for the product

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

Notation for the coproduct

@[inline, reducible]

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

The projection map to the first component of the product.

@[inline, reducible]

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

The projection map to the second component of the product.

@[inline, reducible]

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

The inclusion map from the first component of the coproduct.

@[inline, reducible]

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

The inclusion map from the second component of the coproduct.

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

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

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

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

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

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

@[inline, reducible]

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

If the product of X and Y exists, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism prod.lift f g : W ⟶ X ⨯ Y.

@[inline, reducible]

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

diagonal arrow of the binary product in the category fam I

@[inline, reducible]

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

If the coproduct of X and Y exists, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism coprod.desc f g : X ⨿ Y ⟶ W.

@[inline, reducible]

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

codiagonal arrow of the binary coproduct

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

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

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

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

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

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

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

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

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

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

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

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

def CategoryTheory.Limits.prod.lift' {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) : { l // CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.fst = f ∧ CategoryTheory.CategoryStruct.comp l CategoryTheory.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.

def CategoryTheory.Limits.coprod.desc' {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) : { l // CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl l = f ∧ CategoryTheory.CategoryStruct.comp CategoryTheory.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.

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

If the products W ⨯ X and Y ⨯ Z exist, then every pair of morphisms f : W ⟶ Y and g : X ⟶ Z induces a morphism prod.map f g : W ⨯ X ⟶ Y ⨯ Z.

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

If the coproducts W ⨿ X and Y ⨿ Z exist, then every pair of morphisms f : W ⟶ Y and g : W ⟶ Z induces a morphism coprod.map f g : W ⨿ X ⟶ Y ⨿ Z.

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

If the products W ⨯ X and Y ⨯ Z exist, then every pair of isomorphisms f : W ≅ Y and g : X ≅ Z induces an isomorphism prod.mapIso f g : W ⨯ X ≅ Y ⨯ Z.

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[inline, reducible]

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

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

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

@[inline, reducible]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

The braiding isomorphism which swaps a binary product.

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

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

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

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

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

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

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

The braiding isomorphism is symmetric.

@[simp]

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

@[simp]

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

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

The associator isomorphism for binary products.

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

The braiding isomorphism which swaps a binary coproduct.

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

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

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

The braiding isomorphism is symmetric.

@[simp]

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

@[simp]

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

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

The associator isomorphism for binary coproducts.

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The binary product functor.

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

The product functor can be decomposed.

@[simp]

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

@[simp]

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

@[simp]

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

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

The binary coproduct functor.

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

The coproduct functor can be decomposed.

def CategoryTheory.Limits.prodComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) (A : C) (B : C) [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] : F.obj (A ⨯ B) ⟶ F.obj A ⨯ F.obj B

The product comparison morphism.

In CategoryTheory/Limits/Preserves we show this is always an iso iff F preserves binary products.

@[simp]

theorem CategoryTheory.Limits.prodComparison_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) h

@[simp]

theorem CategoryTheory.Limits.prodComparison_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) CategoryTheory.Limits.prod.fst = F.map CategoryTheory.Limits.prod.fst

@[simp]

theorem CategoryTheory.Limits.prodComparison_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.snd) h

@[simp]

theorem CategoryTheory.Limits.prodComparison_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) CategoryTheory.Limits.prod.snd = F.map CategoryTheory.Limits.prod.snd

theorem CategoryTheory.Limits.prodComparison_natural_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : F.obj A' ⨯ F.obj B' ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A' B') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g)) h)

theorem CategoryTheory.Limits.prodComparison_natural {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g)) (CategoryTheory.Limits.prodComparison F A' B') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B) (CategoryTheory.Limits.prod.map (F.map f) (F.map g))

Naturality of the prodComparison morphism in both arguments.

@[simp]

theorem CategoryTheory.Limits.prodComparisonNatTrans_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (F : CategoryTheory.Functor C D) (A : C) (B : C) : (CategoryTheory.Limits.prodComparisonNatTrans F A).app B = CategoryTheory.Limits.prodComparison F A B

def CategoryTheory.Limits.prodComparisonNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (F : CategoryTheory.Functor C D) (A : C) : CategoryTheory.Functor.comp (CategoryTheory.Limits.prod.functor.obj A) F ⟶ CategoryTheory.Functor.comp F (CategoryTheory.Limits.prod.functor.obj (F.obj A))

The product comparison morphism from F(A ⨯ -) to FA ⨯ F-, whose components are given by prodComparison.

theorem CategoryTheory.Limits.inv_prodComparison_map_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] {Z : D} (h : F.obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)) (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.fst) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h

theorem CategoryTheory.Limits.inv_prodComparison_map_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)) (F.map CategoryTheory.Limits.prod.fst) = CategoryTheory.Limits.prod.fst

theorem CategoryTheory.Limits.inv_prodComparison_map_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] {Z : D} (h : F.obj B ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)) (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.snd) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h

theorem CategoryTheory.Limits.inv_prodComparison_map_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)) (F.map CategoryTheory.Limits.prod.snd) = CategoryTheory.Limits.prod.snd

theorem CategoryTheory.Limits.prodComparison_inv_natural_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A' B')] {Z : D} (h : F.obj (A' ⨯ B') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.prod.map f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A' B')) h)

theorem CategoryTheory.Limits.prodComparison_inv_natural {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryProduct A B] [CategoryTheory.Limits.HasBinaryProduct A' B'] [CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryProduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] [CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A' B')] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)) (F.map (CategoryTheory.Limits.prod.map f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (F.map f) (F.map g)) (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A' B'))

If the product comparison morphism is an iso, its inverse is natural.

@[simp]

theorem CategoryTheory.Limits.prodComparisonNatIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : (CategoryTheory.Limits.prodComparisonNatIso F A).hom = CategoryTheory.Limits.prodComparisonNatTrans F A

@[simp]

theorem CategoryTheory.Limits.prodComparisonNatIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : (CategoryTheory.Limits.prodComparisonNatIso F A).inv = (CategoryTheory.asIso (CategoryTheory.NatTrans.mk fun B => CategoryTheory.Limits.prodComparison F A B)).inv

def CategoryTheory.Limits.prodComparisonNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] : CategoryTheory.Functor.comp (CategoryTheory.Limits.prod.functor.obj A) F ≅ CategoryTheory.Functor.comp F (CategoryTheory.Limits.prod.functor.obj (F.obj A))

The natural isomorphism F(A ⨯ -) ≅ FA ⨯ F-, provided each prodComparison F A B is an isomorphism (as B changes).

def CategoryTheory.Limits.coprodComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) (A : C) (B : C) [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] : F.obj A ⨿ F.obj B ⟶ F.obj (A ⨿ B)

The coproduct comparison morphism.

In CategoryTheory/Limits/Preserves we show this is always an iso iff F preserves binary coproducts.

@[simp]

theorem CategoryTheory.Limits.coprodComparison_inl_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) h

@[simp]

theorem CategoryTheory.Limits.coprodComparison_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.coprodComparison F A B) = F.map CategoryTheory.Limits.coprod.inl

@[simp]

theorem CategoryTheory.Limits.coprodComparison_inr_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj (A ⨿ B) ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) h) = CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) h

@[simp]

theorem CategoryTheory.Limits.coprodComparison_inr {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.coprodComparison F A B) = F.map CategoryTheory.Limits.coprod.inr

theorem CategoryTheory.Limits.coprodComparison_natural_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') {Z : D} (h : F.obj (A' ⨿ B') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A' B') h)

theorem CategoryTheory.Limits.coprodComparison_natural {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprodComparison F A B) (F.map (CategoryTheory.Limits.coprod.map f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) (CategoryTheory.Limits.coprodComparison F A' B')

Naturality of the coprod_comparison morphism in both arguments.

@[simp]

theorem CategoryTheory.Limits.coprodComparisonNatTrans_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (F : CategoryTheory.Functor C D) (A : C) (B : C) : (CategoryTheory.Limits.coprodComparisonNatTrans F A).app B = CategoryTheory.Limits.coprodComparison F A B

def CategoryTheory.Limits.coprodComparisonNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (F : CategoryTheory.Functor C D) (A : C) : CategoryTheory.Functor.comp F (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) ⟶ CategoryTheory.Functor.comp (CategoryTheory.Limits.coprod.functor.obj A) F

The coproduct comparison morphism from FA ⨿ F- to F(A ⨿ -), whose components are given by coprodComparison.

theorem CategoryTheory.Limits.map_inl_inv_coprodComparison_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] {Z : D} (h : F.obj A ⨿ F.obj B ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h

theorem CategoryTheory.Limits.map_inl_inv_coprodComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inl) (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) = CategoryTheory.Limits.coprod.inl

theorem CategoryTheory.Limits.map_inr_inv_coprodComparison_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] {Z : D} (h : F.obj A ⨿ F.obj B ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h

theorem CategoryTheory.Limits.map_inr_inv_coprodComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {B : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr) (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) = CategoryTheory.Limits.coprod.inr

theorem CategoryTheory.Limits.coprodComparison_inv_natural_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')] {Z : D} (h : F.obj A' ⨿ F.obj B' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B')) h)

theorem CategoryTheory.Limits.coprodComparison_inv_natural {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) {A : C} {A' : C} {B : C} {B' : C} [CategoryTheory.Limits.HasBinaryCoproduct A B] [CategoryTheory.Limits.HasBinaryCoproduct A' B'] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)] [CategoryTheory.Limits.HasBinaryCoproduct (F.obj A') (F.obj B')] (f : A ⟶ A') (g : B ⟶ B') [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] [CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A' B')] : CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) (CategoryTheory.Limits.coprod.map (F.map f) (F.map g)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.coprod.map f g)) (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A' B'))

If the coproduct comparison morphism is an iso, its inverse is natural.

@[simp]

theorem CategoryTheory.Limits.coprodComparisonNatIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : (CategoryTheory.Limits.coprodComparisonNatIso F A).hom = CategoryTheory.Limits.coprodComparisonNatTrans F A

@[simp]

theorem CategoryTheory.Limits.coprodComparisonNatIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : (CategoryTheory.Limits.coprodComparisonNatIso F A).inv = (CategoryTheory.asIso (CategoryTheory.NatTrans.mk fun B => CategoryTheory.Limits.coprodComparison F A B)).inv

def CategoryTheory.Limits.coprodComparisonNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)] : CategoryTheory.Functor.comp F (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) ≅ CategoryTheory.Functor.comp (CategoryTheory.Limits.coprod.functor.obj A) F

The natural isomorphism FA ⨿ F- ≅ F(A ⨿ -), provided each coprodComparison F A B is an isomorphism (as B changes).

@[simp]

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

@[simp]

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

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

Auxiliary definition for Over.coprod.

@[simp]

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

@[simp]

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

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

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