doc-next-gen

Mathlib.CategoryTheory.Category.Basic

Module docstring

{"# Categories

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

Notations

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

Users may like to add g ⊚ f for composition in the standard convention, using lean local notation:80 g \" ⊚ \" f:80 => CategoryTheory.CategoryStruct.comp f g -- type as \\oo

"}

CategoryTheory.CategoryStruct structure
(obj : Type u) : Type max u (v + 1) extends Quiver.{v + 1} obj
Full source 
/-- A preliminary structure on the way to defining a category,
containing the data, but none of the axioms. -/
@[pp_with_univ]
class CategoryStruct (obj : Type u) : Type max u (v + 1) extends Quiver.{v + 1} obj where
  /-- The identity morphism on an object. -/
  id : ∀ X : obj, Hom X X
  /-- Composition of morphisms in a category, written `f ≫ g`. -/
  comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
Category Structure (Preliminary)
Informal description
The structure `CategoryStruct` provides the basic data for defining a category, without including the category axioms. It consists of a type of objects and a quiver (a directed graph with hom-sets) structure on these objects, which includes the morphisms between objects and their composition. More precisely, for a type `obj` representing the objects of the category, `CategoryStruct` extends `Quiver` to include the data of morphisms between objects, but does not enforce the associativity of composition or the identity laws.
CategoryTheory.evalSorryIfSorry definition
: Tactic
Full source 
@[tactic sorryIfSorry, inherit_doc sorryIfSorry] def evalSorryIfSorry : Tactic := fun _ => do
  let goalType ← getMainTarget
  if goalType.hasSorry then
    closeMainGoal `sorry_if_sorry (← mkSorry goalType true)
  else
    throwError "The goal does not contain `sorry`"
"sorry" checker tactic
Informal description
A Lean tactic that checks whether the current proof goal contains `sorry`, and if so, closes the goal with `sorry_if_sorry`; otherwise throws an error indicating the goal doesn't contain `sorry`.
CategoryTheory.aesop_cat definition
: Lean.ParserDescr✝
Full source 
macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause* : tactic =>
`(tactic|
  first | sorry_if_sorry | rfl_cat |
  aesop $c* (config := { introsTransparency? := some .default, terminal := true })
            (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
Category theory specialized aesop tactic
Informal description
A specialized version of the `aesop` tactic for category theory that: 1. Automatically tries `sorry_if_sorry` and `rfl_cat` tactics first 2. Uses the `CategoryTheory` rule set 3. Allows `aesop` to look through semireducible definitions during `intros` 4. Fails when unable to solve the goal (making it suitable for auto-params)
CategoryTheory.aesop_cat? definition
: Lean.ParserDescr✝
Full source 
macro (name := aesop_cat?) "aesop_cat?" c:Aesop.tactic_clause* : tactic =>
`(tactic|
  first | sorry_if_sorry | try_this rfl_cat |
  aesop? $c* (config := { introsTransparency? := some .default, terminal := true })
             (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
Aesop category tactic with suggestion
Informal description
The macro `aesop_cat?` provides a `Try this` suggestion when using the `aesop_cat` tactic in category theory. It attempts to solve the current goal using the Aesop automation tool with a configuration tailored for category theory, including transparency settings and rule sets specific to category theory. If the goal cannot be solved, it falls back to suggesting `rfl_cat` or marking the goal as `sorry`.
CategoryTheory.aesop_cat_nonterminal definition
: Lean.ParserDescr✝
Full source 
macro (name := aesop_cat_nonterminal) "aesop_cat_nonterminal" c:Aesop.tactic_clause* : tactic =>
  `(tactic|
    aesop $c* (config := { introsTransparency? := some .default, warnOnNonterminal := false })
              (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
Nonterminal category theory automation tactic
Informal description
A nonterminal variant of the `aesop_cat` tactic which does not fail when it is unable to solve the goal. This is intended for exploratory purposes only, as nonterminal tactics can lead to unpredictable behavior.
CategoryTheory.Category structure
(obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj
Full source 
/-- 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`.) -/
@[pp_with_univ, stacks 0014]
class Category (obj : Type u) : Type max u (v + 1) extends CategoryStruct.{v} obj where
  /-- Identity morphisms are left identities for composition. -/
  id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙𝟙 X ≫ f = f := by aesop_cat
  /-- Identity morphisms are right identities for composition. -/
  comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f := by aesop_cat
  /-- Composition in a category is associative. -/
  assoc : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h := by
    aesop_cat
Category
Informal description
The structure `Category C` represents a category with objects of type `C` and morphisms between them. It extends the `CategoryStruct` which provides the basic structure of a category, including composition of morphisms and identity morphisms. The universe levels of the objects and morphisms can be specified independently.
CategoryTheory.LargeCategory abbrev
(C : Type (u + 1)) : Type (u + 1)
Full source 
/-- 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.
-/
abbrev LargeCategory (C : Type (u + 1)) : Type (u + 1) := Category.{u} C
Definition of Large Category
Informal description
A `LargeCategory` is a category where the objects are in a universe level one higher than the universe level of the morphisms. This is particularly useful for categories like the category of types or the category of groups, where the objects naturally live in a higher universe level than the morphisms.
CategoryTheory.SmallCategory abbrev
(C : Type u) : Type (u + 1)
Full source 
/-- A `SmallCategory` has objects and morphisms in the same universe level.
-/
abbrev SmallCategory (C : Type u) : Type (u + 1) := Category.{u} C
Small Category (Universe-Consistent)
Informal description
A small category is a category where both the objects and morphisms are in the same universe level. That is, if the objects are of type `C : Type u`, then the morphisms are also in `Type u`.
CategoryTheory.whisker_eq theorem
(f : X ⟶ Y) {g h : Y ⟶ Z} (w : g = h) : f ≫ g = f ≫ h
Full source 
/-- precompose an equation between morphisms by another morphism -/
theorem whisker_eq (f : X ⟶ Y) {g h : Y ⟶ Z} (w : g = h) : f ≫ g = f ≫ h := by rw [w]
Left whiskering preserves equality of morphisms
Informal description
Given a morphism $f \colon X \to Y$ and two morphisms $g, h \colon Y \to Z$ such that $g = h$, then the compositions $f \gg g$ and $f \gg h$ are equal, i.e., $f \gg g = f \gg h$.
CategoryTheory.term_=≫_ definition
: Lean.TrailingParserDescr✝
Full source 
/--
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`.
-/
scoped infixr:80 " =≫ " => eq_whisker
Right whiskering of an equation by a morphism
Informal description
Given morphisms \( f, g : X \longrightarrow Y \) and an equation \( w : f = g \), and a morphism \( h : Y \longrightarrow Z \), the notation \( w =\!\gg h \) denotes the equation \( f \gg h = g \gg h \), where \( \gg \) is the composition of morphisms in the category.
CategoryTheory.term_≫=_ definition
: Lean.TrailingParserDescr✝
Full source 
/--
Notation for whiskering an equation by a morphism (on the left).
If `g h : Y ⟶ Z` and `w : g = h` and `f : X ⟶ Y`, then `f ≫= w : f ≫ g = f ≫ h`.
-/
scoped infixr:80 " ≫= " => whisker_eq
Left whiskering of an equality by a morphism
Informal description
Given morphisms \( g, h : Y \to Z \) and an equality \( w : g = h \), and a morphism \( f : X \to Y \), the notation \( f \gg\!\!= w \) denotes the equality \( f \gg g = f \gg h \), where \( \gg \) denotes composition of morphisms in the category.
CategoryTheory.id_of_comp_left_id theorem
(f : X ⟶ X) (w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g) : f = 𝟙 X
Full source 
theorem id_of_comp_left_id (f : X ⟶ X) (w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g) : f = 𝟙 X := by
  convert w (𝟙 X)
  simp
Left Composition with Identity Condition Implies Identity Morphism
Informal description
For any endomorphism $f \colon X \to X$ in a category $\mathcal{C}$, if for every object $Y$ and every morphism $g \colon X \to Y$ the composition $f \circ g$ equals $g$, then $f$ must be the identity morphism on $X$, i.e., $f = \mathrm{id}_X$.
CategoryTheory.id_of_comp_right_id theorem
(f : X ⟶ X) (w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) : f = 𝟙 X
Full source 
theorem id_of_comp_right_id (f : X ⟶ X) (w : ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) : f = 𝟙 X := by
  convert w (𝟙 X)
  simp
Right Composition with Identity Condition Implies Identity Morphism
Informal description
For any endomorphism $f \colon X \to X$ in a category $\mathcal{C}$, if for every object $Y$ and every morphism $g \colon Y \to X$ the composition $g \circ f$ equals $g$, then $f$ must be the identity morphism on $X$, i.e., $f = \mathrm{id}_X$.
CategoryTheory.comp_ite theorem
{P : Prop} [Decidable P] {X Y Z : C} (f : X ⟶ Y) (g g' : Y ⟶ Z) : (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'
Full source 
theorem comp_ite {P : Prop} [Decidable P] {X Y Z : C} (f : X ⟶ Y) (g g' : Y ⟶ Z) :
    (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g' := by aesop
Composition with Conditional Morphism
Informal description
For any morphism $f \colon X \to Y$ and morphisms $g, g' \colon Y \to Z$ in a category $\mathcal{C}$, and for any decidable proposition $P$, the composition of $f$ with the conditional morphism (if $P$ then $g$ else $g'$) is equal to the conditional morphism (if $P$ then $f \circ g$ else $f \circ g'$). In symbols: $$ f \circ (\text{if } P \text{ then } g \text{ else } g') = \text{if } P \text{ then } f \circ g \text{ else } f \circ g' $$
CategoryTheory.ite_comp theorem
{P : Prop} [Decidable P] {X Y Z : C} (f f' : X ⟶ Y) (g : Y ⟶ Z) : (if P then f else f') ≫ g = if P then f ≫ g else f' ≫ g
Full source 
theorem ite_comp {P : Prop} [Decidable P] {X Y Z : C} (f f' : X ⟶ Y) (g : Y ⟶ Z) :
    (if P then f else f') ≫ g = if P then f ≫ g else f' ≫ g := by aesop
Conditional Morphism Composition Identity
Informal description
For any morphisms $f, f' \colon X \to Y$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, and for any decidable proposition $P$, the composition of the conditional morphism (if $P$ then $f$ else $f'$) with $g$ is equal to the conditional morphism (if $P$ then $f \circ g$ else $f' \circ g$). In symbols: $$ (\text{if } P \text{ then } f \text{ else } f') \circ g = \text{if } P \text{ then } f \circ g \text{ else } f' \circ g $$
CategoryTheory.comp_dite theorem
{P : Prop} [Decidable P] {X Y 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
Full source 
theorem comp_dite {P : Prop} [Decidable P]
    {X Y 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 := by aesop
Composition with Dependent Conditional Morphism
Informal description
Let $P$ be a decidable proposition, and let $X, Y, Z$ be objects in a category $\mathcal{C}$. For any morphism $f \colon X \to Y$ and families of morphisms $g \colon P \to (Y \to Z)$ and $g' \colon \neg P \to (Y \to Z)$, the following equality holds: $$ f \circ \left(\text{if } h : P \text{ then } g(h) \text{ else } g'(h)\right) = \text{if } h : P \text{ then } f \circ g(h) \text{ else } f \circ g'(h) $$
CategoryTheory.dite_comp theorem
{P : Prop} [Decidable P] {X Y 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
Full source 
theorem dite_comp {P : Prop} [Decidable P]
    {X Y 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 := by aesop
Conditional Morphism Composition Identity (Dependent Case)
Informal description
For any decidable proposition $P$, objects $X, Y, Z$ in a category $\mathcal{C}$, and morphisms $f \colon P \to (X \to Y)$, $f' \colon \neg P \to (X \to Y)$, and $g \colon Y \to Z$, the following equality holds: $$ \left(\text{if } h : P \text{ then } f(h) \text{ else } f'(h)\right) \circ g = \text{if } h : P \text{ then } f(h) \circ g \text{ else } f'(h) \circ g $$
CategoryTheory.Epi structure
(f : X ⟶ Y)
Full source 
/-- A morphism `f` is an epimorphism if it can be cancelled when precomposed:
`f ≫ g = f ≫ h` implies `g = h`. -/
@[stacks 003B]
class Epi (f : X ⟶ Y) : Prop where
  /-- 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
Epimorphism
Informal description
A morphism \( f : X \to Y \) in a category is called an epimorphism if for any two morphisms \( g, h : Y \to Z \), the equality \( f \circ g = f \circ h \) implies \( g = h \). In other words, \( f \) can be cancelled when precomposed.
CategoryTheory.Mono structure
(f : X ⟶ Y)
Full source 
/-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed:
`g ≫ f = h ≫ f` implies `g = h`. -/
@[stacks 003B]
class Mono (f : X ⟶ Y) : Prop where
  /-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed. -/
  right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Monomorphism
Informal description
A morphism \( f : X \to Y \) in a category is called a monomorphism if for any two morphisms \( g, h : Z \to X \), the equality \( g \circ f = h \circ f \) implies \( g = h \). In other words, \( f \) can be cancelled when postcomposed.
CategoryTheory.instEpiId instance
(X : C) : Epi (𝟙 X)
Full source 
instance (X : C) : Epi (𝟙 X) :=
  ⟨fun g h w => by aesop⟩
Identity Morphism is an Epimorphism
Informal description
For any object $X$ in a category $\mathcal{C}$, the identity morphism $\mathrm{id}_X$ is an epimorphism.
CategoryTheory.instMonoId instance
(X : C) : Mono (𝟙 X)
Full source 
instance (X : C) : Mono (𝟙 X) :=
  ⟨fun g h w => by aesop⟩
Identity Morphism is a Monomorphism
Informal description
For any object $X$ in a category $\mathcal{C}$, the identity morphism $\mathrm{id}_X$ is a monomorphism.
CategoryTheory.cancel_epi_assoc_iff theorem
(f : X ⟶ Y) [Epi f] {g h : Y ⟶ Z} {W : C} {k l : Z ⟶ W} : (f ≫ g) ≫ k = (f ≫ h) ≫ l ↔ g ≫ k = h ≫ l
Full source 
theorem cancel_epi_assoc_iff (f : X ⟶ Y) [Epi f] {g h : Y ⟶ Z} {W : C} {k l : Z ⟶ W} :
    (f ≫ g) ≫ k(f ≫ g) ≫ k = (f ≫ h) ≫ l ↔ g ≫ k = h ≫ l :=
  ⟨fun p => (cancel_epi f).1 <| by simpa using p, fun p => by simp only [Category.assoc, p]⟩
Associative Cancellation Property for Epimorphisms: $(f \circ g) \circ k = (f \circ h) \circ l \leftrightarrow g \circ k = h \circ l$
Informal description
Let $f \colon X \to Y$ be an epimorphism in a category $\mathcal{C}$, and let $g, h \colon Y \to Z$ and $k, l \colon Z \to W$ be morphisms in $\mathcal{C}$. Then the equality $(f \circ g) \circ k = (f \circ h) \circ l$ holds if and only if $g \circ k = h \circ l$.
CategoryTheory.cancel_mono theorem
(f : X ⟶ Y) [Mono f] {g h : Z ⟶ X} : g ≫ f = h ≫ f ↔ g = h
Full source 
theorem cancel_mono (f : X ⟶ Y) [Mono f] {g h : Z ⟶ X} : g ≫ fg ≫ f = h ≫ f ↔ g = h :=
  -- Porting note: in Lean 3 we could just write `congr_arg _` here.
  ⟨fun p => Mono.right_cancellation g h p, congr_arg (fun k => k ≫ f)⟩
Cancellation Property of Monomorphisms
Informal description
For any monomorphism $f \colon X \to Y$ in a category, and any pair of morphisms $g, h \colon Z \to X$, the equality $g \circ f = h \circ f$ holds if and only if $g = h$.
CategoryTheory.cancel_mono_assoc_iff theorem
(f : X ⟶ Y) [Mono f] {g h : Z ⟶ X} {W : C} {k l : W ⟶ Z} : k ≫ (g ≫ f) = l ≫ (h ≫ f) ↔ k ≫ g = l ≫ h
Full source 
theorem cancel_mono_assoc_iff (f : X ⟶ Y) [Mono f] {g h : Z ⟶ X} {W : C} {k l : W ⟶ Z} :
    k ≫ (g ≫ f)k ≫ (g ≫ f) = l ≫ (h ≫ f) ↔ k ≫ g = l ≫ h :=
  ⟨fun p => (cancel_mono f).1 <| by simpa using p, fun p => by simp only [← Category.assoc, p]⟩
Associative Cancellation Property for Monomorphisms: $k \circ (g \circ f) = l \circ (h \circ f) \leftrightarrow k \circ g = l \circ h$
Informal description
Let $f \colon X \to Y$ be a monomorphism in a category $\mathcal{C}$, and let $g, h \colon Z \to X$ and $k, l \colon W \to Z$ be morphisms in $\mathcal{C}$. Then the equality $k \circ (g \circ f) = l \circ (h \circ f)$ holds if and only if $k \circ g = l \circ h$.
CategoryTheory.cancel_epi_id theorem
(f : X ⟶ Y) [Epi f] {h : Y ⟶ Y} : f ≫ h = f ↔ h = 𝟙 Y
Full source 
theorem cancel_epi_id (f : X ⟶ Y) [Epi f] {h : Y ⟶ Y} : f ≫ hf ≫ h = f ↔ h = 𝟙 Y := by
  convert cancel_epi f
  simp
Identity Cancellation Property for Epimorphisms
Informal description
For any epimorphism $f \colon X \to Y$ in a category and any endomorphism $h \colon Y \to Y$, the equality $f \circ h = f$ holds if and only if $h$ is the identity morphism on $Y$, i.e., $h = \mathrm{id}_Y$.
CategoryTheory.cancel_mono_id theorem
(f : X ⟶ Y) [Mono f] {g : X ⟶ X} : g ≫ f = f ↔ g = 𝟙 X
Full source 
theorem cancel_mono_id (f : X ⟶ Y) [Mono f] {g : X ⟶ X} : g ≫ fg ≫ f = f ↔ g = 𝟙 X := by
  convert cancel_mono f
  simp
Identity Cancellation Property for Monomorphisms
Informal description
For any monomorphism $f \colon X \to Y$ in a category and any endomorphism $g \colon X \to X$, the equality $g \circ f = f$ holds if and only if $g$ is the identity morphism on $X$.
CategoryTheory.epi_comp instance
{X Y Z : C} (f : X ⟶ Y) [Epi f] (g : Y ⟶ Z) [Epi g] : Epi (f ≫ g)
Full source 
/-- The composition of epimorphisms is again an epimorphism. This version takes `Epi f` and `Epi g`
as typeclass arguments. For a version taking them as explicit arguments, see `epi_comp'`. -/
instance epi_comp {X Y Z : C} (f : X ⟶ Y) [Epi f] (g : Y ⟶ Z) [Epi g] : Epi (f ≫ g) :=
  ⟨fun _ _ w => (cancel_epi g).1 <| (cancel_epi_assoc_iff f).1 w⟩
Composition of Epimorphisms is an Epimorphism
Informal description
In any category, the composition $f \circ g$ of two epimorphisms $f \colon X \to Y$ and $g \colon Y \to Z$ is again an epimorphism.
CategoryTheory.epi_comp' theorem
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Epi f) (hg : Epi g) : Epi (f ≫ g)
Full source 
/-- The composition of epimorphisms is again an epimorphism. This version takes `Epi f` and `Epi g`
as explicit arguments. For a version taking them as typeclass arguments, see `epi_comp`. -/
theorem epi_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Epi f) (hg : Epi g) : Epi (f ≫ g) :=
  inferInstance
Composition of Explicit Epimorphisms is Epimorphic
Informal description
For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category $\mathcal{C}$, if $f$ and $g$ are epimorphisms, then their composition $f \circ g$ is also an epimorphism.
CategoryTheory.mono_comp instance
{X Y Z : C} (f : X ⟶ Y) [Mono f] (g : Y ⟶ Z) [Mono g] : Mono (f ≫ g)
Full source 
/-- The composition of monomorphisms is again a monomorphism. This version takes `Mono f` and
`Mono g` as typeclass arguments. For a version taking them as explicit arguments, see `mono_comp'`.
-/
instance mono_comp {X Y Z : C} (f : X ⟶ Y) [Mono f] (g : Y ⟶ Z) [Mono g] : Mono (f ≫ g) :=
  ⟨fun _ _ w => (cancel_mono f).1 <| (cancel_mono_assoc_iff g).1 w⟩
Composition of Monomorphisms is Monic
Informal description
For any monomorphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category, their composition $f \circ g$ is also a monomorphism.
CategoryTheory.mono_comp' theorem
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Mono f) (hg : Mono g) : Mono (f ≫ g)
Full source 
/-- The composition of monomorphisms is again a monomorphism. This version takes `Mono f` and
`Mono g` as explicit arguments. For a version taking them as typeclass arguments, see `mono_comp`.
-/
theorem mono_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Mono f) (hg : Mono g) :
    Mono (f ≫ g) :=
  inferInstance
Composition of Monomorphisms is Monic (explicit argument version)
Informal description
For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category, if $f$ and $g$ are monomorphisms, then their composition $f \circ g$ is also a monomorphism.
CategoryTheory.mono_of_mono theorem
{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono (f ≫ g)] : Mono f
Full source 
theorem mono_of_mono {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono (f ≫ g)] : Mono f :=
  ⟨fun _ _ w => (cancel_mono (f ≫ g)).1 <| by simp only [← Category.assoc, w]⟩
Monomorphism Property of Composition Factors: Left Factor is Mono
Informal description
For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category, if the composition $f \circ g$ is a monomorphism, then $f$ is a monomorphism.
CategoryTheory.mono_of_mono_fac theorem
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [Mono h] (w : f ≫ g = h) : Mono f
Full source 
theorem mono_of_mono_fac {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [Mono h]
    (w : f ≫ g = h) : Mono f := by
  subst h; exact mono_of_mono f g
Left Factor is Mono when Composition is Mono
Informal description
Given morphisms $f \colon X \to Y$, $g \colon Y \to Z$, and $h \colon X \to Z$ in a category such that $h$ is a monomorphism and $f \circ g = h$, then $f$ is a monomorphism.
CategoryTheory.epi_of_epi_fac theorem
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [Epi h] (w : f ≫ g = h) : Epi g
Full source 
theorem epi_of_epi_fac {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [Epi h]
    (w : f ≫ g = h) : Epi g := by
  subst h; exact epi_of_epi f g
Epimorphism Property via Factorization: $g$ is epi if $f \circ g$ is epi
Informal description
For any morphisms $f \colon X \to Y$ and $g \colon Y \to Z$ in a category, if there exists a morphism $h \colon X \to Z$ such that $h$ is an epimorphism and $f \circ g = h$, then $g$ is an epimorphism.
CategoryTheory.instMono instance
: Mono f
Full source 
instance : Mono f where
  right_cancellation _ _ _ := Subsingleton.elim _ _
$f$ is a Monomorphism
Informal description
The morphism $f : X \to Y$ is a monomorphism in the given category.
CategoryTheory.instEpi instance
: Epi f
Full source 
instance : Epi f where
  left_cancellation _ _ _ := Subsingleton.elim _ _
Epimorphism Property of $f$
Informal description
The morphism $f : X \to Y$ is an epimorphism in the given category.
CategoryTheory.uliftCategory instance
: Category.{v} (ULift.{u'} C)
Full source 
instance uliftCategory : Category.{v} (ULift.{u'} C) where
  Hom X Y := X.down ⟶ Y.down
  id X := 𝟙 X.down
  comp f g := f ≫ g

-- We verify that this previous instance can lift small categories to large categories.
Category Structure on Universe-Lifted Objects
Informal description
For any category $C$ and universe levels $u'$ and $v$, the lifted category $\mathrm{ULift}_{u'}(C)$ forms a category with morphisms and composition inherited from $C$.