Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2017 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Stephen Morgan, Scott Morrison, Johannes Hölzl, Reid Barton
Ported by: Scott Morrison

! This file was ported from Lean 3 source module category_theory.category.basic
! leanprover-community/mathlib commit 2efd2423f8d25fa57cf7a179f5d8652ab4d0df44
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.CategoryTheory.Category.Init
import Mathlib.Combinatorics.Quiver.Basic
import Mathlib.Tactic.RestateAxiom

/-!
# Categories

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

## Notations

Introduces notations
* `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 `f ⊚ g` for composition in the standard convention, using
```lean
local notation f ` ⊚ `: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`.
-/


library_note "CategoryTheory universes"
/--
The typeclass `Category C` describes morphisms associated to objects of type `C : Type u`.

The universe levels of the objects and morphisms are independent, and will often need to be
specified explicitly, as `Category.{v} C`.

Typically any concrete example will either be a `SmallCategory`, where `v = u`,
which can be introduced as
```
universes u
variables {C : Type u} [SmallCategory C]
```
or a `LargeCategory`, where `u = v+1`, which can be introduced as
```
universes u
variables {C : Type (u+1)} [LargeCategory C]
```

In order for the library to handle these cases uniformly,
we generally work with the unconstrained `Category.{v u}`,
for which objects live in `Type u` and morphisms live in `Type v`.

Because the universe parameter `u` for the objects can be inferred from `C`
when we write `Category C`, while the universe parameter `v` for the morphisms
can not be automatically inferred, through the category theory library
we introduce universe parameters with morphism levels listed first,
as in
```
universes v u
```
or
```
universes v₁ v₂ u₁ u₂
```
when multiple independent universes are needed.

This has the effect that we can simply write `Category.{v} C`
(that is, only specifying a single parameter) while `u` will be inferred.

Often, however, it's not even necessary to include the `.{v}`.
(Although it was in earlier versions of Lean.)
If it is omitted a "free" universe will be used.
-/

namespace Std.Tactic.Ext
open Lean Elab Tactic

/-- A wrapper for `ext` that will fail if it does not make progress. -/
-- After https://github.com/leanprover/std4/pull/33
-- we can just `` evalTactic (← `(tactic| ext))``
-- (But it would be good to have a name for that, too, so we can pass it to aesop.)
def 
extCore': TacticM Unit
extCore'
:
TacticM: Type → Type
TacticM
Unit: Type
Unit
:= do let
gs: ?m.274
gs
←
Std.Tactic.Ext.extCore: MVarId → List (TSyntax `rcasesPat) → optParam ℕ 1000000 → optParam Bool true → TermElabM (Array (MVarId × List (TSyntax `rcasesPat)))
Std.Tactic.Ext.extCore
(← getMainGoal): ?m.73
(←
getMainGoal: TacticM MVarId
getMainGoal
(← getMainGoal): ?m.73
)
[]: List ?m.136
[]
1000000: ?m.147
1000000
true: Bool
true
replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal
<|
gs: ?m.274
gs
.
map: {α : Type ?u.286} → {β : Type ?u.285} → (α → β) → Array α → Array β
map
(·.1): MVarId × List (TSyntax `rcasesPat) → MVarId
(·.1)
|>.
toList: {α : Type ?u.300} → Array α → List α
toList
end Std.Tactic.Ext universe v u namespace CategoryTheory /-- A preliminary structure on the way to defining a category, containing the data, but none of the axioms. -/ class
CategoryStruct: {obj : Type u} → [toQuiver : Quiver obj] → ((X : obj) → X ⟶ X) → ({X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)) → CategoryStruct obj
CategoryStruct
(
obj: Type u
obj
:
Type u: Type (u+1)
Type u
) extends
Quiver: Type ?u.894 → Type (max?u.894(v+1))
Quiver
.{v + 1}
obj: Type u
obj
:
Type max u (v + 1): Type ((maxu(v+1))+1)
Type max u (v + 1)
where /-- The identity morphism on an object. -/
id: {obj : Type u} → [self : CategoryStruct obj] → (X : obj) → X ⟶ X
id
: ∀
X: obj
X
:
obj: Type u
obj
,
Hom: obj → obj → Type v
Hom
X: obj
X
X: obj
X
/-- Composition of morphisms in a category, written `f ≫ g`. -/
comp: {obj : Type u} → [self : CategoryStruct obj] → {X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
comp
: ∀ {
X: obj
X
Y: obj
Y
Z: obj
Z
:
obj: Type u
obj
}, (
X: obj
X
⟶
Y: obj
Y
) → (
Y: obj
Y
⟶
Z: obj
Z
) → (
X: obj
X
⟶
Z: obj
Z
) #align category_theory.category_struct
CategoryTheory.CategoryStruct: Type u → Type (maxu(v+1))
CategoryTheory.CategoryStruct
initialize_simps_projections
CategoryStruct: Type u → Type (maxu(v+1))
CategoryStruct
(-
toQuiver_Hom: (obj : Type u) → CategoryStruct obj → obj → obj → Type v
toQuiver_Hom
) /-- Notation for the identity morphism in a category. -/ notation "𝟙" =>
CategoryStruct.id: {obj : Type u} → [self : CategoryStruct obj] → (X : obj) → X ⟶ X
CategoryStruct.id
-- type as \b1 /-- Notation for composition of morphisms in a category. -/ infixr:80 " ≫ " =>
CategoryStruct.comp: {obj : Type u} → [self : CategoryStruct obj] → {X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
CategoryStruct.comp
-- type as \gg /-- 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. -/ macro (name :=
aesop_cat: Lean.ParserDescr
aesop_cat
) "aesop_cat"
c: ?m.15200
c
:
Aesop.tactic_clause: Lean.Parser.Category
Aesop.tactic_clause
*: tactic => `(tactic| aesop $
c: ?m.15200
c
* (options := { introsTransparency? := some .default, terminal := true }) (rule_sets [$(
Lean.mkIdent: Lean.Name → Lean.Ident
Lean.mkIdent
`CategoryTheory: Lean.Name
`CategoryTheory
):ident])) /-- 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`. -/ macro (name :=
aesop_cat_nonterminal: Lean.ParserDescr
aesop_cat_nonterminal
) "aesop_cat_nonterminal"
c: ?m.19116
c
:
Aesop.tactic_clause: Lean.Parser.Category
Aesop.tactic_clause
*: tactic => `(tactic| aesop $
c: ?m.19116
c
* (options := { introsTransparency? := some .default, warnOnNonterminal := false }) (rule_sets [$(
Lean.mkIdent: Lean.Name → Lean.Ident
Lean.mkIdent
`CategoryTheory: Lean.Name
`CategoryTheory
):ident])) -- We turn on `ext` inside `aesop_cat`. attribute [aesop safe tactic (rule_sets [CategoryTheory])]
Std.Tactic.Ext.extCore': Lean.Elab.Tactic.TacticM Unit
Std.Tactic.Ext.extCore'
-- Porting note: -- Workaround for issue discussed at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Failure.20of.20TC.20search.20in.20.60simp.60.20with.20.60etaExperiment.60.2E -- when etaExperiment is on. attribute [aesop safe (rule_sets [CategoryTheory])]
Subsingleton.elim: ∀ {α : Sort u} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim
/-- 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 . -/ class
Category: {obj : Type u} → [toCategoryStruct : CategoryStruct obj] → autoParam (∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f) _auto✝ → autoParam (∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f) _auto✝¹ → autoParam (∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h) _auto✝² → Category obj
Category
(
obj: Type u
obj
:
Type u: Type (u+1)
Type u
) extends
CategoryStruct: Type ?u.23087 → Type (max?u.23087(v+1))
CategoryStruct
.{v}
obj: Type u
obj
:
Type max u (v + 1): Type ((maxu(v+1))+1)
Type max u (v + 1)
where /-- Identity morphisms are left identities for composition. -/
id_comp: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
id_comp
: ∀ {
X: obj
X
Y: obj
Y
:
obj: Type u
obj
} (
f: X ⟶ Y
f
:
X: obj
X
⟶
Y: obj
Y
),
𝟙: (X : ?m.23136) → X ⟶ X
𝟙
X: obj
X
≫
f: X ⟶ Y
f
=
f: X ⟶ Y
f
:= by aesop_cat /-- Identity morphisms are right identities for composition. -/
comp_id: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
comp_id
: ∀ {
X: obj
X
Y: obj
Y
:
obj: Type u
obj
} (
f: X ⟶ Y
f
:
X: obj
X
⟶
Y: obj
Y
),
f: X ⟶ Y
f
≫
𝟙: (X : ?m.23213) → X ⟶ X
𝟙
Y: obj
Y
=
f: X ⟶ Y
f
:= by aesop_cat /-- Composition in a category is associative. -/
assoc: ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
assoc
: ∀ {
W: obj
W
X: obj
X
Y: obj
Y
Z: obj
Z
:
obj: Type u
obj
} (
f: W ⟶ X
f
:
W: obj
W
⟶
X: obj
X
) (
g: X ⟶ Y
g
:
X: obj
X
⟶
Y: obj
Y
) (
h: Y ⟶ Z
h
:
Y: obj
Y
⟶
Z: obj
Z
), (
f: W ⟶ X
f
≫
g: X ⟶ Y
g
) ≫
h: Y ⟶ Z
h
=
f: W ⟶ X
f
≫
g: X ⟶ Y
g
≫
h: Y ⟶ Z
h
:= by aesop_cat #align category_theory.category
CategoryTheory.Category: Type u → Type (maxu(v+1))
CategoryTheory.Category
#align category_theory.category.assoc
CategoryTheory.Category.assoc: ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
CategoryTheory.Category.assoc
#align category_theory.category.comp_id
CategoryTheory.Category.comp_id: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
CategoryTheory.Category.comp_id
#align category_theory.category.id_comp
CategoryTheory.Category.id_comp: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
CategoryTheory.Category.id_comp
-- Porting note: `restate_axiom` should not be necessary in lean4 -- Hopefully we can just remove the backticks from field names, -- then delete the invocation of `restate_axiom`. attribute [simp]
Category.id_comp: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
Category.id_comp
Category.comp_id: ∀ {obj : Type u} [self : Category obj] {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
Category.comp_id
Category.assoc: ∀ {obj : Type u} [self : Category obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
Category.assoc
attribute [trans]
CategoryStruct.comp: {obj : Type u} → [self : CategoryStruct obj] → {X Y Z : obj} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
CategoryStruct.comp
example: ∀ {C : Type u_1} [inst : Category C] {X Y : C} (f : X ⟶ Y), 𝟙 X ≫ f = f
example
{
C: Type ?u.23458
C
} [
Category: Type ?u.23458 → Type (max?u.23458(?u.23459+1))
Category
C: ?m.23455
C
] {
X: C
X
Y: C
Y
:
C: ?m.23455
C
} (
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) :
𝟙: (X : ?m.23509) → X ⟶ X
𝟙
X: C
X
≫
f: X ⟶ Y
f
=
f: X ⟶ Y
f
:=

Goals accomplished! 🐙
C: Type ?u.23458

inst✝: Category C

X, Y: C

f: X ⟶ Y



Goals accomplished! 🐙
example: ∀ {C : Type u_1} [inst : Category C] {X Y : C} (f : X ⟶ Y), f ≫ 𝟙 Y = f
example
{
C: ?m.23630
C
} [
Category: Type ?u.23633 → Type (max?u.23633(?u.23634+1))
Category
C: ?m.23630
C
] {
X: C
X
Y: C
Y
:
C: ?m.23630
C
} (
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) :
f: X ⟶ Y
f
≫
𝟙: (X : ?m.23697) → X ⟶ X
𝟙
Y: C
Y
=
f: X ⟶ Y
f
:=

Goals accomplished! 🐙
C: Type ?u.23633

inst✝: Category C

X, Y: C

f: X ⟶ Y



Goals accomplished! 🐙
/-- 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: Type (u+1) → Type (u+1)
LargeCategory
(
C: Type (u+1)
C
:
Type (u + 1): Type (u+2)
Type (u + 1)
) :
Type (u + 1): Type (u+2)
Type (u + 1)
:=
Category: Type ?u.23810 → Type (max?u.23810(u+1))
Category
.{u}
C: Type (u+1)
C
#align category_theory.large_category
CategoryTheory.LargeCategory: Type (u+1) → Type (u+1)
CategoryTheory.LargeCategory
/-- A `SmallCategory` has objects and morphisms in the same universe level. -/ abbrev
SmallCategory: Type u → Type (u+1)
SmallCategory
(
C: Type u
C
:
Type u: Type (u+1)
Type u
) :
Type (u + 1): Type (u+2)
Type (u + 1)
:=
Category: Type ?u.23818 → Type (max?u.23818(u+1))
Category
.{u}
C: Type u
C
#align category_theory.small_category
CategoryTheory.SmallCategory: Type u → Type (u+1)
CategoryTheory.SmallCategory
section variable {
C: Type u
C
:
Type u: Type (u+1)
Type u
} [
Category: Type ?u.47370 → Type (max?u.47370(v+1))
Category
.{v}
C: Type u
C
] {
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} initialize_simps_projections
Category: Type u → Type (maxu(v+1))
Category
(-
Hom: (obj : Type u) → Category obj → obj → obj → Type v
Hom
) /-- postcompose an equation between morphisms by another morphism -/ theorem
eq_whisker: ∀ {f g : X ⟶ Y}, f = g → ∀ (h : Y ⟶ Z), f ≫ h = g ≫ h
eq_whisker
{
f: X ⟶ Y
f
g: X ⟶ Y
g
:
X: C
X
⟶
Y: C
Y
} (
w: f = g
w
:
f: X ⟶ Y
f
=
g: X ⟶ Y
g
) (
h: Y ⟶ Z
h
:
Y: C
Y
⟶
Z: C
Z
) :
f: X ⟶ Y
f
≫
h: Y ⟶ Z
h
=
g: X ⟶ Y
g
≫
h: Y ⟶ Z
h
:=

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: f = g

h: Y ⟶ Z


f ≫ h = g ≫ h
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: f = g

h: Y ⟶ Z


f ≫ h = g ≫ h
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

w: f = g

h: Y ⟶ Z


g ≫ h = g ≫ h

Goals accomplished! 🐙
#align category_theory.eq_whisker
CategoryTheory.eq_whisker: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f g : X ⟶ Y}, f = g → ∀ (h : Y ⟶ Z), f ≫ h = g ≫ h
CategoryTheory.eq_whisker
/-- precompose an equation between morphisms by another morphism -/ theorem
whisker_eq: ∀ (f : X ⟶ Y) {g h : Y ⟶ Z}, g = h → f ≫ g = f ≫ h
whisker_eq
(
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) {
g: Y ⟶ Z
g
h: Y ⟶ Z
h
:
Y: C
Y
⟶
Z: C
Z
} (
w: g = h
w
:
g: Y ⟶ Z
g
=
h: Y ⟶ Z
h
) :
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
=
f: X ⟶ Y
f
≫
h: Y ⟶ Z
h
:=

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ Y

g, h: Y ⟶ Z

w: g = h


f ≫ g = f ≫ h
C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ Y

g, h: Y ⟶ Z

w: g = h


f ≫ g = f ≫ h
C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ Y

g, h: Y ⟶ Z

w: g = h


f ≫ h = f ≫ h

Goals accomplished! 🐙
#align category_theory.whisker_eq
CategoryTheory.whisker_eq: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) {g h : Y ⟶ Z}, g = h → f ≫ g = f ≫ h
CategoryTheory.whisker_eq
/-- 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`. -/ infixr:80 " =≫ " =>
eq_whisker: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f g : X ⟶ Y}, f = g → ∀ (h : Y ⟶ Z), f ≫ h = g ≫ h
eq_whisker
/-- 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`. -/ infixr:80 " ≫= " =>
whisker_eq: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) {g h : Y ⟶ Z}, g = h → f ≫ g = f ≫ h
whisker_eq
theorem
eq_of_comp_left_eq: ∀ {f g : X ⟶ Y}, (∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) → f = g
eq_of_comp_left_eq
{
f: X ⟶ Y
f
g: X ⟶ Y
g
:
X: C
X
⟶
Y: C
Y
} (
w: ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
w
: ∀ {
Z: C
Z
:
C: Type u
C
} (
h: Y ⟶ Z
h
:
Y: C
Y
⟶
Z: C
Z
),
f: X ⟶ Y
f
≫
h: Y ⟶ Z
h
=
g: X ⟶ Y
g
≫
h: Y ⟶ Z
h
) :
f: X ⟶ Y
f
=
g: X ⟶ Y
g
:=

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

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


f = g
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

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


h.e'_2
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

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


h.e'_3
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

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


f = g
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

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


h.e'_2
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

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


h.e'_3
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: X ⟶ Y

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


f = g

Goals accomplished! 🐙
#align category_theory.eq_of_comp_left_eq
CategoryTheory.eq_of_comp_left_eq: ∀ {C : Type u} [inst : Category C] {X Y : C} {f g : X ⟶ Y}, (∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) → f = g
CategoryTheory.eq_of_comp_left_eq
theorem
eq_of_comp_right_eq: ∀ {f g : Y ⟶ Z}, (∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g) → f = g
eq_of_comp_right_eq
{
f: Y ⟶ Z
f
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
} (
w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g
w
: ∀ {
X: C
X
:
C: Type u
C
} (
h: X ⟶ Y
h
:
X: C
X
⟶
Y: C
Y
),
h: X ⟶ Y
h
≫
f: Y ⟶ Z
f
=
h: X ⟶ Y
h
≫
g: Y ⟶ Z
g
) :
f: Y ⟶ Z
f
=
g: Y ⟶ Z
g
:=

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g


f = g
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g


h.e'_2
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g


h.e'_3
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g


f = g
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g


h.e'_2
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g


h.e'_3
C: Type u

inst✝: Category C

X, Y, Z: C

f, g: Y ⟶ Z

w: ∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g


f = g

Goals accomplished! 🐙
#align category_theory.eq_of_comp_right_eq
CategoryTheory.eq_of_comp_right_eq: ∀ {C : Type u} [inst : Category C] {Y Z : C} {f g : Y ⟶ Z}, (∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g) → f = g
CategoryTheory.eq_of_comp_right_eq
theorem
eq_of_comp_left_eq': ∀ (f g : X ⟶ Y), ((fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h) → f = g
eq_of_comp_left_eq'
(
f: X ⟶ Y
f
g: X ⟶ Y
g
:
X: C
X
⟶
Y: C
Y
) (
w: (fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h
w
: (fun {
Z: ?m.47446
Z
} (
h: Y ⟶ Z
h
:
Y: C
Y
⟶
Z: ?m.47446
Z
) =>
f: X ⟶ Y
f
≫
h: Y ⟶ Z
h
) = fun {
Z: ?m.47511
Z
} (
h: Y ⟶ Z
h
:
Y: C
Y
⟶
Z: ?m.47511
Z
) =>
g: X ⟶ Y
g
≫
h: Y ⟶ Z
h
) :
f: X ⟶ Y
f
=
g: X ⟶ Y
g
:=
eq_of_comp_left_eq: ∀ {C : Type ?u.47589} [inst : Category C] {X Y : C} {f g : X ⟶ Y}, (∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) → f = g
eq_of_comp_left_eq
@fun
Z: ?m.47610
Z
h: ?m.47613
h
=>

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X, Y, Z✝: C

f, g: X ⟶ Y

w: (fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h

Z: C

h: Y ⟶ Z


f ≫ h = g ≫ h

Goals accomplished! 🐙
#align category_theory.eq_of_comp_left_eq'
CategoryTheory.eq_of_comp_left_eq': ∀ {C : Type u} [inst : Category C] {X Y : C} (f g : X ⟶ Y), ((fun {Z} h => f ≫ h) = fun {Z} h => g ≫ h) → f = g
CategoryTheory.eq_of_comp_left_eq'
theorem
eq_of_comp_right_eq': ∀ (f g : Y ⟶ Z), ((fun {X} h => h ≫ f) = fun {X} h => h ≫ g) → f = g
eq_of_comp_right_eq'
(
f: Y ⟶ Z
f
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
) (
w: (fun {X} h => h ≫ f) = fun {X} h => h ≫ g
w
: (fun {
X: ?m.47795
X
} (
h: X ⟶ Y
h
:
X: ?m.47795
X
⟶
Y: C
Y
) =>
h: X ⟶ Y
h
≫
f: Y ⟶ Z
f
) = fun {
X: ?m.47860
X
} (
h: X ⟶ Y
h
:
X: ?m.47860
X
⟶
Y: C
Y
) =>
h: X ⟶ Y
h
≫
g: Y ⟶ Z
g
) :
f: Y ⟶ Z
f
=
g: Y ⟶ Z
g
:=
eq_of_comp_right_eq: ∀ {C : Type ?u.47938} [inst : Category C] {Y Z : C} {f g : Y ⟶ Z}, (∀ {X : C} (h : X ⟶ Y), h ≫ f = h ≫ g) → f = g
eq_of_comp_right_eq
@fun
X: ?m.47959
X
h: ?m.47962
h
=>

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X✝, Y, Z: C

f, g: Y ⟶ Z

w: (fun {X} h => h ≫ f) = fun {X} h => h ≫ g

X: C

h: X ⟶ Y


h ≫ f = h ≫ g

Goals accomplished! 🐙
#align category_theory.eq_of_comp_right_eq'
CategoryTheory.eq_of_comp_right_eq': ∀ {C : Type u} [inst : Category C] {Y Z : C} (f g : Y ⟶ Z), ((fun {X} h => h ≫ f) = fun {X} h => h ≫ g) → f = g
CategoryTheory.eq_of_comp_right_eq'
theorem
id_of_comp_left_id: ∀ {C : Type u} [inst : Category C] {X : C} (f : X ⟶ X), (∀ {Y : C} (g : X ⟶ Y), f ≫ g = g) → f = 𝟙 X
id_of_comp_left_id
(
f: X ⟶ X
f
:
X: C
X
⟶
X: C
X
) (
w: ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
w
: ∀ {
Y: C
Y
:
C: Type u
C
} (
g: X ⟶ Y
g
:
X: C
X
⟶
Y: C
Y
),
f: X ⟶ X
f
≫
g: X ⟶ Y
g
=
g: X ⟶ Y
g
) :
f: X ⟶ X
f
=
𝟙: (X : ?m.48183) → X ⟶ X
𝟙
X: C
X
:=

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g


C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g


h.e'_2
C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g



Goals accomplished! 🐙
#align category_theory.id_of_comp_left_id
CategoryTheory.id_of_comp_left_id: ∀ {C : Type u} [inst : Category C] {X : C} (f : X ⟶ X), (∀ {Y : C} (g : X ⟶ Y), f ≫ g = g) → f = 𝟙 X
CategoryTheory.id_of_comp_left_id
theorem
id_of_comp_right_id: ∀ {C : Type u} [inst : Category C] {X : C} (f : X ⟶ X), (∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) → f = 𝟙 X
id_of_comp_right_id
(
f: X ⟶ X
f
:
X: C
X
⟶
X: C
X
) (
w: ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g
w
: ∀ {
Y: C
Y
:
C: Type u
C
} (
g: Y ⟶ X
g
:
Y: C
Y
⟶
X: C
X
),
g: Y ⟶ X
g
≫
f: X ⟶ X
f
=
g: Y ⟶ X
g
) :
f: X ⟶ X
f
=
𝟙: (X : ?m.50257) → X ⟶ X
𝟙
X: C
X
:=

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g


C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g


h.e'_2
C: Type u

inst✝: Category C

X, Y, Z: C

f: X ⟶ X

w: ∀ {Y : C} (g : Y ⟶ X), g ≫ f = g



Goals accomplished! 🐙
#align category_theory.id_of_comp_right_id
CategoryTheory.id_of_comp_right_id: ∀ {C : Type u} [inst : Category C] {X : C} (f : X ⟶ X), (∀ {Y : C} (g : Y ⟶ X), g ≫ f = g) → f = 𝟙 X
CategoryTheory.id_of_comp_right_id
theorem
comp_ite: ∀ {P : Prop} [inst : 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'
comp_ite
{
P: Prop
P
:
Prop: Type
Prop
} [
Decidable: Prop → Type
Decidable
P: Prop
P
] {
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} (
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) (
g: Y ⟶ Z
g
g': Y ⟶ Z
g'
:
Y: C
Y
⟶
Z: C
Z
) : (
f: X ⟶ Y
f
≫ if
P: Prop
P
then
g: Y ⟶ Z
g
else
g': Y ⟶ Z
g'
) = if
P: Prop
P
then
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
else
f: X ⟶ Y
f
≫
g': Y ⟶ Z
g'
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝: C

P: Prop

inst✝: 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'

Goals accomplished! 🐙
#align category_theory.comp_ite
CategoryTheory.comp_ite: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : 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'
CategoryTheory.comp_ite
theorem
ite_comp: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : 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
ite_comp
{
P: Prop
P
:
Prop: Type
Prop
} [
Decidable: Prop → Type
Decidable
P: Prop
P
] {
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} (
f: X ⟶ Y
f
f': X ⟶ Y
f'
:
X: C
X
⟶
Y: C
Y
) (
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
) : (if
P: Prop
P
then
f: X ⟶ Y
f
else
f': X ⟶ Y
f'
) ≫
g: Y ⟶ Z
g
= if
P: Prop
P
then
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
else
f': X ⟶ Y
f'
≫
g: Y ⟶ Z
g
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝: C

P: Prop

inst✝: 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

Goals accomplished! 🐙
#align category_theory.ite_comp
CategoryTheory.ite_comp: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : 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
CategoryTheory.ite_comp
theorem
comp_dite: ∀ {P : Prop} [inst : 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
comp_dite
{
P: Prop
P
:
Prop: Type
Prop
} [
Decidable: Prop → Type
Decidable
P: Prop
P
] {
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} (
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) (
g: P → (Y ⟶ Z)
g
:
P: Prop
P
→ (
Y: C
Y
⟶
Z: C
Z
)) (
g': ¬P → (Y ⟶ Z)
g'
: ¬
P: Prop
P
→ (
Y: C
Y
⟶
Z: C
Z
)) : (
f: X ⟶ Y
f
≫ if
h: ?m.55087
h
:
P: Prop
P
then
g: P → (Y ⟶ Z)
g
h: ?m.55078
h
else
g': ¬P → (Y ⟶ Z)
g'
h: ?m.55087
h
) = if
h: ?m.55105
h
:
P: Prop
P
then
f: X ⟶ Y
f
≫
g: P → (Y ⟶ Z)
g
h: ?m.55105
h
else
f: X ⟶ Y
f
≫
g': ¬P → (Y ⟶ Z)
g'
h: ?m.55141
h
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝: C

P: Prop

inst✝: 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

Goals accomplished! 🐙
#align category_theory.comp_dite
CategoryTheory.comp_dite: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : 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
CategoryTheory.comp_dite
theorem
dite_comp: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : 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
dite_comp
{
P: Prop
P
:
Prop: Type
Prop
} [
Decidable: Prop → Type
Decidable
P: Prop
P
] {
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} (
f: P → (X ⟶ Y)
f
:
P: Prop
P
→ (
X: C
X
⟶
Y: C
Y
)) (
f': ¬P → (X ⟶ Y)
f'
: ¬
P: Prop
P
→ (
X: C
X
⟶
Y: C
Y
)) (
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
) : (if
h: ?m.56863
h
:
P: Prop
P
then
f: P → (X ⟶ Y)
f
h: ?m.56845
h
else
f': ¬P → (X ⟶ Y)
f'
h: ?m.56863
h
) ≫
g: Y ⟶ Z
g
= if
h: ?m.56921
h
:
P: Prop
P
then
f: P → (X ⟶ Y)
f
h: ?m.56885
h
≫
g: Y ⟶ Z
g
else
f': ¬P → (X ⟶ Y)
f'
h: ?m.56921
h
≫
g: Y ⟶ Z
g
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝: C

P: Prop

inst✝: 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

Goals accomplished! 🐙
#align category_theory.dite_comp
CategoryTheory.dite_comp: ∀ {C : Type u} [inst : Category C] {P : Prop} [inst_1 : 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
CategoryTheory.dite_comp
/-- A morphism `f` is an epimorphism if it can be cancelled when precomposed: `f ≫ g = f ≫ h` implies `g = h`. See . -/ class
Epi: ∀ {C : Type u} [inst : Category C] {X Y : C} {f : X ⟶ Y}, (∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h) → Epi f
Epi
(
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) :
Prop: Type
Prop
where /-- A morphism `f` is an epimorphism if it can be cancelled when precomposed. -/
left_cancellation: ∀ {C : Type u} [inst : Category C] {X Y : C} {f : X ⟶ Y} [self : Epi f] {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
left_cancellation
: ∀ {
Z: C
Z
:
C: Type u
C
} (
g: Y ⟶ Z
g
h: Y ⟶ Z
h
:
Y: C
Y
⟶
Z: C
Z
),
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
=
f: X ⟶ Y
f
≫
h: Y ⟶ Z
h
→
g: Y ⟶ Z
g
=
h: Y ⟶ Z
h
#align category_theory.epi
CategoryTheory.Epi: {C : Type u} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
CategoryTheory.Epi
/-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed: `g ≫ f = h ≫ f` implies `g = h`. See . -/ class
Mono: {C : Type u} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
(
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) :
Prop: Type
Prop
where /-- A morphism `f` is an monomorphism if it can be cancelled when postcomposed. -/
right_cancellation: ∀ {C : Type u} [inst : Category C] {X Y : C} {f : X ⟶ Y} [self : Mono f] {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
right_cancellation
: ∀ {
Z: C
Z
:
C: Type u
C
} (
g: Z ⟶ X
g
h: Z ⟶ X
h
:
Z: C
Z
⟶
X: C
X
),
g: Z ⟶ X
g
≫
f: X ⟶ Y
f
=
h: Z ⟶ X
h
≫
f: X ⟶ Y
f
→
g: Z ⟶ X
g
=
h: Z ⟶ X
h
#align category_theory.mono
CategoryTheory.Mono: {C : Type u} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
CategoryTheory.Mono
instance: ∀ {C : Type u} [inst : Category C] (X : C), Epi (𝟙 X)
instance
(
X: C
X
:
C: Type u
C
) :
Epi: {C : Type ?u.58872} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
(
𝟙: (X : ?m.58882) → X ⟶ X
𝟙
X: C
X
) := ⟨fun
g: ?m.58943
g
h: ?m.58946
h
w: ?m.58949
w
=>

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X✝, Y, Z, X, Z✝: C

g, h: X ⟶ Z✝

w: 𝟙 X ≫ g = 𝟙 X ≫ h


g = h

Goals accomplished! 🐙
⟩
instance: ∀ {C : Type u} [inst : Category C] (X : C), Mono (𝟙 X)
instance
(
X: C
X
:
C: Type u
C
) :
Mono: {C : Type ?u.59190} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
(
𝟙: (X : ?m.59200) → X ⟶ X
𝟙
X: C
X
) := ⟨fun
g: ?m.59261
g
h: ?m.59264
h
w: ?m.59267
w
=>

Goals accomplished! 🐙
C: Type u

inst✝: Category C

X✝, Y, Z, X, Z✝: C

g, h: Z✝ ⟶ X

w: g ≫ 𝟙 X = h ≫ 𝟙 X


g = h

Goals accomplished! 🐙
⟩ theorem
cancel_epi: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] {g h : Y ⟶ Z}, f ≫ g = f ≫ h ↔ g = h
cancel_epi
(
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) [
Epi: {C : Type ?u.59542} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
f: X ⟶ Y
f
] {
g: Y ⟶ Z
g
h: Y ⟶ Z
h
:
Y: C
Y
⟶
Z: C
Z
} :
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
=
f: X ⟶ Y
f
≫
h: Y ⟶ Z
h
↔
g: Y ⟶ Z
g
=
h: Y ⟶ Z
h
:= ⟨fun
p: ?m.59691
p
=>
Epi.left_cancellation: ∀ {C : Type ?u.59693} [inst : Category C] {X Y : C} {f : X ⟶ Y} [self : Epi f] {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
Epi.left_cancellation
g: Y ⟶ Z
g
h: Y ⟶ Z
h
p: ?m.59691
p
,
congr_arg: ∀ {α : Sort ?u.59737} {β : Sort ?u.59736} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg
_: ?m.59738 → ?m.59739
_
⟩ #align category_theory.cancel_epi
CategoryTheory.cancel_epi: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] {g h : Y ⟶ Z}, f ≫ g = f ≫ h ↔ g = h
CategoryTheory.cancel_epi
theorem
cancel_mono: ∀ (f : X ⟶ Y) [inst : Mono f] {g h : Z ⟶ X}, g ≫ f = h ≫ f ↔ g = h
cancel_mono
(
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) [
Mono: {C : Type ?u.59803} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
f: X ⟶ Y
f
] {
g: Z ⟶ X
g
h: Z ⟶ X
h
:
Z: C
Z
⟶
X: C
X
} :
g: Z ⟶ X
g
≫
f: X ⟶ Y
f
=
h: Z ⟶ X
h
≫
f: X ⟶ Y
f
↔
g: Z ⟶ X
g
=
h: Z ⟶ X
h
:= -- Porting note: in Lean 3 we could just write `congr_arg _` here. ⟨fun
p: ?m.59952
p
=>
Mono.right_cancellation: ∀ {C : Type ?u.59954} [inst : Category C] {X Y : C} {f : X ⟶ Y} [self : Mono f] {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
Mono.right_cancellation
g: Z ⟶ X
g
h: Z ⟶ X
h
p: ?m.59952
p
,
congr_arg: ∀ {α : Sort ?u.59998} {β : Sort ?u.59997} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg
(fun
k: ?m.60004
k
=>
k: ?m.60004
k
≫
f: X ⟶ Y
f
)⟩ #align category_theory.cancel_mono
CategoryTheory.cancel_mono: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] {g h : Z ⟶ X}, g ≫ f = h ≫ f ↔ g = h
CategoryTheory.cancel_mono
theorem
cancel_epi_id: ∀ (f : X ⟶ Y) [inst : Epi f] {h : Y ⟶ Y}, f ≫ h = f ↔ h = 𝟙 Y
cancel_epi_id
(
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) [
Epi: {C : Type ?u.60115} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
f: X ⟶ Y
f
] {
h: Y ⟶ Y
h
:
Y: C
Y
⟶
Y: C
Y
} :
f: X ⟶ Y
f
≫
h: Y ⟶ Y
h
=
f: X ⟶ Y
f
↔
h: Y ⟶ Y
h
=
𝟙: (X : ?m.60200) → X ⟶ X
𝟙
Y: C
Y
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Epi f

h: Y ⟶ Y


C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Epi f

h: Y ⟶ Y


h.e'_1.h.e'_3.h
C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Epi f

h: Y ⟶ Y



Goals accomplished! 🐙
#align category_theory.cancel_epi_id
CategoryTheory.cancel_epi_id: ∀ {C : Type u} [inst : Category C] {X Y : C} (f : X ⟶ Y) [inst_1 : Epi f] {h : Y ⟶ Y}, f ≫ h = f ↔ h = 𝟙 Y
CategoryTheory.cancel_epi_id
theorem
cancel_mono_id: ∀ (f : X ⟶ Y) [inst : Mono f] {g : X ⟶ X}, g ≫ f = f ↔ g = 𝟙 X
cancel_mono_id
(
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) [
Mono: {C : Type ?u.62959} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
f: X ⟶ Y
f
] {
g: X ⟶ X
g
:
X: C
X
⟶
X: C
X
} :
g: X ⟶ X
g
≫
f: X ⟶ Y
f
=
f: X ⟶ Y
f
↔
g: X ⟶ X
g
=
𝟙: (X : ?m.63044) → X ⟶ X
𝟙
X: C
X
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Mono f

g: X ⟶ X


C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Mono f

g: X ⟶ X


h.e'_1.h.e'_3.h
C: Type u

inst✝¹: Category C

X, Y, Z: C

f: X ⟶ Y

inst✝: Mono f

g: X ⟶ X



Goals accomplished! 🐙
#align category_theory.cancel_mono_id
CategoryTheory.cancel_mono_id: ∀ {C : Type u} [inst : Category C] {X Y : C} (f : X ⟶ Y) [inst_1 : Mono f] {g : X ⟶ X}, g ≫ f = f ↔ g = 𝟙 X
CategoryTheory.cancel_mono_id
theorem
epi_comp: ∀ {X Y Z : C} (f : X ⟶ Y) [inst : Epi f] (g : Y ⟶ Z) [inst : Epi g], Epi (f ≫ g)
epi_comp
{
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} (
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) [
Epi: {C : Type ?u.65808} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
f: X ⟶ Y
f
] (
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
) [
Epi: {C : Type ?u.65858} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
g: Y ⟶ Z
g
] :
Epi: {C : Type ?u.65876} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
(
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
) :=

Goals accomplished! 🐙
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g


Epi (f ≫ g)
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g


left_cancellation
∀ {Z_1 : C} (g_1 h : Z ⟶ Z_1), (f ≫ g) ≫ g_1 = (f ≫ g) ≫ h → g_1 = h
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g


Epi (f ≫ g)
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z✝

inst✝: Epi g

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b


left_cancellation
a = b
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g


Epi (f ≫ g)
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z✝

inst✝: Epi g

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b


left_cancellation
g ≫ a = g ≫ b
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g


Epi (f ≫ g)
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z✝

inst✝: Epi g

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b


left_cancellation
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Epi f

g: Y ⟶ Z

inst✝: Epi g


Epi (f ≫ g)

Goals accomplished! 🐙
#align category_theory.epi_comp
CategoryTheory.epi_comp: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Epi f] (g : Y ⟶ Z) [inst_2 : Epi g], Epi (f ≫ g)
CategoryTheory.epi_comp
theorem
mono_comp: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] (g : Y ⟶ Z) [inst_2 : Mono g], Mono (f ≫ g)
mono_comp
{
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} (
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) [
Mono: {C : Type ?u.66258} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
f: X ⟶ Y
f
] (
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
) [
Mono: {C : Type ?u.66308} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
g: Y ⟶ Z
g
] :
Mono: {C : Type ?u.66326} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
(
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
) :=

Goals accomplished! 🐙
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g


Mono (f ≫ g)
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g


right_cancellation
∀ {Z_1 : C} (g_1 h : Z_1 ⟶ X), g_1 ≫ f ≫ g = h ≫ f ≫ g → g_1 = h
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g


Mono (f ≫ g)
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z✝

inst✝: Mono g

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g


right_cancellation
a = b
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g


Mono (f ≫ g)
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z✝

inst✝: Mono g

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g


right_cancellation
a ≫ f = b ≫ f
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g


Mono (f ≫ g)
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z✝

inst✝: Mono g

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g


right_cancellation
(a ≫ f) ≫ g = (b ≫ f) ≫ g
C: Type u

inst✝²: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

inst✝¹: Mono f

g: Y ⟶ Z

inst✝: Mono g


Mono (f ≫ g)

Goals accomplished! 🐙
#align category_theory.mono_comp
CategoryTheory.mono_comp: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) [inst_1 : Mono f] (g : Y ⟶ Z) [inst_2 : Mono g], Mono (f ≫ g)
CategoryTheory.mono_comp
theorem
mono_of_mono: ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : Mono (f ≫ g)], Mono f
mono_of_mono
{
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} (
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) (
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
) [
Mono: {C : Type ?u.66730} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
(
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
)] :
Mono: {C : Type ?u.66787} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
f: X ⟶ Y
f
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)


C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)


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

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)


C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f = b ≫ f


right_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)


C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: (fun k => k ≫ g) (a ≫ f) = (fun k => k ≫ g) (b ≫ f)


right_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)


C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: (a ≫ f) ≫ g = (b ≫ f) ≫ g


right_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)


C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: (a ≫ f) ≫ g = (b ≫ f) ≫ g


right_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = (b ≫ f) ≫ g


right_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: (a ≫ f) ≫ g = (b ≫ f) ≫ g


right_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g


right_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g


right_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Mono (f ≫ g)

Z: C

a, b: Z ⟶ X

w: a ≫ f ≫ g = b ≫ f ≫ g


right_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)



Goals accomplished! 🐙
#align category_theory.mono_of_mono
CategoryTheory.mono_of_mono: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : Mono (f ≫ g)], Mono f
CategoryTheory.mono_of_mono
theorem
mono_of_mono_fac: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst_1 : Mono h], f ≫ g = h → Mono f
mono_of_mono_fac
{
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} {
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
} {
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
} {
h: X ⟶ Z
h
:
X: C
X
⟶
Z: C
Z
} [
Mono: {C : Type ?u.67186} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
h: X ⟶ Z
h
] (
w: f ≫ g = h
w
:
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
=
h: X ⟶ Z
h
) :
Mono: {C : Type ?u.67239} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Mono
f: X ⟶ Y
f
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

h: X ⟶ Z

inst✝: Mono h

w: f ≫ g = h


C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Mono (f ≫ g)


C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

h: X ⟶ Z

inst✝: Mono h

w: f ≫ g = h



Goals accomplished! 🐙
#align category_theory.mono_of_mono_fac
CategoryTheory.mono_of_mono_fac: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst_1 : Mono h], f ≫ g = h → Mono f
CategoryTheory.mono_of_mono_fac
theorem
epi_of_epi: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : Epi (f ≫ g)], Epi g
epi_of_epi
{
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} (
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
) (
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
) [
Epi: {C : Type ?u.67397} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
(
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
)] :
Epi: {C : Type ?u.67454} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
g: Y ⟶ Z
g
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)


Epi g
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)


left_cancellation
∀ {Z_1 : C} (g_1 h : Z ⟶ Z_1), g ≫ g_1 = g ≫ h → g_1 = h
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)


Epi g
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: g ≫ a = g ≫ b


left_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)


Epi g
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (fun k => f ≫ k) (g ≫ a) = (fun k => f ≫ k) (g ≫ b)


left_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)


Epi g
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: f ≫ g ≫ a = f ≫ g ≫ b


left_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)


Epi g
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: f ≫ g ≫ a = f ≫ g ≫ b


left_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = f ≫ g ≫ b


left_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: f ≫ g ≫ a = f ≫ g ≫ b


left_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b


left_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b


left_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝¹, X, Y, Z✝: C

f: X ⟶ Y

g: Y ⟶ Z✝

inst✝: Epi (f ≫ g)

Z: C

a, b: Z✝ ⟶ Z

w: (f ≫ g) ≫ a = (f ≫ g) ≫ b


left_cancellation
a = b
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)


Epi g

Goals accomplished! 🐙
#align category_theory.epi_of_epi
CategoryTheory.epi_of_epi: ∀ {C : Type u} [inst : Category C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : Epi (f ≫ g)], Epi g
CategoryTheory.epi_of_epi
theorem
epi_of_epi_fac: ∀ {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst : Epi h], f ≫ g = h → Epi g
epi_of_epi_fac
{
X: C
X
Y: C
Y
Z: C
Z
:
C: Type u
C
} {
f: X ⟶ Y
f
:
X: C
X
⟶
Y: C
Y
} {
g: Y ⟶ Z
g
:
Y: C
Y
⟶
Z: C
Z
} {
h: X ⟶ Z
h
:
X: C
X
⟶
Z: C
Z
} [
Epi: {C : Type ?u.67838} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
h: X ⟶ Z
h
] (
w: f ≫ g = h
w
:
f: X ⟶ Y
f
≫
g: Y ⟶ Z
g
=
h: X ⟶ Z
h
) :
Epi: {C : Type ?u.67891} → [inst : Category C] → {X Y : C} → (X ⟶ Y) → Prop
Epi
g: Y ⟶ Z
g
:=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

h: X ⟶ Z

inst✝: Epi h

w: f ≫ g = h


Epi g
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)


Epi g
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

inst✝: Epi (f ≫ g)


Epi g
C: Type u

inst✝¹: Category C

X✝, Y✝, Z✝, X, Y, Z: C

f: X ⟶ Y

g: Y ⟶ Z

h: X ⟶ Z

inst✝: Epi h

w: f ≫ g = h


Epi g

Goals accomplished! 🐙
#align category_theory.epi_of_epi_fac
CategoryTheory.epi_of_epi_fac: ∀ {C : Type u} [inst : Category C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [inst_1 : Epi h], f ≫ g = h → Epi g
CategoryTheory.epi_of_epi_fac
end section variable (
C: Type u
C
:
Type u: Type (u+1)
Type u
) variable [
Category: Type ?u.67976 → Type (max?u.67976(v+1))
Category
.{v}
C: Type u
C
] universe u' instance
uliftCategory: Category (ULift C)
uliftCategory
:
Category: Type ?u.67979 → Type (max?u.67979(v+1))
Category
.{v} (
ULift: Type ?u.67980 → Type (max?u.67980u')
ULift
.{u'}
C: Type u
C
) where Hom
X: ?m.67995
X
Y: ?m.67998
Y
:=
X: ?m.67995
X
.
down: {α : Type ?u.68012} → ULift α → α
down
⟶
Y: ?m.67998
Y
.
down: {α : Type ?u.68016} → ULift α → α
down
id
X: ?m.68040
X
:=
𝟙: (X : ?m.68044) → X ⟶ X
𝟙
X: ?m.68040
X
.
down: {α : Type ?u.68054} → ULift α → α
down
comp
f: ?m.68072
f
g: ?m.68075
g
:=
f: ?m.68072
f
≫
g: ?m.68075
g
#align category_theory.ulift_category
CategoryTheory.uliftCategory: (C : Type u) → [inst : Category C] → Category (ULift C)
CategoryTheory.uliftCategory
-- We verify that this previous instance can lift small categories to large categories.
example: (D : Type u) → [inst : SmallCategory D] → LargeCategory (ULift D)
example
(
D: Type u
D
:
Type u: Type (u+1)
Type u
) [
SmallCategory: Type ?u.69448 → Type (?u.69448+1)
SmallCategory
D: Type u
D
] :
LargeCategory: Type (?u.69451+1) → Type (?u.69451+1)
LargeCategory
(
ULift: Type ?u.69452 → Type (max?u.69452(u+1))
ULift
.{u + 1}
D: Type u
D
) :=

Goals accomplished! 🐙
C: Type u

inst✝¹: Category C

D: Type u

inst✝: SmallCategory D



Goals accomplished! 🐙
end end CategoryTheory -- Porting note: We hope that this will become less necessary, -- as in Lean4 `simp` will automatically enter "`dsimp` mode" when needed with dependent arguments. -- Optimistically, we will eventually remove this library note. library_note "dsimp, simp" /-- Many proofs in the category theory library use the `dsimp, simp` pattern, which typically isn't necessary elsewhere. One would usually hope that the same effect could be achieved simply with `simp`. The essential issue is that composition of morphisms involves dependent types. When you have a chain of morphisms being composed, say `f : X ⟶ Y` and `g : Y ⟶ Z`, then `simp` can operate successfully on the morphisms (e.g. if `f` is the identity it can strip that off). However if we have an equality of objects, say `Y = Y'`, then `simp` can't operate because it would break the typing of the composition operations. We rarely have interesting equalities of objects (because that would be "evil" --- anything interesting should be expressed as an isomorphism and tracked explicitly), except of course that we have plenty of definitional equalities of objects. `dsimp` can apply these safely, even inside a composition. After `dsimp` has cleared up the object level, `simp` can resume work on the morphism level --- but without the `dsimp` step, because `simp` looks at expressions syntactically, the relevant lemmas might not fire. There's no bound on how many times you potentially could have to switch back and forth, if the `simp` introduced new objects we again need to `dsimp`. In practice this does occur, but only rarely, because `simp` tends to shorten chains of compositions (i.e. not introduce new objects at all). -/