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 onX
(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
.
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.
The identity morphism on an object.
id : (X : obj) → X ⟶ XComposition of morphisms in a category, written
f ≫ g≫ g
.
A preliminary structure on the way to defining a category, containing the data, but none of the axioms.
Instances
Notation for the identity morphism in a category.
Equations
- CategoryTheory.«term𝟙» = Lean.ParserDescr.node `CategoryTheory.term𝟙 1024 (Lean.ParserDescr.symbol "𝟙")
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))
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.
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.
Identity morphisms are left identities for composition.
Identity morphisms are right identities for composition.
Composition in a category is associative.
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
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
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.
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.
A morphism
f
is an epimorphism if it can be cancelled when precomposed.
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.
Instances
A morphism
f
is an monomorphism if it can be cancelled when postcomposed.
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.
Instances
Equations
- CategoryTheory.uliftCategory C = CategoryTheory.Category.mk