Sums and products of discrete categories.

This file shows that binary products and binary sums of discrete categories are also discrete, both in the form of explicit equivalences and through the IsDiscrete typeclass.

Main declarations

• Discrete.productEquiv: The equivalence of categories between Discrete (J × K) and Discrete J × Discrete K
• Discrete.sumEquiv: The equivalence of categories between Discrete (J ⊕ K) and Discrete J ⊕ Discrete K.
• IsDiscrete.prod: an IsDiscrete instance on the product of two discrete categories.
• IsDiscrete.sum: an IsDiscrete instance on the sum of two discrete categories.

def CategoryTheory.Discrete.productEquiv {J : Type u_1} {K : Type u_2} : Discrete (J × K) ≌ Discrete J × Discrete K

The discrete category on a product is equivalent to the product of the discrete categories.

Equations

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

@[simp]

theorem CategoryTheory.Discrete.productEquiv_functor_obj {J : Type u_1} {K : Type u_2} (a✝ : Discrete (J × K)) : productEquiv.functor.obj a✝ = ({ as := a✝.as.1 }, { as := a✝.as.2 })

@[simp]

theorem CategoryTheory.Discrete.productEquiv_inverse_obj_as {J : Type u_1} {K : Type u_2} (x✝ : Discrete J × Discrete K) : (productEquiv.inverse.obj x✝).as = (x✝.1.as, x✝.2.as)

@[simp]

theorem CategoryTheory.Discrete.productEquiv_counitIso_inv_app {J : Type u_1} {K : Type u_2} (X : Discrete J × Discrete K) : productEquiv.counitIso.inv.app X = Prod.mkHom (CategoryStruct.id X.1) (CategoryStruct.id X.2)

@[simp]

theorem CategoryTheory.Discrete.productEquiv_inverse_map {J : Type u_1} {K : Type u_2} {X✝ Y✝ : Discrete J × Discrete K} (x✝ : X✝ ⟶ Y✝) : productEquiv.inverse.map x✝ = match x✝ with | (f₁, f₂) => eqToHom ⋯

@[simp]

theorem CategoryTheory.Discrete.productEquiv_functor_map {J : Type u_1} {K : Type u_2} {X Y : Discrete (J × K)} (f : X ⟶ Y) : productEquiv.functor.map f = Hom.rec (fun (eq : X.as = Y.as) => eqToHom ⋯) f

@[simp]

theorem CategoryTheory.Discrete.productEquiv_counitIso_hom_app {J : Type u_1} {K : Type u_2} (X : Discrete J × Discrete K) : productEquiv.counitIso.hom.app X = Prod.mkHom (CategoryStruct.id X.1) (CategoryStruct.id X.2)

def CategoryTheory.Discrete.sumEquiv {J : Type u_1} {K : Type u_2} : Discrete (J ⊕ K) ≌ Discrete J ⊕ Discrete K

The discrete category on a sum is equivalent to the sum of the discrete categories.

Equations

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

@[simp]

theorem CategoryTheory.Discrete.sumEquiv_counitIso_inv_app {J : Type u_1} {K : Type u_2} (X : Discrete J ⊕ Discrete K) : sumEquiv.counitIso.inv.app X = (match X with | Sum.inl x => Iso.refl (Sum.inl x) | Sum.inr x => Iso.refl (Sum.inr x)).inv

@[simp]

theorem CategoryTheory.Discrete.sumEquiv_inverse_obj {J : Type u_1} {K : Type u_2} (x✝ : Discrete J ⊕ Discrete K) : sumEquiv.inverse.obj x✝ = match x✝ with | Sum.inl X => { as := Sum.inl X.as } | Sum.inr X => { as := Sum.inr X.as }

@[simp]

theorem CategoryTheory.Discrete.sumEquiv_counitIso_hom_app {J : Type u_1} {K : Type u_2} (X : Discrete J ⊕ Discrete K) : sumEquiv.counitIso.hom.app X = (match X with | Sum.inl x => Iso.refl (Sum.inl x) | Sum.inr x => Iso.refl (Sum.inr x)).hom

@[simp]

theorem CategoryTheory.Discrete.sumEquiv_functor_map {J : Type u_1} {K : Type u_2} {X Y : Discrete (J ⊕ K)} (f : X ⟶ Y) : sumEquiv.functor.map f = Hom.rec (fun (eq : X.as = Y.as) => eqToHom ⋯) f

@[simp]

theorem CategoryTheory.Discrete.sumEquiv_functor_obj {J : Type u_1} {K : Type u_2} (a✝ : Discrete (J ⊕ K)) : sumEquiv.functor.obj a✝ = match a✝.as with | Sum.inl j => Sum.inl { as := j } | Sum.inr k => Sum.inr { as := k }

@[simp]

theorem CategoryTheory.Discrete.sumEquiv_unitIso_inv_app {J : Type u_1} {K : Type u_2} (X : Discrete (J ⊕ K)) : sumEquiv.unitIso.inv.app X = (match X.as with | Sum.inl x => Iso.refl { as := Sum.inl x } | Sum.inr x => Iso.refl { as := Sum.inr x }).inv

@[simp]

theorem CategoryTheory.Discrete.sumEquiv_unitIso_hom_app {J : Type u_1} {K : Type u_2} (X : Discrete (J ⊕ K)) : sumEquiv.unitIso.hom.app X = (match X.as with | Sum.inl x => Iso.refl { as := Sum.inl x } | Sum.inr x => Iso.refl { as := Sum.inr x }).hom

@[simp]

theorem CategoryTheory.Discrete.sumEquiv_inverse_map {J : Type u_1} {K : Type u_2} {X Y : Discrete J ⊕ Discrete K} (f : X ⟶ Y) : sumEquiv.inverse.map f = Sum.homInduction (fun (x x_1 : Discrete J) (f : x ⟶ x_1) => (functor fun (t : J) => { as := Sum.inl t }).map f) (fun (x x_1 : Discrete K) (g : x ⟶ x_1) => (functor fun (t : K) => { as := Sum.inr t }).map g) f

instance CategoryTheory.IsDiscrete.prod (C : Type u_1) [Category.{v_1, u_1} C] (D : Type u_3) [Category.{v_3, u_3} D] [IsDiscrete C] [IsDiscrete D] : IsDiscrete (C × D)

A product of discrete categories is discrete.

instance CategoryTheory.IsDiscrete.sum (C : Type u_1) (C' : Type u_2) [Category.{v_1, u_1} C] [Category.{v_2, u_2} C'] [IsDiscrete C] [IsDiscrete C'] : IsDiscrete (C ⊕ C')

A sum of discrete categories is discrete.