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

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

• left : WalkingPair
• right : WalkingPair

@[implicit_reducible]

instance CategoryTheory.Limits.instDecidableEqWalkingPair : DecidableEq WalkingPair

@[implicit_reducible]

instance CategoryTheory.Limits.instInhabitedWalkingPair : Inhabited WalkingPair

def CategoryTheory.Limits.instInhabitedWalkingPair.default : WalkingPair

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

The equivalence swapping left and right.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.pairFunction {C : Type u} (X Y : C) : 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 Y : C) : pairFunction X Y WalkingPair.left = X

@[simp]

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

def CategoryTheory.Limits.pair {C : Type u} [Category.{v, u} C] (X Y : C) : Functor (Discrete 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} [Category.{v, u} C] (X Y : C) : (pair X Y).obj { as := WalkingPair.left } = X

@[simp]

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

def CategoryTheory.Limits.mapPair {C : Type u} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ⟶ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ⟶ G.obj { as := 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} [Category.{v, u} C] {F G : Functor (Discrete WalkingPair) C} (f : F.obj { as := WalkingPair.left } ⟶ G.obj { as := WalkingPair.left }) (g : F.obj { as := WalkingPair.right } ⟶ G.obj { as := WalkingPair.right }) : (mapPair f g).app { as := WalkingPair.left } = f

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

The first projection of a binary fan.

@[reducible, inline]

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

The second projection of a binary fan.

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

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

def CategoryTheory.Limits.BinaryFan.ext {C : Type u} [Category.{v, u} C] {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryStruct.comp e.hom c'.fst) (h₂ : c.snd = CategoryStruct.comp e.hom c'.snd) : c ≅ c'

Constructs an isomorphism of BinaryFans out of an isomorphism of the tips that commutes with the projections.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.ext_hom_hom {C : Type u} [Category.{v, u} C] {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt) (h₁ : c.fst = CategoryStruct.comp e.hom c'.fst) (h₂ : c.snd = CategoryStruct.comp e.hom c'.snd) : (ext e h₁ h₂).hom.hom = e.hom

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

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

The first inclusion of a binary cofan.

@[reducible, inline]

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

The second inclusion of a binary cofan.

def CategoryTheory.Limits.BinaryCofan.ext {C : Type u} [Category.{v, u} C] {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : CategoryStruct.comp c.inl e.hom = c'.inl) (h₂ : CategoryStruct.comp c.inr e.hom = c'.inr) : c ≅ c'

Constructs an isomorphism of BinaryCofans out of an isomorphism of the tips that commutes with the injections.

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.ext_hom_hom {C : Type u} [Category.{v, u} C] {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : CategoryStruct.comp c.inl e.hom = c'.inl) (h₂ : CategoryStruct.comp c.inr e.hom = c'.inr) : (ext e h₁ h₂).hom.hom = e.hom

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

def CategoryTheory.Limits.BinaryFan.isLimitMk {C : Type u} [Category.{v, u} C] {X Y W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (lift : (s : BinaryFan X Y) → s.pt ⟶ W) (fac_left : ∀ (s : BinaryFan X Y), CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : BinaryFan X Y), CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W), CategoryStruct.comp m fst = s.fst → CategoryStruct.comp m snd = s.snd → m = lift s) : IsLimit (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} [Category.{v, u} C] {X Y W : C} {inl : X ⟶ W} {inr : Y ⟶ W} (desc : (s : BinaryCofan X Y) → W ⟶ s.pt) (fac_left : ∀ (s : BinaryCofan X Y), CategoryStruct.comp inl (desc s) = s.inl) (fac_right : ∀ (s : BinaryCofan X Y), CategoryStruct.comp inr (desc s) = s.inr) (uniq : ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt), CategoryStruct.comp inl m = s.inl → CategoryStruct.comp inr m = s.inr → m = desc s) : IsColimit (mk inl inr)

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

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

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

@[simp]

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

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

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

@[simp]

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

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

Binary products are symmetric.

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

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

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

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

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

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

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

Binary coproducts are symmetric.

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

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

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

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

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

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

@[reducible, inline]

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

An abbreviation for HasLimit (pair X Y).

@[reducible, inline]

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

An abbreviation for HasColimit (pair X Y).

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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

Notation for the product

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

Notation for the coproduct

@[reducible, inline]

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

The projection map to the first component of the product.

@[reducible, inline]

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

The projection map to the second component of the product.

@[reducible, inline]

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

The inclusion map from the first component of the coproduct.

@[reducible, inline]

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

The inclusion map from the second component of the coproduct.

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

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

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

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

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

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

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

diagonal arrow of the binary product in the category fam I

@[reducible, inline]

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

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

@[reducible, inline]

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

codiagonal arrow of the binary coproduct

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

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

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

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

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

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

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

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

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

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

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

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

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

If the product of X and Y exists, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism l : W ⟶ X ⨯ Y satisfying l ≫ Prod.fst = f and l ≫ Prod.snd = g.

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

If the coproduct of X and Y exists, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism l : X ⨿ Y ⟶ W satisfying coprod.inl ≫ l = f and coprod.inr ≫ l = g.

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

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

noncomputable def CategoryTheory.Limits.coprod.map {C : Type u} [Category.{v, u} C] {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] (f : 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.

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

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

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

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

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

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

The braiding isomorphism which swaps a binary product.

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

The braiding isomorphism is symmetric.

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

The braiding isomorphism is symmetric.

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

The associator isomorphism for binary products.

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

The braiding isomorphism which swaps a binary coproduct.

@[simp]

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

@[simp]

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

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

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

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

The braiding isomorphism is symmetric.

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

The associator isomorphism for binary coproducts.

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

The binary product functor.

@[simp]

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

@[simp]

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

@[simp]

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

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

The product functor can be decomposed.

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

The binary coproduct functor.

@[simp]

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

@[simp]

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

@[simp]

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

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

The coproduct functor can be decomposed.

noncomputable def CategoryTheory.Limits.prodComparison {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) (A B : C) [HasBinaryProduct A B] [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 {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) (A B : C) [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] : CategoryStruct.comp (prodComparison F A B) prod.fst = F.map prod.fst

@[simp]

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

@[simp]

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

@[simp]

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

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

Naturality of the prodComparison morphism in both arguments.

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

Naturality of the prodComparison morphism in both arguments.

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

Naturality of the prodComparison morphism in a natural transformation.

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

Naturality of the prodComparison morphism in a natural transformation.

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

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

@[simp]

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

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

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

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

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

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

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

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

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

noncomputable def CategoryTheory.Limits.prodComparisonNatIso {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] (F : Functor C D) [HasBinaryProducts C] [HasBinaryProducts D] (A : C) [∀ (B : C), IsIso (prodComparison F A B)] : (prod.functor.obj A).comp F ≅ F.comp (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).

@[simp]

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

@[simp]

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

theorem CategoryTheory.Limits.prodComparison_comp {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{w, u₂} D] {E : Type u₃} [Category.{w', u₃} E] (F : Functor C D) (G : Functor D E) {A B : C} [HasBinaryProduct A B] [HasBinaryProduct (F.obj A) (F.obj B)] [HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))] [HasBinaryProduct ((F.comp G).obj A) ((F.comp G).obj B)] : prodComparison (F.comp G) A B = CategoryStruct.comp (G.map (prodComparison F A B)) (prodComparison G (F.obj A) (F.obj B))

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

The coproduct comparison morphism.

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Naturality of the coprodComparison morphism in both arguments.

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

Naturality of the coprodComparison morphism in both arguments.

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

Auxiliary definition for Over.coprod.

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

A binary fan gives a binary cofan in the opposite category.

@[reducible, inline]

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

A binary cofan gives a binary fan in the opposite category.

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.unop {C : Type u} [Category.{v, u} C] {X Y : C} (c : BinaryFan (Opposite.op X) (Opposite.op Y)) : BinaryCofan X Y

A binary fan in the opposite category gives a binary cofan.

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCofan.unop {C : Type u} [Category.{v, u} C] {X Y : C} (c : BinaryCofan (Opposite.op X) (Opposite.op Y)) : BinaryFan X Y

A binary cofan in the opposite category gives a binary fan.

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.BinaryFan.unop_mk {C : Type u} [Category.{v, u} C] {X Y P : C} (π₁ : Opposite.op P ⟶ Opposite.op X) (π₂ : Opposite.op P ⟶ Opposite.op Y) : (mk π₁ π₂).unop = BinaryCofan.mk π₁.unop π₂.unop

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.BinaryCofan.unop_mk {C : Type u} [Category.{v, u} C] {X Y P : C} (ι₁ : Opposite.op X ⟶ Opposite.op P) (ι₂ : Opposite.op Y ⟶ Opposite.op P) : (mk ι₁ ι₂).unop = BinaryFan.mk ι₁.unop ι₂.unop

def CategoryTheory.Limits.BinaryFan.IsLimit.op {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryFan X Y} (hc : IsLimit c) : IsColimit c.op

If a BinaryFan is a limit, then its opposite is a colimit.

def CategoryTheory.Limits.BinaryCofan.IsColimit.op {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryCofan X Y} (hc : IsColimit c) : IsLimit c.op

If a BinaryCofan is a colimit, then its opposite is a limit.

def CategoryTheory.Limits.BinaryFan.IsLimit.unop {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryFan (Opposite.op X) (Opposite.op Y)} (hc : IsLimit c) : IsColimit c.unop

If a BinaryFan in the opposite category is a limit, then its unop is a colimit.

def CategoryTheory.Limits.BinaryCofan.IsColimit.unop {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryCofan (Opposite.op X) (Opposite.op Y)} (hc : IsColimit c) : IsLimit c.unop

If a BinaryCofan in the opposite category is a colimit, then its unop is a limit.

def CategoryTheory.Limits.BinaryFan.swap {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : BinaryFan Y X

Swap the two sides of a BinaryFan.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.swap_fst {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : s.swap.fst = s.snd

@[simp]

theorem CategoryTheory.Limits.BinaryFan.swap_snd {C : Type u} [Category.{v, u} C] {X Y : C} (s : BinaryFan X Y) : s.swap.snd = s.fst

def CategoryTheory.Limits.IsLimit.binaryFanSwap {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (I : IsLimit s) : IsLimit s.swap

If a binary fan s over X Y is a limit cone, then s.swap is a limit cone over Y X.

@[simp]

theorem CategoryTheory.Limits.IsLimit.binaryFanSwap_lift {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (I : IsLimit s) (t : Cone (pair Y X)) : I.binaryFanSwap.lift t = I.lift (BinaryFan.swap t)

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

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

def CategoryTheory.Limits.BinaryFan.braiding {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} {t : BinaryFan Y X} (P : IsLimit s) (Q : IsLimit t) : s.pt ≅ t.pt

Given a limit cone over X and Y, and another limit cone over Y and X, we can construct an isomorphism between the cone points. Relative to some fixed choice of limits cones for every pair, these isomorphisms constitute a braiding.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_hom_fst {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) : CategoryStruct.comp (braiding P Q).hom t.fst = s.snd

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_hom_fst_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) {Z : C} (h : (pair Y X).obj { as := WalkingPair.left } ⟶ Z) : CategoryStruct.comp (braiding P Q).hom (CategoryStruct.comp t.fst h) = CategoryStruct.comp s.snd h

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_hom_snd {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) : CategoryStruct.comp (braiding P Q).hom t.snd = s.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_hom_snd_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) {Z : C} (h : (pair Y X).obj { as := WalkingPair.right } ⟶ Z) : CategoryStruct.comp (braiding P Q).hom (CategoryStruct.comp t.snd h) = CategoryStruct.comp s.fst h

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_inv_fst {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) : CategoryStruct.comp (braiding P Q).inv s.fst = t.snd

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_inv_fst_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) {Z : C} (h : (pair X Y).obj { as := WalkingPair.left } ⟶ Z) : CategoryStruct.comp (braiding P Q).inv (CategoryStruct.comp s.fst h) = CategoryStruct.comp t.snd h

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_inv_snd {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) : CategoryStruct.comp (braiding P Q).inv s.snd = t.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.braiding_inv_snd_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t) {Z : C} (h : (pair X Y).obj { as := WalkingPair.right } ⟶ Z) : CategoryStruct.comp (braiding P Q).inv (CategoryStruct.comp s.snd h) = CategoryStruct.comp t.fst h

def CategoryTheory.Limits.BinaryFan.assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (Q : IsLimit sYZ) (s : BinaryFan sXY.pt Z) : BinaryFan X sYZ.pt

Given binary fans sXY over X Y, and sYZ over Y Z, and s over sXY.X Z, if sYZ is a limit cone we can construct a binary fan over X sYZ.X.

This is an ingredient of building the associator for a Cartesian category.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assoc_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (Q : IsLimit sYZ) (s : BinaryFan sXY.pt Z) : (assoc Q s).fst = CategoryStruct.comp s.fst sXY.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assoc_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (Q : IsLimit sYZ) (s : BinaryFan sXY.pt Z) : (assoc Q s).snd = Q.lift (mk (CategoryStruct.comp s.fst sXY.snd) s.snd)

def CategoryTheory.Limits.BinaryFan.assocInv {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (s : BinaryFan X sYZ.pt) : BinaryFan sXY.pt Z

Given binary fans sXY over X Y, and sYZ over Y Z, and s over X sYZ.X, if sYZ is a limit cone we can construct a binary fan over sXY.X Z.

This is an ingredient of building the associator for a Cartesian category.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assocInv_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (s : BinaryFan X sYZ.pt) : (assocInv P s).fst = P.lift (mk s.fst (CategoryStruct.comp s.snd sYZ.fst))

@[simp]

theorem CategoryTheory.Limits.BinaryFan.assocInv_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (s : BinaryFan X sYZ.pt) : (assocInv P s).snd = CategoryStruct.comp s.snd sYZ.snd

def CategoryTheory.Limits.IsLimit.assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (Q : IsLimit sYZ) {s : BinaryFan sXY.pt Z} (R : IsLimit s) : IsLimit (BinaryFan.assoc Q s)

If all the binary fans involved a limit cones, BinaryFan.assoc produces another limit cone.

@[simp]

theorem CategoryTheory.Limits.IsLimit.assoc_lift {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (Q : IsLimit sYZ) {s : BinaryFan sXY.pt Z} (R : IsLimit s) (t : Cone (pair X sYZ.pt)) : (P.assoc Q R).lift t = R.lift (BinaryFan.assocInv P t)

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.associator {C : Type u} [Category.{v, u} C] {X Y Z : C} {sXY : BinaryFan X Y} {sYZ : BinaryFan Y Z} (P : IsLimit sXY) (Q : IsLimit sYZ) {s : BinaryFan sXY.pt Z} (R : IsLimit s) {t : BinaryFan X sYZ.pt} (S : IsLimit t) : s.pt ≅ t.pt

Given two pairs of limit cones corresponding to the parenthesisations of X × Y × Z, we obtain an isomorphism between the cone points.

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryFan.associatorOfLimitCone {C : Type u} [Category.{v, u} C] (L : (X Y : C) → LimitCone (pair X Y)) (X Y Z : C) : (L (L X Y).cone.pt Z).cone.pt ≅ (L X (L Y Z).cone.pt).cone.pt

Given a fixed family of limit data for every pair X Y, we obtain an associator.

def CategoryTheory.Limits.BinaryFan.leftUnitor {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan s.pt X} (Q : IsLimit t) : t.pt ≅ X

Construct a left unitor from specified limit cones.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.leftUnitor_hom {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan s.pt X} (Q : IsLimit t) : (leftUnitor P Q).hom = t.snd

@[simp]

theorem CategoryTheory.Limits.BinaryFan.leftUnitor_inv {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan s.pt X} (Q : IsLimit t) : (leftUnitor P Q).inv = Q.lift (mk (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) => x.as.elim, naturality := ⋯ } }) (CategoryStruct.id { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) => x.as.elim, naturality := ⋯ } }.pt))

def CategoryTheory.Limits.BinaryFan.rightUnitor {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan X s.pt} (Q : IsLimit t) : t.pt ≅ X

Construct a right unitor from specified limit cones.

@[simp]

theorem CategoryTheory.Limits.BinaryFan.rightUnitor_hom {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan X s.pt} (Q : IsLimit t) : (rightUnitor P Q).hom = t.fst

@[simp]

theorem CategoryTheory.Limits.BinaryFan.rightUnitor_inv {C : Type u} [Category.{v, u} C] {X : C} {s : Cone (Functor.empty C)} (P : IsLimit s) {t : BinaryFan X s.pt} (Q : IsLimit t) : (rightUnitor P Q).inv = Q.lift (mk (CategoryStruct.id X) (P.lift { pt := X, π := { app := fun (x : Discrete PEmpty.{1}) => x.as.elim, naturality := ⋯ } }))