Products in Type

We describe arbitrary products in the category of types, as well as binary products, and the terminal object.

instance CategoryTheory.Limits.Types.instHasProductsType : HasProducts (Type v)

@[simp]

theorem CategoryTheory.Limits.Types.pi_lift_π_apply {β : Type v} [Small.{u, v} β] (f : β → Type u) {P : Type u} (s : (b : β) → P ⟶ f b) (b : β) (x : P) : Pi.π f b (Pi.lift s x) = s b x

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift.

theorem CategoryTheory.Limits.Types.pi_lift_π_apply' {β : Type v} (f : β → Type v) {P : Type v} (s : (b : β) → P ⟶ f b) (b : β) (x : P) : Pi.π f b (Pi.lift s x) = s b x

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift, with specialized universes.

theorem CategoryTheory.Limits.Types.pi_map_π_apply {β : Type v} [Small.{u, v} β] {f g : β → Type u} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ᶜ f) : Pi.π g b (Pi.map α x) = α b (Pi.π f b x)

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map.

theorem CategoryTheory.Limits.Types.pi_map_π_apply' {β : Type v} {f g : β → Type v} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ᶜ f) : Pi.π g b (Pi.map α x) = α b (Pi.π f b x)

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map, with specialized universes.

def CategoryTheory.Limits.Types.terminalLimitCone : LimitCone (Functor.empty (Type u))

The category of types has PUnit as a terminal object.

Equations

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

noncomputable def CategoryTheory.Limits.Types.terminalIso : ⊤_ Type u ≅ PUnit.{u + 1}

The terminal object in Type u is PUnit.

Equations

• CategoryTheory.Limits.Types.terminalIso = CategoryTheory.Limits.limit.isoLimitCone CategoryTheory.Limits.Types.terminalLimitCone

noncomputable def CategoryTheory.Limits.Types.isTerminalPunit : IsTerminal PUnit.{u + 1}

The terminal object in Type u is PUnit.

Equations

• CategoryTheory.Limits.Types.isTerminalPunit = CategoryTheory.Limits.terminalIsTerminal.ofIso CategoryTheory.Limits.Types.terminalIso

noncomputable instance CategoryTheory.Limits.Types.instInhabitedTerminalType : Inhabited (⊤_ Type u)

Equations

• CategoryTheory.Limits.Types.instInhabitedTerminalType = { default := CategoryTheory.Limits.terminal.from (ULift.{?u.8, 0} (Fin 1)) { down := 0 } }

instance CategoryTheory.Limits.Types.instSubsingletonTerminalType : Subsingleton (⊤_ Type u)

noncomputable instance CategoryTheory.Limits.Types.instUniqueTerminalType : Unique (⊤_ Type u)

Equations

• CategoryTheory.Limits.Types.instUniqueTerminalType = Unique.mk' (⊤_ Type ?u.8)

noncomputable def CategoryTheory.Limits.Types.isTerminalEquivUnique (X : Type u) : IsTerminal X ≃ Unique X

A type is terminal if and only if it contains exactly one element.

Equations

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

noncomputable def CategoryTheory.Limits.Types.isTerminalEquivIsoPUnit (X : Type u) : IsTerminal X ≃ (X ≅ PUnit.{u + 1})

A type is terminal if and only if it is isomorphic to PUnit.

Equations

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

def CategoryTheory.Limits.Types.binaryProductCone (X Y : Type u) : BinaryFan X Y

The product type X × Y forms a cone for the binary product of X and Y.

Equations

• CategoryTheory.Limits.Types.binaryProductCone X Y = CategoryTheory.Limits.BinaryFan.mk Prod.fst Prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_pt (X Y : Type u) : (binaryProductCone X Y).pt = (X × Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_fst (X Y : Type u) : (binaryProductCone X Y).fst = _root_.Prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_snd (X Y : Type u) : (binaryProductCone X Y).snd = _root_.Prod.snd

def CategoryTheory.Limits.Types.binaryProductLimit (X Y : Type u) : IsLimit (binaryProductCone X Y)

The product type X × Y is a binary product for X and Y.

Equations

• CategoryTheory.Limits.Types.binaryProductLimit X Y = { lift := fun (s : CategoryTheory.Limits.BinaryFan X Y) (x : s.pt) => (s.fst x, s.snd x), fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimit_lift (X Y : Type u) (s : BinaryFan X Y) (x : s.pt) : (binaryProductLimit X Y).lift s x = (s.fst x, s.snd x)

def CategoryTheory.Limits.Types.binaryProductLimitCone (X Y : Type u) : LimitCone (pair X Y)

The category of types has X × Y, the usual Cartesian product, as the binary product of X and Y.

Equations

• CategoryTheory.Limits.Types.binaryProductLimitCone X Y = { cone := CategoryTheory.Limits.Types.binaryProductCone X Y, isLimit := CategoryTheory.Limits.Types.binaryProductLimit X Y }

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimitCone_isLimit (X Y : Type u) : (binaryProductLimitCone X Y).isLimit = binaryProductLimit X Y

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimitCone_cone (X Y : Type u) : (binaryProductLimitCone X Y).cone = binaryProductCone X Y

noncomputable def CategoryTheory.Limits.Types.binaryProductIso (X Y : Type u) : X ⨯ Y ≅ X × Y

The categorical binary product in Type u is Cartesian product.

Equations

• CategoryTheory.Limits.Types.binaryProductIso X Y = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst (X Y : Type u) : CategoryStruct.comp (binaryProductIso X Y).hom _root_.Prod.fst = prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst_apply (X Y : Type u) (x : X ⨯ Y) : ((binaryProductIso X Y).hom x).1 = prod.fst x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd (X Y : Type u) : CategoryStruct.comp (binaryProductIso X Y).hom _root_.Prod.snd = prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd_apply (X Y : Type u) (x : X ⨯ Y) : ((binaryProductIso X Y).hom x).2 = prod.snd x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst (X Y : Type u) : CategoryStruct.comp (binaryProductIso X Y).inv prod.fst = _root_.Prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst_apply (X Y : Type u) (x : X × Y) : prod.fst ((binaryProductIso X Y).inv x) = x.1

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd (X Y : Type u) : CategoryStruct.comp (binaryProductIso X Y).inv prod.snd = _root_.Prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd_apply (X Y : Type u) (x : X × Y) : prod.snd ((binaryProductIso X Y).inv x) = x.2

def CategoryTheory.Limits.Types.binaryProductFunctor : Functor (Type u) (Functor (Type u) (Type u))

The functor which sends X, Y to the product type X × Y.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_obj_map (X : Type u) {x✝ Y₂ : Type u} (f : x✝ ⟶ Y₂) (a✝ : (BinaryFan.mk _root_.Prod.fst (CategoryStruct.comp _root_.Prod.snd f)).pt) : (binaryProductFunctor.obj X).map f a✝ = (binaryProductLimit X Y₂).lift (BinaryFan.mk _root_.Prod.fst (CategoryStruct.comp _root_.Prod.snd f)) a✝

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_map_app {X₁ X₂ : Type u} (f : X₁ ⟶ X₂) (Y : Type u) (a✝ : (BinaryFan.mk (CategoryStruct.comp _root_.Prod.fst f) _root_.Prod.snd).pt) : (binaryProductFunctor.map f).app Y a✝ = (binaryProductLimit X₂ Y).lift (BinaryFan.mk (CategoryStruct.comp _root_.Prod.fst f) _root_.Prod.snd) a✝

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_obj_obj (X Y : Type u) : (binaryProductFunctor.obj X).obj Y = (X × Y)

noncomputable def CategoryTheory.Limits.Types.binaryProductIsoProd : binaryProductFunctor ≅ prod.functor

The product functor given by the instance HasBinaryProducts (Type u) is isomorphic to the explicit binary product functor given by the product type.

Equations

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

def CategoryTheory.Limits.Types.productLimitCone {J : Type v} (F : J → Type (max v u)) : LimitCone (Discrete.functor F)

The category of types has Π j, f j as the product of a type family f : J → Type max v u.

Equations

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

noncomputable def CategoryTheory.Limits.Types.productIso {J : Type v} (F : J → Type (max v u)) : ∏ᶜ F ≅ (j : J) → F j

The categorical product in Type max v u is the type-theoretic product Π j, F j.

Equations

• CategoryTheory.Limits.Types.productIso F = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.productLimitCone F)

@[simp]

theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval {J : Type v} (F : J → Type (max v u)) (j : J) : (CategoryStruct.comp (productIso F).hom fun (f : (j : J) → F j) => f j) = Pi.π F j

@[simp]

theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply {J : Type v} (F : J → Type (max v u)) (j : J) (x : ∏ᶜ F) : (productIso F).hom x j = Pi.π F j x

@[simp]

theorem CategoryTheory.Limits.Types.productIso_inv_comp_π {J : Type v} (F : J → Type (max v u)) (j : J) : CategoryStruct.comp (productIso F).inv (Pi.π F j) = fun (f : (j : J) → F j) => f j

@[simp]

theorem CategoryTheory.Limits.Types.productIso_inv_comp_π_apply {J : Type v} (F : J → Type (max v u)) (j : J) (x : (j : J) → F j) : Pi.π F j ((productIso F).inv x) = x j

noncomputable def CategoryTheory.Limits.Types.Small.productLimitCone {J : Type v} (F : J → Type u) [Small.{u, v} J] : LimitCone (Discrete.functor F)

A variant of productLimitCone using a Small hypothesis rather than a function to Type.

Equations

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

noncomputable def CategoryTheory.Limits.Types.Small.productIso {J : Type v} (F : J → Type u) [Small.{u, v} J] : ∏ᶜ F ≅ Shrink.{u, max u v} ((j : J) → F j)

The categorical product in Type u indexed in Type v is the type-theoretic product Π j, F j, after shrinking back to Type u.

Equations

• CategoryTheory.Limits.Types.Small.productIso F = CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.Small.productLimitCone F)

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) : (CategoryStruct.comp (productIso F).hom fun (f : Shrink.{u, max u v} ((j : J) → F j)) => (equivShrink ((j : J) → F j)).symm f j) = Pi.π F j

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_hom_comp_eval_apply {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) (x : ∏ᶜ F) : (equivShrink ((j : J) → F j)).symm ((productIso F).hom x) j = Pi.π F j x

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_inv_comp_π {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) : CategoryStruct.comp (productIso F).inv (Pi.π F j) = fun (f : Shrink.{u, max u v} ((j : J) → F j)) => (equivShrink ((j : J) → F j)).symm f j

@[simp]

theorem CategoryTheory.Limits.Types.Small.productIso_inv_comp_π_apply {J : Type v} (F : J → Type u) [Small.{u, v} J] (j : J) (x : Shrink.{u, max u v} ((j : J) → F j)) : Pi.π F j ((productIso F).inv x) = (equivShrink ((j : J) → F j)).symm x j