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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.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.

@[simp]

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

def CategoryTheory.FunctorToTypes.prod.fst {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} : CategoryTheory.FunctorToTypes.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.snd_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} : ∀ (x : C) (a : (CategoryTheory.FunctorToTypes.prod F G).obj x), CategoryTheory.FunctorToTypes.prod.snd.app x a = a.2

def CategoryTheory.FunctorToTypes.prod.snd {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} : CategoryTheory.FunctorToTypes.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.lift_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) (x : C) (y : F.obj x) : (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂).app x y = (τ₁.app x y, τ₂.app x y)

def CategoryTheory.FunctorToTypes.prod.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) : F ⟶ CategoryTheory.FunctorToTypes.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_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F ⟶ F₁) (τ₂ : F ⟶ F₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂) CategoryTheory.FunctorToTypes.prod.fst = τ₁

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.FunctorToTypes.binaryProductCone {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.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.binaryProductLimit_lift {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (s : CategoryTheory.Limits.BinaryFan F G) : (CategoryTheory.FunctorToTypes.binaryProductLimit F G).lift s = CategoryTheory.FunctorToTypes.prod.lift s.fst s.snd

def CategoryTheory.FunctorToTypes.binaryProductLimit {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Limits.IsLimit (CategoryTheory.FunctorToTypes.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 := ⋯ }

def CategoryTheory.FunctorToTypes.binaryProductLimitCone {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Limits.LimitCone (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : F ⨯ G ≅ CategoryTheory.FunctorToTypes.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.binaryProductIso F G).hom CategoryTheory.FunctorToTypes.prod.fst = CategoryTheory.Limits.prod.fst

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.FunctorToTypes.prodMk {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) : CategoryTheory.Limits.prod.fst.app a (CategoryTheory.FunctorToTypes.prodMk x y) = x

@[simp]

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

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

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.FunctorToTypes.binaryProductEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.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.

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

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

def CategoryTheory.FunctorToTypes.coprod {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.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.

@[simp]

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

def CategoryTheory.FunctorToTypes.coprod.inl {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} : F ⟶ CategoryTheory.FunctorToTypes.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.inr_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} : ∀ (x : C) (x_1 : G.obj x), CategoryTheory.FunctorToTypes.coprod.inr.app x x_1 = Sum.inr x_1

def CategoryTheory.FunctorToTypes.coprod.inr {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} : G ⟶ CategoryTheory.FunctorToTypes.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.desc_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) (a : C) (x : (CategoryTheory.FunctorToTypes.coprod F₁ F₂).obj a) : (CategoryTheory.FunctorToTypes.coprod.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) ⋯

def CategoryTheory.FunctorToTypes.coprod.desc {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) : CategoryTheory.FunctorToTypes.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_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F₁ ⟶ F) (τ₂ : F₂ ⟶ F) : CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inl (CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂) = τ₁

@[simp]

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

@[simp]

theorem CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : ∀ {X Y : C} (f : X ⟶ Y) (x : F.obj X ⊕ G.obj X), (CategoryTheory.FunctorToTypes.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (a : C) : (CategoryTheory.FunctorToTypes.binaryCoproductCocone F G).pt.obj a = (F.obj a ⊕ G.obj a)

@[simp]

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

def CategoryTheory.FunctorToTypes.binaryCoproductCocone {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.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.binaryCoproductColimit_desc {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (s : CategoryTheory.Limits.BinaryCofan F G) : (CategoryTheory.FunctorToTypes.binaryCoproductColimit F G).desc s = CategoryTheory.FunctorToTypes.coprod.desc s.inl s.inr

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

coprod F G is a colimit cocone.

Equations

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

def CategoryTheory.FunctorToTypes.binaryCoproductColimitCocone {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : F ⨿ G ≅ CategoryTheory.FunctorToTypes.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} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom = CategoryTheory.FunctorToTypes.coprod.inl

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.FunctorToTypes.coprodInl {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.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)

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.FunctorToTypes.binaryCoproductEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.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.