Binary (co)products of type-valued functors

Defines an explicit construction of binary products and coproducts of type-valued functors.

Also defines isomorphisms to the categorical product and coproduct, respectively.

def CategoryTheory.FunctorToTypes.prod {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Functor C (Type w)

prod F G is the explicit binary product of type-valued functors F and G.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.FunctorToTypes.prod.fst {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} : prod F G ⟶ F

The first projection of prod F G, onto F.

Equations

• CategoryTheory.FunctorToTypes.prod.fst = { app := fun (x : C) (a : (CategoryTheory.FunctorToTypes.prod F G).obj x) => a.1, naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.fst_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (x✝ : C) (a : (prod F G).obj x✝) : fst.app x✝ a = a.1

def CategoryTheory.FunctorToTypes.prod.snd {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} : prod F G ⟶ G

The second projection of prod F G, onto G.

Equations

• CategoryTheory.FunctorToTypes.prod.snd = { app := fun (x : C) (a : (CategoryTheory.FunctorToTypes.prod F G).obj x) => a.2, naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.snd_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (x✝ : C) (a : (prod F G).obj x✝) : snd.app x✝ a = a.2

def CategoryTheory.FunctorToTypes.prod.lift {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) : F ⟶ prod F₁ F₂

Given natural transformations F ⟶ F₁ and F ⟶ F₂, construct a natural transformation F ⟶ prod F₁ F₂.

Equations

• CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂ = { app := fun (x : C) (y : F.obj x) => (τ₁.app x y, τ₂.app x y), naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.lift_app {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) (x : C) (y : F.obj x) : (lift τ₁ τ₂).app x y = (τ₁.app x y, τ₂.app x y)

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.lift_fst {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) : CategoryStruct.comp (lift τ₁ τ₂) fst = τ₁

@[simp]

theorem CategoryTheory.FunctorToTypes.prod.lift_snd {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) : CategoryStruct.comp (lift τ₁ τ₂) snd = τ₂

def CategoryTheory.FunctorToTypes.binaryProductCone {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.BinaryFan F G

The binary fan whose point is prod F G.

Equations

• CategoryTheory.FunctorToTypes.binaryProductCone F G = CategoryTheory.Limits.BinaryFan.mk CategoryTheory.FunctorToTypes.prod.fst CategoryTheory.FunctorToTypes.prod.snd

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductCone_pt_map {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (a : F.obj X✝ × G.obj X✝) : (binaryProductCone F G).pt.map f a = (F.map f a.1, G.map f a.2)

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductCone_π_app {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (x✝ : Discrete Limits.WalkingPair) : (binaryProductCone F G).π.app x✝ = match x✝.as with | Limits.WalkingPair.left => prod.fst | Limits.WalkingPair.right => prod.snd

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductCone_pt_obj {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (binaryProductCone F G).pt.obj a = (F.obj a × G.obj a)

def CategoryTheory.FunctorToTypes.binaryProductLimit {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.IsLimit (binaryProductCone F G)

prod F G is a limit cone.

Equations

• CategoryTheory.FunctorToTypes.binaryProductLimit F G = { lift := fun (s : CategoryTheory.Limits.BinaryFan F G) => CategoryTheory.FunctorToTypes.prod.lift s.fst s.snd, fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductLimit_lift {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (s : Limits.BinaryFan F G) : (binaryProductLimit F G).lift s = prod.lift s.fst s.snd

def CategoryTheory.FunctorToTypes.binaryProductLimitCone {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.LimitCone (Limits.pair F G)

prod F G is a binary product for F and G.

Equations

• CategoryTheory.FunctorToTypes.binaryProductLimitCone F G = { cone := CategoryTheory.FunctorToTypes.binaryProductCone F G, isLimit := CategoryTheory.FunctorToTypes.binaryProductLimit F G }

noncomputable def CategoryTheory.FunctorToTypes.binaryProductIso {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : F ⨯ G ≅ prod F G

The categorical binary product of type-valued functors is prod F G.

Equations

• CategoryTheory.FunctorToTypes.binaryProductIso F G = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.FunctorToTypes.binaryProductLimitCone F G)

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_hom_comp_fst {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp (binaryProductIso F G).hom prod.fst = Limits.prod.fst

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_hom_comp_snd {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp (binaryProductIso F G).hom prod.snd = Limits.prod.snd

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_fst {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp (binaryProductIso F G).inv Limits.prod.fst = prod.fst

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_fst_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : (prod F G).obj a) : Limits.prod.fst.app a ((binaryProductIso F G).inv.app a z) = z.1

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_snd {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp (binaryProductIso F G).inv Limits.prod.snd = prod.snd

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductIso_inv_comp_snd_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : (prod F G).obj a) : Limits.prod.snd.app a ((binaryProductIso F G).inv.app a z) = z.2

noncomputable def CategoryTheory.FunctorToTypes.prodMk {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) : (F ⨯ G).obj a

Construct an element of (F ⨯ G).obj a from an element of F.obj a and an element of G.obj a.

Equations

• CategoryTheory.FunctorToTypes.prodMk x y = (CategoryTheory.FunctorToTypes.binaryProductIso F G).inv.app a (x, y)

@[simp]

theorem CategoryTheory.FunctorToTypes.prodMk_fst {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) : Limits.prod.fst.app a (prodMk x y) = x

@[simp]

theorem CategoryTheory.FunctorToTypes.prodMk_snd {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) : Limits.prod.snd.app a (prodMk x y) = y

theorem CategoryTheory.FunctorToTypes.prod_ext {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (z w : (prod F G).obj a) (h1 : z.1 = w.1) (h2 : z.2 = w.2) : z = w

theorem CategoryTheory.FunctorToTypes.prod_ext_iff {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} {z w : (prod F G).obj a} : z = w ↔ z.1 = w.1 ∧ z.2 = w.2

noncomputable def CategoryTheory.FunctorToTypes.binaryProductEquiv {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (F ⨯ G).obj a ≃ F.obj a × G.obj a

(F ⨯ G).obj a is in bijection with the product of F.obj a and G.obj a.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductEquiv_symm_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : F.obj a × G.obj a) : (binaryProductEquiv F G a).symm z = prodMk z.1 z.2

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryProductEquiv_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : (F ⨯ G).obj a) : (binaryProductEquiv F G a) z = (((binaryProductIso F G).hom.app a z).1, ((binaryProductIso F G).hom.app a z).2)

theorem CategoryTheory.FunctorToTypes.prod_ext' {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z w : (F ⨯ G).obj a) (h1 : Limits.prod.fst.app a z = Limits.prod.fst.app a w) (h2 : Limits.prod.snd.app a z = Limits.prod.snd.app a w) : z = w

theorem CategoryTheory.FunctorToTypes.prod_ext'_iff {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} {z w : (F ⨯ G).obj a} : z = w ↔ Limits.prod.fst.app a z = Limits.prod.fst.app a w ∧ Limits.prod.snd.app a z = Limits.prod.snd.app a w

def CategoryTheory.FunctorToTypes.coprod {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Functor C (Type w)

coprod F G is the explicit binary coproduct of type-valued functors F and G.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.FunctorToTypes.coprod.inl {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} : F ⟶ coprod F G

The left inclusion of F into coprod F G.

Equations

• CategoryTheory.FunctorToTypes.coprod.inl = { app := fun (x : C) (x_1 : F.obj x) => Sum.inl x_1, naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.inl_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (x✝ : C) (x : F.obj x✝) : inl.app x✝ x = Sum.inl x

def CategoryTheory.FunctorToTypes.coprod.inr {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} : G ⟶ coprod F G

The right inclusion of G into coprod F G.

Equations

• CategoryTheory.FunctorToTypes.coprod.inr = { app := fun (x : C) (x_1 : G.obj x) => Sum.inr x_1, naturality := ⋯ }

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.inr_app {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} (x✝ : C) (x : G.obj x✝) : inr.app x✝ x = Sum.inr x

def CategoryTheory.FunctorToTypes.coprod.desc {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) : coprod F₁ F₂ ⟶ F

Given natural transformations F₁ ⟶ F and F₂ ⟶ F, construct a natural transformation coprod F₁ F₂ ⟶ F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.desc_app {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) (a : C) (x : (coprod F₁ F₂).obj a) : (desc τ₁ τ₂).app a x = Sum.casesOn (motive := fun (t : F₁.obj a ⊕ F₂.obj a) => x = t → F.obj a) x (fun (x_1 : F₁.obj a) (h : x = Sum.inl x_1) => τ₁.app a x_1) (fun (x_1 : F₂.obj a) (h : x = Sum.inr x_1) => τ₂.app a x_1) ⋯

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.desc_inl {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) : CategoryStruct.comp inl (desc τ₁ τ₂) = τ₁

@[simp]

theorem CategoryTheory.FunctorToTypes.coprod.desc_inr {C : Type u} [Category.{v, u} C] {F F₁ F₂ : Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) : CategoryStruct.comp inr (desc τ₁ τ₂) = τ₂

def CategoryTheory.FunctorToTypes.binaryCoproductCocone {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.BinaryCofan F G

The binary cofan whose point is coprod F G.

Equations

• CategoryTheory.FunctorToTypes.binaryCoproductCocone F G = CategoryTheory.Limits.BinaryCofan.mk CategoryTheory.FunctorToTypes.coprod.inl CategoryTheory.FunctorToTypes.coprod.inr

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_map {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x : F.obj X✝ ⊕ G.obj X✝) : (binaryCoproductCocone F G).pt.map f x = Sum.rec (motive := fun (t : F.obj X✝ ⊕ G.obj X✝) => x = t → F.obj Y✝ ⊕ G.obj Y✝) (fun (val : F.obj X✝) (h : x = Sum.inl val) => Sum.inl (F.map f val)) (fun (val : G.obj X✝) (h : x = Sum.inr val) => Sum.inr (G.map f val)) x ⋯

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_obj {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (binaryCoproductCocone F G).pt.obj a = (F.obj a ⊕ G.obj a)

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductCocone_ι_app {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (x✝ : Discrete Limits.WalkingPair) : (binaryCoproductCocone F G).ι.app x✝ = match x✝.as with | Limits.WalkingPair.left => coprod.inl | Limits.WalkingPair.right => coprod.inr

def CategoryTheory.FunctorToTypes.binaryCoproductColimit {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.IsColimit (binaryCoproductCocone F G)

coprod F G is a colimit cocone.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductColimit_desc {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (s : Limits.BinaryCofan F G) : (binaryCoproductColimit F G).desc s = coprod.desc s.inl s.inr

def CategoryTheory.FunctorToTypes.binaryCoproductColimitCocone {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : Limits.ColimitCocone (Limits.pair F G)

coprod F G is a binary coproduct for F and G.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.FunctorToTypes.binaryCoproductIso {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : F ⨿ G ≅ coprod F G

The categorical binary coproduct of type-valued functors is coprod F G.

Equations

• CategoryTheory.FunctorToTypes.binaryCoproductIso F G = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.FunctorToTypes.binaryCoproductColimitCocone F G)

@[simp]

theorem CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_hom {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp Limits.coprod.inl (binaryCoproductIso F G).hom = coprod.inl

@[simp]

theorem CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_hom_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (x : F.obj a) : (binaryCoproductIso F G).hom.app a (Limits.coprod.inl.app a x) = Sum.inl x

@[simp]

theorem CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_hom {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp Limits.coprod.inr (binaryCoproductIso F G).hom = coprod.inr

@[simp]

theorem CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_hom_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (x : G.obj a) : (binaryCoproductIso F G).hom.app a (Limits.coprod.inr.app a x) = Sum.inr x

@[simp]

theorem CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_inv {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp coprod.inl (binaryCoproductIso F G).inv = Limits.coprod.inl

@[simp]

theorem CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_inv_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (x : F.obj a) : (binaryCoproductIso F G).inv.app a (Sum.inl x) = Limits.coprod.inl.app a x

@[simp]

theorem CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_inv {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) : CategoryStruct.comp coprod.inr (binaryCoproductIso F G).inv = Limits.coprod.inr

@[simp]

theorem CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_inv_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (x : G.obj a) : (binaryCoproductIso F G).inv.app a (Sum.inr x) = Limits.coprod.inr.app a x

@[reducible, inline]

noncomputable abbrev CategoryTheory.FunctorToTypes.coprodInl {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : F.obj a) : (F ⨿ G).obj a

Construct an element of (F ⨿ G).obj a from an element of F.obj a

Equations

• CategoryTheory.FunctorToTypes.coprodInl x = (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a (Sum.inl x)

@[reducible, inline]

noncomputable abbrev CategoryTheory.FunctorToTypes.coprodInr {C : Type u} [Category.{v, u} C] {F G : Functor C (Type w)} {a : C} (x : G.obj a) : (F ⨿ G).obj a

Construct an element of (F ⨿ G).obj a from an element of G.obj a

Equations

• CategoryTheory.FunctorToTypes.coprodInr x = (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).inv.app a (Sum.inr x)

noncomputable def CategoryTheory.FunctorToTypes.binaryCoproductEquiv {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) : (F ⨿ G).obj a ≃ F.obj a ⊕ G.obj a

(F ⨿ G).obj a is in bijection with disjoint union of F.obj a and G.obj a.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductEquiv_symm_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : F.obj a ⊕ G.obj a) : (binaryCoproductEquiv F G a).symm z = (binaryCoproductIso F G).inv.app a z

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductEquiv_apply {C : Type u} [Category.{v, u} C] (F G : Functor C (Type w)) (a : C) (z : (F ⨿ G).obj a) : (binaryCoproductEquiv F G a) z = (binaryCoproductIso F G).hom.app a z