Categories

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

Notations

Introduces notations

• X ⟶ Y⟶ Y for the morphism spaces (type as \hom),
• 𝟙 X for the identity morphism on X (type as \b1),
• f ≫ g≫ g for composition in the 'arrows' convention (type as \gg).

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

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

Porting note

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

ink

def Std.Tactic.Ext.extCore' : Lean.Elab.Tactic.TacticM Unit

A wrapper for ext that will fail if it does not make progress.

Equations

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

ink

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

• The identity morphism on an object.

  id : (X : obj) → X ⟶ X

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

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

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

ink

def CategoryTheory.«term𝟙» : Lean.ParserDescr

Notation for the identity morphism in a category.

Equations

• CategoryTheory.«term𝟙» = Lean.ParserDescr.node `CategoryTheory.term𝟙 1024 (Lean.ParserDescr.symbol "𝟙")

ink

def CategoryTheory.«term_≫_» : Lean.TrailingParserDescr

Notation for composition of morphisms in a category.

Equations

• CategoryTheory.«term_≫_» = Lean.ParserDescr.trailingNode `CategoryTheory.term_≫_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≫ ") (Lean.ParserDescr.cat `term 80))

ink

def CategoryTheory.aesop_cat : Lean.ParserDescr

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.

ink

def CategoryTheory.aesop_cat_nonterminal : Lean.ParserDescr

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.

ink

class CategoryTheory.Category (obj : Type u) extends CategoryTheory.CategoryStruct : Type (maxu(v+1))

• Identity morphisms are left identities for composition.

  id_comp : autoParam (∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f) _auto✝

• Identity morphisms are right identities for composition.

  comp_id : autoParam (∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f) _auto✝

• Composition in a category is associative.

  assoc : autoParam (∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h) _auto✝

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.

ink

@[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

• CategoryTheory.LargeCategory C = CategoryTheory.Category C

ink

@[inline]

abbrev CategoryTheory.SmallCategory (C : Type u) : Type (u+1)

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

Equations

• CategoryTheory.SmallCategory C = CategoryTheory.Category C

ink

theorem CategoryTheory.eq_whisker {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : X ⟶ Y} (w : f = g) (h : Y ⟶ Z) : f ≫ h = g ≫ h

postcompose an equation between morphisms by another morphism

ink

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

precompose an equation between morphisms by another morphism

ink

def CategoryTheory.«term_=≫_» : Lean.TrailingParserDescr

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

Equations

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

ink

def CategoryTheory.«term_≫=_» : Lean.TrailingParserDescr

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

Equations

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

ink

theorem CategoryTheory.eq_of_comp_left_eq {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} (w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) : f = g

ink

theorem CategoryTheory.eq_of_comp_right_eq {C : Type u} [inst : CategoryTheory.Category C] {Y : C} {Z : C} {f : Y ⟶ Z} {g : Y ⟶ Z} (w : ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g) : f = g

ink

theorem CategoryTheory.eq_of_comp_left_eq' {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) (w : (fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h) : f = g

ink

theorem CategoryTheory.eq_of_comp_right_eq' {C : Type u} [inst : CategoryTheory.Category C] {Y : C} {Z : C} (f : Y ⟶ Z) (g : Y ⟶ Z) (w : (fun {X} h => h ≫ f) = fun {X} h => h ≫ g) : f = g

ink

theorem CategoryTheory.id_of_comp_left_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} (f : X ⟶ X) (w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g) : f = 𝟙 X

ink

theorem CategoryTheory.id_of_comp_right_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} (f : X ⟶ X) (w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) : f = 𝟙 X

ink

theorem CategoryTheory.comp_ite {C : Type u} [inst : CategoryTheory.Category C] {P : Prop} [inst : Decidable P] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (g' : Y ⟶ Z) : (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'

ink

theorem CategoryTheory.ite_comp {C : Type u} [inst : CategoryTheory.Category C] {P : Prop} [inst : Decidable P] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (f' : X ⟶ Y) (g : Y ⟶ Z) : (if P then f else f') ≫ g = if P then f ≫ g else f' ≫ g

ink

theorem CategoryTheory.comp_dite {C : Type u} [inst : CategoryTheory.Category C] {P : Prop} [inst : Decidable P] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)) : (f ≫ if h : P then g h else g' h) = if h : P then f ≫ g h else f ≫ g' h

ink

theorem CategoryTheory.dite_comp {C : Type u} [inst : CategoryTheory.Category C] {P : Prop} [inst : Decidable P] {X : C} {Y : C} {Z : C} (f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y)) (g : Y ⟶ Z) : (if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g

ink

class CategoryTheory.Epi {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X ⟶ Y) : Prop

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

  left_cancellation : ∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h

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

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

ink

class CategoryTheory.Mono {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X ⟶ Y) : Prop

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

  right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h

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

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

ink

instance CategoryTheory.instEpiIdToCategoryStruct {C : Type u} [inst : CategoryTheory.Category C] (X : C) : CategoryTheory.Epi (𝟙 X)

Equations

• @CategoryTheory.instEpiIdToCategoryStruct = @CategoryTheory.instEpiIdToCategoryStruct.proof_1

ink

instance CategoryTheory.instMonoIdToCategoryStruct {C : Type u} [inst : CategoryTheory.Category C] (X : C) : CategoryTheory.Mono (𝟙 X)

Equations

• @CategoryTheory.instMonoIdToCategoryStruct = @CategoryTheory.instMonoIdToCategoryStruct.proof_1

ink

theorem CategoryTheory.cancel_epi {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) [inst : CategoryTheory.Epi f] {g : Y ⟶ Z} {h : Y ⟶ Z} : f ≫ g = f ≫ h ↔ g = h

ink

theorem CategoryTheory.cancel_mono {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f] {g : Z ⟶ X} {h : Z ⟶ X} : g ≫ f = h ≫ f ↔ g = h

ink

theorem CategoryTheory.cancel_epi_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Epi f] {h : Y ⟶ Y} : f ≫ h = f ↔ h = 𝟙 Y

ink

theorem CategoryTheory.cancel_mono_id {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f] {g : X ⟶ X} : g ≫ f = f ↔ g = 𝟙 X

ink

theorem CategoryTheory.epi_comp {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) [inst : CategoryTheory.Epi f] (g : Y ⟶ Z) [inst : CategoryTheory.Epi g] : CategoryTheory.Epi (f ≫ g)

ink

theorem CategoryTheory.mono_comp {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f] (g : Y ⟶ Z) [inst : CategoryTheory.Mono g] : CategoryTheory.Mono (f ≫ g)

ink

theorem CategoryTheory.mono_of_mono {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : CategoryTheory.Mono (f ≫ g)] : CategoryTheory.Mono f

ink

theorem CategoryTheory.mono_of_mono_fac {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst : CategoryTheory.Mono h] (w : f ≫ g = h) : CategoryTheory.Mono f

ink

theorem CategoryTheory.epi_of_epi {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : CategoryTheory.Epi (f ≫ g)] : CategoryTheory.Epi g

ink

theorem CategoryTheory.epi_of_epi_fac {C : Type u} [inst : CategoryTheory.Category C] {X : C} {Y : C} {Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst : CategoryTheory.Epi h] (w : f ≫ g = h) : CategoryTheory.Epi g

ink

instance CategoryTheory.uliftCategory (C : Type u) [inst : CategoryTheory.Category C] : CategoryTheory.Category (ULift C)

Equations

• CategoryTheory.uliftCategory C = CategoryTheory.Category.mk