Documentation

Mathlib.CategoryTheory.Discrete.SumsProducts

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 #

source
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.
Instances For
    source
    @[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✝ = eqToHom ⋯
    source
    @[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 = (CategoryStruct.id X.1, CategoryStruct.id X.2)
    source
    @[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 = ULift.rec (fun (down : PLift (X.as = Y.as)) => eqToHom ⋯) f
    source
    @[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 = (CategoryStruct.id X.1, CategoryStruct.id X.2)
    source
    @[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 })
    source
    @[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)
    source
    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.
    Instances For
      source
      @[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 }
      source
      @[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 = ULift.rec (fun (down : PLift (X.as = Y.as)) => eqToHom ⋯) f
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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 }
      source
      @[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
      source
      instance CategoryTheory.IsDiscrete.prod (C : Type u_1) [Category.{u_4, u_1} C] (D : Type u_3) [Category.{u_5, u_3} D] [IsDiscrete C] [IsDiscrete D] :
      IsDiscrete (C × D)

      A product of discrete categories is discrete.

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

      A product of discrete categories is discrete.