-
Notifications
You must be signed in to change notification settings - Fork 298
/
epi_mono.lean
168 lines (134 loc) · 6.41 KB
/
epi_mono.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
/-
Copyright (c) 2019 Reid Barton. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Reid Barton, Scott Morrison
-/
import category_theory.adjunction.basic
import category_theory.opposites
import category_theory.groupoid
/-!
# Facts about epimorphisms and monomorphisms.
The definitions of `epi` and `mono` are in `category_theory.category`,
since they are used by some lemmas for `iso`, which is used everywhere.
-/
universes v₁ v₂ u₁ u₂
namespace category_theory
variables {C : Type u₁} [category.{v₁} C]
instance unop_mono_of_epi {A B : Cᵒᵖ} (f : A ⟶ B) [epi f] : mono f.unop :=
⟨λ Z g h eq, quiver.hom.op_inj ((cancel_epi f).1 (quiver.hom.unop_inj eq))⟩
instance unop_epi_of_mono {A B : Cᵒᵖ} (f : A ⟶ B) [mono f] : epi f.unop :=
⟨λ Z g h eq, quiver.hom.op_inj ((cancel_mono f).1 (quiver.hom.unop_inj eq))⟩
instance op_mono_of_epi {A B : C} (f : A ⟶ B) [epi f] : mono f.op :=
⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_epi f).1 (quiver.hom.op_inj eq))⟩
instance op_epi_of_mono {A B : C} (f : A ⟶ B) [mono f] : epi f.op :=
⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_mono f).1 (quiver.hom.op_inj eq))⟩
/--
A split monomorphism is a morphism `f : X ⟶ Y` admitting a retraction `retraction f : Y ⟶ X`
such that `f ≫ retraction f = 𝟙 X`.
Every split monomorphism is a monomorphism.
-/
class split_mono {X Y : C} (f : X ⟶ Y) :=
(retraction : Y ⟶ X)
(id' : f ≫ retraction = 𝟙 X . obviously)
/--
A split epimorphism is a morphism `f : X ⟶ Y` admitting a section `section_ f : Y ⟶ X`
such that `section_ f ≫ f = 𝟙 Y`.
(Note that `section` is a reserved keyword, so we append an underscore.)
Every split epimorphism is an epimorphism.
-/
class split_epi {X Y : C} (f : X ⟶ Y) :=
(section_ : Y ⟶ X)
(id' : section_ ≫ f = 𝟙 Y . obviously)
/-- The chosen retraction of a split monomorphism. -/
def retraction {X Y : C} (f : X ⟶ Y) [split_mono f] : Y ⟶ X := split_mono.retraction f
@[simp, reassoc]
lemma split_mono.id {X Y : C} (f : X ⟶ Y) [split_mono f] : f ≫ retraction f = 𝟙 X :=
split_mono.id'
/-- The retraction of a split monomorphism is itself a split epimorphism. -/
instance retraction_split_epi {X Y : C} (f : X ⟶ Y) [split_mono f] : split_epi (retraction f) :=
{ section_ := f }
/-- A split mono which is epi is an iso. -/
lemma is_iso_of_epi_of_split_mono {X Y : C} (f : X ⟶ Y) [split_mono f] [epi f] : is_iso f :=
⟨⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩⟩
/--
The chosen section of a split epimorphism.
(Note that `section` is a reserved keyword, so we append an underscore.)
-/
def section_ {X Y : C} (f : X ⟶ Y) [split_epi f] : Y ⟶ X := split_epi.section_ f
@[simp, reassoc]
lemma split_epi.id {X Y : C} (f : X ⟶ Y) [split_epi f] : section_ f ≫ f = 𝟙 Y :=
split_epi.id'
/-- The section of a split epimorphism is itself a split monomorphism. -/
instance section_split_mono {X Y : C} (f : X ⟶ Y) [split_epi f] : split_mono (section_ f) :=
{ retraction := f }
/-- A split epi which is mono is an iso. -/
lemma is_iso_of_mono_of_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [split_epi f] : is_iso f :=
⟨⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩⟩
/-- Every iso is a split mono. -/
@[priority 100]
noncomputable
instance split_mono.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_mono f :=
{ retraction := inv f }
/-- Every iso is a split epi. -/
@[priority 100]
noncomputable
instance split_epi.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_epi f :=
{ section_ := inv f }
/-- Every split mono is a mono. -/
@[priority 100]
instance split_mono.mono {X Y : C} (f : X ⟶ Y) [split_mono f] : mono f :=
{ right_cancellation := λ Z g h w, begin replace w := w =≫ retraction f, simpa using w, end }
/-- Every split epi is an epi. -/
@[priority 100]
instance split_epi.epi {X Y : C} (f : X ⟶ Y) [split_epi f] : epi f :=
{ left_cancellation := λ Z g h w, begin replace w := section_ f ≫= w, simpa using w, end }
/-- Every split mono whose retraction is mono is an iso. -/
lemma is_iso.of_mono_retraction {X Y : C} {f : X ⟶ Y} [split_mono f] [mono $ retraction f]
: is_iso f :=
⟨⟨retraction f, ⟨by simp, (cancel_mono_id $ retraction f).mp (by simp)⟩⟩⟩
/-- Every split epi whose section is epi is an iso. -/
lemma is_iso.of_epi_section {X Y : C} {f : X ⟶ Y} [split_epi f] [epi $ section_ f]
: is_iso f :=
⟨⟨section_ f, ⟨(cancel_epi_id $ section_ f).mp (by simp), by simp⟩⟩⟩
/-- A category where every morphism has a `trunc` retraction is computably a groupoid. -/
-- FIXME this has unnecessarily become noncomputable!
noncomputable
def groupoid.of_trunc_split_mono
(all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (split_mono f)) :
groupoid.{v₁} C :=
begin
apply groupoid.of_is_iso,
intros X Y f,
trunc_cases all_split_mono f,
trunc_cases all_split_mono (retraction f),
apply is_iso.of_mono_retraction,
end
section
variables (C)
/-- A split mono category is a category in which every monomorphism is split. -/
class split_mono_category :=
(split_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [mono f], split_mono f)
/-- A split epi category is a category in which every epimorphism is split. -/
class split_epi_category :=
(split_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [epi f], split_epi f)
end
/-- In a category in which every monomorphism is split, every monomorphism splits. This is not an
instance because it would create an instance loop. -/
def split_mono_of_mono [split_mono_category C] {X Y : C} (f : X ⟶ Y) [mono f] : split_mono f :=
split_mono_category.split_mono_of_mono _
/-- In a category in which every epimorphism is split, every epimorphism splits. This is not an
instance because it would create an instance loop. -/
def split_epi_of_epi [split_epi_category C] {X Y : C} (f : X ⟶ Y) [epi f] : split_epi f :=
split_epi_category.split_epi_of_epi _
section
variables {D : Type u₂} [category.{v₂} D]
/-- Split monomorphisms are also absolute monomorphisms. -/
instance {X Y : C} (f : X ⟶ Y) [split_mono f] (F : C ⥤ D) : split_mono (F.map f) :=
{ retraction := F.map (retraction f),
id' := by { rw [←functor.map_comp, split_mono.id, functor.map_id], } }
/-- Split epimorphisms are also absolute epimorphisms. -/
instance {X Y : C} (f : X ⟶ Y) [split_epi f] (F : C ⥤ D) : split_epi (F.map f) :=
{ section_ := F.map (section_ f),
id' := by { rw [←functor.map_comp, split_epi.id, functor.map_id], } }
end
end category_theory