Discrete categories

We define Discrete α as a structure containing a term a : α for any type α, and use this type alias to provide a SmallCategory instance whose only morphisms are the identities.

There is an annoying technical difficulty that it has turned out to be inconvenient to allow categories with morphisms living in Prop, so instead of defining X ⟶ Y in Discrete α as X = Y, one might define it as PLift (X = Y). In fact, to allow Discrete α to be a SmallCategory (i.e. with morphisms in the same universe as the objects), we actually define the hom type X ⟶ Y as ULift (PLift (X = Y)).

Discrete.functor promotes a function f : I → C (for any category C) to a functor Discrete.functor f : Discrete I ⥤ C.

Similarly, Discrete.natTrans and Discrete.natIso promote I-indexed families of morphisms, or I-indexed families of isomorphisms to natural transformations or natural isomorphism.

We show equivalences of types are the same as (categorical) equivalences of the corresponding discrete categories.

structure CategoryTheory.Discrete (α : Type u₁) : Type u₁

A wrapper for promoting any type to a category, with the only morphisms being equalities.

• as : α

  A wrapper for promoting any type to a category, with the only morphisms being equalities.

theorem CategoryTheory.Discrete.ext {α : Type u₁} {x y : Discrete α} (as : x.as = y.as) : x = y

theorem CategoryTheory.Discrete.ext_iff {α : Type u₁} {x y : Discrete α} : x = y ↔ x.as = y.as

@[simp]

theorem CategoryTheory.Discrete.mk_as {α : Type u₁} (X : Discrete α) : { as := X.as } = X

def CategoryTheory.discreteEquiv {α : Type u₁} : Discrete α ≃ α

Discrete α is equivalent to the original type α.

@[simp]

theorem CategoryTheory.discreteEquiv_symm_apply_as {α : Type u₁} (as : α) : (discreteEquiv.symm as).as = as

@[simp]

theorem CategoryTheory.discreteEquiv_apply {α : Type u₁} (self : Discrete α) : discreteEquiv self = self.as

@[implicit_reducible]

instance CategoryTheory.instDecidableEqDiscrete {α : Type u₁} [DecidableEq α] : DecidableEq (Discrete α)

@[implicit_reducible]

instance CategoryTheory.discreteCategory (α : Type u₁) : SmallCategory (Discrete α)

The "Discrete" category on a type, whose morphisms are equalities.

Because we do not allow morphisms in Prop (only in Type), somewhat annoyingly we have to define X ⟶ Y as ULift (PLift (X = Y)).

@[implicit_reducible]

instance CategoryTheory.Discrete.instInhabited {α : Type u₁} [Inhabited α] : Inhabited (Discrete α)

instance CategoryTheory.Discrete.instSubsingleton {α : Type u₁} [Subsingleton α] : Subsingleton (Discrete α)

instance CategoryTheory.Discrete.instSubsingletonDiscreteHom {α : Type u₁} (X Y : Discrete α) : Subsingleton (X ⟶ Y)

def CategoryTheory.Discrete.tacticDiscrete_cases : Lean.ParserDescr

A simple tactic to run cases on any Discrete α hypotheses.

def CategoryTheory.Discrete.discreteCases : Lean.Elab.Tactic.TacticM Unit

Use:

attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
  CategoryTheory.Discrete.discreteCases

to locally give cat_disch the ability to call cases on Discrete and (_ : Discrete _) ⟶ (_ : Discrete _) hypotheses.

@[implicit_reducible]

instance CategoryTheory.Discrete.instUnique {α : Type u₁} [Unique α] : Unique (Discrete α)

theorem CategoryTheory.Discrete.eq_of_hom {α : Type u₁} {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as

Extract the equation from a morphism in a discrete category.

@[reducible, inline]

abbrev CategoryTheory.Discrete.eqToHom {α : Type u₁} {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y

Promote an equation between the wrapped terms in X Y : Discrete α to a morphism X ⟶ Y in the discrete category.

@[reducible, inline]

abbrev CategoryTheory.Discrete.eqToIso {α : Type u₁} {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y

Promote an equation between the wrapped terms in X Y : Discrete α to an isomorphism X ≅ Y in the discrete category.

@[reducible, inline]

abbrev CategoryTheory.Discrete.eqToHom' {α : Type u₁} {a b : α} (h : a = b) : { as := a } ⟶ { as := b }

A variant of eqToHom that lifts terms to the discrete category.

@[reducible, inline]

abbrev CategoryTheory.Discrete.eqToIso' {α : Type u₁} {a b : α} (h : a = b) : { as := a } ≅ { as := b }

A variant of eqToIso that lifts terms to the discrete category.

@[simp]

theorem CategoryTheory.Discrete.id_def {α : Type u₁} (X : Discrete α) : { down := { down := ⋯ } } = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Discrete.id_def' {α : Type u₁} (X : α) : { down := { down := ⋯ } } = CategoryStruct.id { as := X }

instance CategoryTheory.Discrete.instIsIso {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f

def CategoryTheory.Discrete.functor {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) : Functor (Discrete I) C

Any function I → C gives a functor Discrete I ⥤ C.

@[simp]

theorem CategoryTheory.Discrete.functor_obj {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (i : I) : (functor F).obj { as := i } = F i

theorem CategoryTheory.Discrete.functor_map {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i) : (functor F).map f = CategoryStruct.id (F i.as)

@[simp]

theorem CategoryTheory.Discrete.functor_obj_eq_as {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (X : Discrete I) : (functor F).obj X = F X.as

theorem CategoryTheory.Discrete.functor_ext {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {G F : Functor (Discrete I) C} (h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }) : G = F

theorem CategoryTheory.Discrete.functor_ext_iff {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {G F : Functor (Discrete I) C} : G = F ↔ ∀ (i : I), G.obj { as := i } = F.obj { as := i }

def CategoryTheory.Discrete.functorComp {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) : functor (f ∘ g) ≅ (functor (mk ∘ g)).comp (functor f)

The discrete functor induced by a composition of maps can be written as a composition of two discrete functors.

@[simp]

theorem CategoryTheory.Discrete.functorComp_hom_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : Discrete I) : (functorComp f g).hom.app X = CategoryStruct.id (f (g X.as))

@[simp]

theorem CategoryTheory.Discrete.functorComp_inv_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : Discrete I) : (functorComp f g).inv.app X = CategoryStruct.id (f (g X.as))

def CategoryTheory.Discrete.natTrans {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {F G : Functor (Discrete I) C} (f : (i : Discrete I) → F.obj i ⟶ G.obj i) : F ⟶ G

For functors out of a discrete category, a natural transformation is just a collection of maps, as the naturality squares are trivial.

@[simp]

theorem CategoryTheory.Discrete.natTrans_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {F G : Functor (Discrete I) C} (f : (i : Discrete I) → F.obj i ⟶ G.obj i) (i : Discrete I) : (natTrans f).app i = f i

def CategoryTheory.Discrete.natIso {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {F G : Functor (Discrete I) C} (f : (i : Discrete I) → F.obj i ≅ G.obj i) : F ≅ G

For functors out of a discrete category, a natural isomorphism is just a collection of isomorphisms, as the naturality squares are trivial.

@[simp]

theorem CategoryTheory.Discrete.natIso_hom_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {F G : Functor (Discrete I) C} (f : (i : Discrete I) → F.obj i ≅ G.obj i) (X : Discrete I) : (natIso f).hom.app X = (f X).hom

@[simp]

theorem CategoryTheory.Discrete.natIso_inv_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {F G : Functor (Discrete I) C} (f : (i : Discrete I) → F.obj i ≅ G.obj i) (X : Discrete I) : (natIso f).inv.app X = (f X).inv

instance CategoryTheory.Discrete.instIsIsoFunctorNatTrans {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u_1} {F G : Functor (Discrete I) C} (f : (i : Discrete I) → F.obj i ⟶ G.obj i) [∀ (i : Discrete I), IsIso (f i)] : IsIso (natTrans f)

@[simp]

theorem CategoryTheory.Discrete.natIso_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {F G : Functor (Discrete I) C} (f : (i : Discrete I) → F.obj i ≅ G.obj i) (i : Discrete I) : (natIso f).app i = f i

def CategoryTheory.Discrete.natIsoFunctor {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {F : Functor (Discrete I) C} : F ≅ functor (F.obj ∘ mk)

Every functor F from a discrete category is naturally isomorphic (actually, equal) to Discrete.functor (F.obj).

@[simp]

theorem CategoryTheory.Discrete.natIsoFunctor_inv_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {F : Functor (Discrete I) C} (X : Discrete I) : natIsoFunctor.inv.app X = CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Discrete.natIsoFunctor_hom_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {F : Functor (Discrete I) C} (X : Discrete I) : natIsoFunctor.hom.app X = CategoryStruct.id (F.obj X)

def CategoryTheory.Discrete.compNatIsoDiscrete {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [Category.{v₃, u₃} D] (F : I → C) (G : Functor C D) : (functor F).comp G ≅ functor (G.obj ∘ F)

Composing Discrete.functor F with another functor G amounts to composing F with G.obj

@[simp]

theorem CategoryTheory.Discrete.compNatIsoDiscrete_hom_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [Category.{v₃, u₃} D] (F : I → C) (G : Functor C D) (X : Discrete I) : (compNatIsoDiscrete F G).hom.app X = CategoryStruct.id (G.obj (F X.as))

@[simp]

theorem CategoryTheory.Discrete.compNatIsoDiscrete_inv_app {C : Type u₂} [Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [Category.{v₃, u₃} D] (F : I → C) (G : Functor C D) (X : Discrete I) : (compNatIsoDiscrete F G).inv.app X = CategoryStruct.id (G.obj (F X.as))

def CategoryTheory.Discrete.equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J

We can promote a type-level Equiv to an equivalence between the corresponding discrete categories.

@[simp]

theorem CategoryTheory.Discrete.equivalence_functor {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (equivalence e).functor = functor (mk ∘ ⇑e)

@[simp]

theorem CategoryTheory.Discrete.equivalence_inverse {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (equivalence e).inverse = functor (mk ∘ ⇑e.symm)

@[simp]

theorem CategoryTheory.Discrete.equivalence_unitIso {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (equivalence e).unitIso = natIso fun (i : Discrete I) => eqToIso ⋯

@[simp]

theorem CategoryTheory.Discrete.equivalence_counitIso {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (equivalence e).counitIso = natIso fun (j : Discrete J) => eqToIso ⋯

def CategoryTheory.Discrete.equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β

We can convert an equivalence of discrete categories to a type-level Equiv.

@[simp]

theorem CategoryTheory.Discrete.equivOfEquivalence_apply {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) (a✝ : α) : (equivOfEquivalence h) a✝ = (as ∘ h.functor.obj ∘ mk) a✝

@[simp]

theorem CategoryTheory.Discrete.equivOfEquivalence_symm_apply {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) (a✝ : β) : (equivOfEquivalence h).symm a✝ = (as ∘ h.inverse.obj ∘ mk) a✝

def CategoryTheory.Discrete.opposite (α : Type u₁) : (Discrete α)ᵒᵖ ≌ Discrete α

A discrete category is equivalent to its opposite category.

@[simp]

theorem CategoryTheory.Discrete.opposite_functor_obj_as (α : Type u₁) (X : (Discrete α)ᵒᵖ) : ((Discrete.opposite α).functor.obj X).as = (Opposite.unop X).as

@[simp]

theorem CategoryTheory.Discrete.opposite_inverse_obj (α : Type u₁) (a✝ : Discrete α) : (Discrete.opposite α).inverse.obj a✝ = Opposite.op a✝

@[simp]

theorem CategoryTheory.Discrete.functor_map_id {J : Type v₁} {C : Type u₂} [Category.{v₂, u₂} C] (F : Functor (Discrete J) C) {j : Discrete J} (f : j ⟶ j) : F.map f = CategoryStruct.id (F.obj j)

@[simp]

theorem CategoryTheory.Discrete.forall {α : Type u_1} {p : Discrete α → Prop} : (∀ (a : Discrete α), p a) ↔ ∀ (a' : α), p { as := a' }

@[simp]

theorem CategoryTheory.Discrete.exists {α : Type u_1} {p : Discrete α → Prop} : (∃ (a : Discrete α), p a) ↔ ∃ (a' : α), p { as := a' }

def CategoryTheory.piEquivalenceFunctorDiscrete (J : Type u₂) (C : Type u₁) [Category.{v₁, u₁} C] : J → C ≌ Functor (Discrete J) C

The equivalence of categories (J → C) ≌ (Discrete J ⥤ C).

@[simp]

theorem CategoryTheory.piEquivalenceFunctorDiscrete_unitIso (J : Type u₂) (C : Type u₁) [Category.{v₁, u₁} C] : (piEquivalenceFunctorDiscrete J C).unitIso = Iso.refl (Functor.id (J → C))

@[simp]

theorem CategoryTheory.piEquivalenceFunctorDiscrete_counitIso (J : Type u₂) (C : Type u₁) [Category.{v₁, u₁} C] : (piEquivalenceFunctorDiscrete J C).counitIso = NatIso.ofComponents (fun (F : Functor (Discrete J) C) => NatIso.ofComponents (fun (x : Discrete J) => Iso.refl ((({ obj := fun (F : Functor (Discrete J) C) (j : J) => F.obj { as := j }, map := fun {X Y : Functor (Discrete J) C} (f : X ⟶ Y) (j : J) => f.app { as := j }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (F : J → C) => Discrete.functor F, map := fun {X Y : J → C} (f : X ⟶ Y) => Discrete.natTrans fun (j : Discrete J) => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).obj x)) ⋯) ⋯

@[simp]

theorem CategoryTheory.piEquivalenceFunctorDiscrete_functor_obj (J : Type u₂) (C : Type u₁) [Category.{v₁, u₁} C] (F : J → C) : (piEquivalenceFunctorDiscrete J C).functor.obj F = Discrete.functor F

@[simp]

theorem CategoryTheory.piEquivalenceFunctorDiscrete_inverse_map (J : Type u₂) (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Functor (Discrete J) C} (f : X✝ ⟶ Y✝) (j : J) : (piEquivalenceFunctorDiscrete J C).inverse.map f j = f.app { as := j }

@[simp]

theorem CategoryTheory.piEquivalenceFunctorDiscrete_functor_map (J : Type u₂) (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : J → C} (f : X✝ ⟶ Y✝) : (piEquivalenceFunctorDiscrete J C).functor.map f = Discrete.natTrans fun (j : Discrete J) => f j.as

@[simp]

theorem CategoryTheory.piEquivalenceFunctorDiscrete_inverse_obj (J : Type u₂) (C : Type u₁) [Category.{v₁, u₁} C] (F : Functor (Discrete J) C) (j : J) : (piEquivalenceFunctorDiscrete J C).inverse.obj F j = F.obj { as := j }

class CategoryTheory.IsDiscrete (C : Type u_1) [Category.{v_1, u_1} C] : Prop

A category is discrete when there is at most one morphism between two objects, in which case they are equal.

• subsingleton (X Y : C) : Subsingleton (X ⟶ Y)
• eq_of_hom {X Y : C} (f : X ⟶ Y) : X = Y

instance CategoryTheory.Discrete.isDiscrete (C : Type u_1) : IsDiscrete (Discrete C)

theorem CategoryTheory.obj_ext_of_isDiscrete {C : Type u_1} [Category.{v_1, u_1} C] [IsDiscrete C] {X Y : C} (f : X ⟶ Y) : X = Y

instance CategoryTheory.isIso_of_isDiscrete {C : Type u_1} [Category.{v_1, u_1} C] [IsDiscrete C] {X Y : C} (f : X ⟶ Y) : IsIso f

instance CategoryTheory.instIsDiscreteOpposite {C : Type u_1} [Category.{v_1, u_1} C] [IsDiscrete C] : IsDiscrete Cᵒᵖ