Documentation

Mathlib.CategoryTheory.Category.Basic

Categories #

Defines a category, as a type class parametrised by the type of objects.

Notations #

Introduces notations in the CategoryTheory scope

Users may like to add g ⊚ f for composition in the standard convention, using

local notation g ` ⊚ `:80 f:80 := category.comp f g    -- type as \oo

Porting note #

I am experimenting with using the aesop tactic as a replacement for tidy.

class CategoryTheory.CategoryStruct (obj : Type u) extends Quiver :
Type (max u (v + 1))

A preliminary structure on the way to defining a category, containing the data, but none of the axioms.

  • Hom : objobjType v
  • id : (X : obj) → X X

    The identity morphism on an object.

  • comp : {X Y Z : obj} → (X Y)(Y Z)(X Z)

    Composition of morphisms in a category, written f ≫ g.

Instances

    Notation for the identity morphism in a category.

    Equations
    Instances For

      Notation for composition of morphisms in a category.

      Equations
      Instances For

        Close the main goal with sorry if its type contains sorry, and fail otherwise.

        Equations
        Instances For

          Close the main goal with sorry if its type contains sorry, and fail otherwise.

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

            A thin wrapper for aesop which adds the CategoryTheory rule set and allows aesop to look through semireducible definitions when calling intros. This tactic fails when it is unable to solve the goal, making it suitable for use in auto-params.

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

              We also use aesop_cat? to pass along a Try this suggestion when using aesop_cat

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

                A variant of aesop_cat which does not fail when it is unable to solve the goal. Use this only for exploration! Nonterminal aesop is even worse than nonterminal simp.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  class CategoryTheory.Category (obj : Type u) extends CategoryTheory.CategoryStruct :
                  Type (max u (v + 1))

                  The typeclass Category C describes morphisms associated to objects of type C. The universe levels of the objects and morphisms are unconstrained, and will often need to be specified explicitly, as Category.{v} C. (See also LargeCategory and SmallCategory.)

                  See https://stacks.math.columbia.edu/tag/0014.

                  Instances
                    @[simp]

                    Identity morphisms are left identities for composition.

                    @[simp]

                    Identity morphisms are right identities for composition.

                    @[simp]

                    Composition in a category is associative.

                    @[reducible, inline]
                    abbrev CategoryTheory.LargeCategory (C : Type (u + 1)) :
                    Type (u + 1)

                    A LargeCategory has objects in one universe level higher than the universe level of the morphisms. It is useful for examples such as the category of types, or the category of groups, etc.

                    Equations
                    Instances For
                      @[reducible, inline]
                      abbrev CategoryTheory.SmallCategory (C : Type u) :
                      Type (u + 1)

                      A SmallCategory has objects and morphisms in the same universe level.

                      Equations
                      Instances For
                        theorem CategoryTheory.eq_whisker {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Y} (w : f = g) (h : Y Z) :

                        postcompose an equation between morphisms by another morphism

                        theorem CategoryTheory.whisker_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) {g : Y Z} {h : Y Z} (w : g = h) :

                        precompose an equation between morphisms by another morphism

                        Notation for whiskering an equation by a morphism (on the right). If f g : X ⟶ Y and w : f = g and h : Y ⟶ Z, then w =≫ h : f ≫ h = g ≫ h.

                        Equations
                        Instances For

                          Notation for whiskering an equation by a morphism (on the left). If g h : Y ⟶ Z and w : g = h and h : X ⟶ Y, then f ≫= w : f ≫ g = f ≫ h.

                          Equations
                          Instances For
                            theorem CategoryTheory.eq_of_comp_left_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} {g : X Y} (w : ∀ {Z : C} (h : Y Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) :
                            f = g
                            theorem CategoryTheory.eq_of_comp_right_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} {Z : C} {f : Y Z} {g : Y Z} (w : ∀ {X : C} (h : X Y), CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) :
                            f = g
                            theorem CategoryTheory.eq_of_comp_left_eq' {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) (g : X Y) (w : (fun {Z : C} (h : Y Z) => CategoryTheory.CategoryStruct.comp f h) = fun {Z : C} (h : Y Z) => CategoryTheory.CategoryStruct.comp g h) :
                            f = g
                            theorem CategoryTheory.eq_of_comp_right_eq' {C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} {Z : C} (f : Y Z) (g : Y Z) (w : (fun {X : C} (h : X Y) => CategoryTheory.CategoryStruct.comp h f) = fun {X : C} (h : X Y) => CategoryTheory.CategoryStruct.comp h g) :
                            f = g
                            theorem CategoryTheory.comp_ite {C : Type u} [CategoryTheory.Category.{v, u} C] {P : Prop} [Decidable P] {X : C} {Y : C} {Z : C} (f : X Y) (g : Y Z) (g' : Y Z) :
                            theorem CategoryTheory.ite_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {P : Prop} [Decidable P] {X : C} {Y : C} {Z : C} (f : X Y) (f' : X Y) (g : Y Z) :
                            theorem CategoryTheory.comp_dite {C : Type u} [CategoryTheory.Category.{v, u} C] {P : Prop} [Decidable P] {X : C} {Y : C} {Z : C} (f : X Y) (g : P(Y Z)) (g' : ¬P(Y Z)) :
                            CategoryTheory.CategoryStruct.comp f (if h : P then g h else g' h) = if h : P then CategoryTheory.CategoryStruct.comp f (g h) else CategoryTheory.CategoryStruct.comp f (g' h)
                            theorem CategoryTheory.dite_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {P : Prop} [Decidable P] {X : C} {Y : C} {Z : C} (f : P(X Y)) (f' : ¬P(X Y)) (g : Y Z) :
                            CategoryTheory.CategoryStruct.comp (if h : P then f h else f' h) g = if h : P then CategoryTheory.CategoryStruct.comp (f h) g else CategoryTheory.CategoryStruct.comp (f' h) g
                            class CategoryTheory.Epi {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :

                            A morphism f is an epimorphism if it can be cancelled when precomposed: f ≫ g = f ≫ h implies g = h.

                            See https://stacks.math.columbia.edu/tag/003B.

                            Instances
                              theorem CategoryTheory.Epi.left_cancellation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} [self : CategoryTheory.Epi f] {Z : C} (g : Y Z) (h : Y Z) :

                              A morphism f is an epimorphism if it can be cancelled when precomposed.

                              class CategoryTheory.Mono {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :

                              A morphism f is a monomorphism if it can be cancelled when postcomposed: g ≫ f = h ≫ f implies g = h.

                              See https://stacks.math.columbia.edu/tag/003B.

                              Instances

                                A morphism f is a monomorphism if it can be cancelled when postcomposed.

                                theorem CategoryTheory.mono_of_mono_fac {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} {h : X Z} [CategoryTheory.Mono h] (w : CategoryTheory.CategoryStruct.comp f g = h) :
                                theorem CategoryTheory.epi_of_epi_fac {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : Y Z} {h : X Z} [CategoryTheory.Epi h] (w : CategoryTheory.CategoryStruct.comp f g = h) :
                                Equations
                                • =
                                Equations
                                • =