Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 239d882

Browse files
joelrioujoelriou
committed
refactor(category_theory/epi_mono): is_split_epi and split_epi (#16036)
This PR makes a distinction between the class `is_split_epi f` which is a `Prop` and `split_epi f` which contains the datum of a section of `f`.
1 parent b5b30b0 commit 239d882

18 files changed

Lines changed: 247 additions & 174 deletions

‎src/category_theory/adjunction/reflective.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -89,8 +89,8 @@ lemma mem_ess_image_of_unit_is_iso [is_right_adjoint i] (A : C)
8989
⟨(left_adjoint i).obj A, ⟨(as_iso ((of_right_adjoint i).unit.app A)).symm⟩⟩
9090

9191
/-- If `η_A` is a split monomorphism, then `A` is in the reflective subcategory. -/
92-
lemma mem_ess_image_of_unit_split_mono [reflective i] {A : C}
93-
[split_mono ((of_right_adjoint i).unit.app A)] : A ∈ i.ess_image :=
92+
lemma mem_ess_image_of_unit_is_split_mono [reflective i] {A : C}
93+
[is_split_mono ((of_right_adjoint i).unit.app A)] : A ∈ i.ess_image :=
9494
begin
9595
let η : 𝟭 C ⟶ left_adjoint i ⋙ i := (of_right_adjoint i).unit,
9696
haveI : is_iso (η.app (i.obj ((left_adjoint i).obj A))) := (i.obj_mem_ess_image _).unit_is_iso,
@@ -99,7 +99,7 @@ begin
9999
rw (show retraction _ ≫ η.app A = _, from η.naturality (retraction (η.app A))),
100100
apply epi_comp (η.app (i.obj ((left_adjoint i).obj A))) },
101101
resetI,
102-
haveI := is_iso_of_epi_of_split_mono (η.app A),
102+
haveI := is_iso_of_epi_of_is_split_mono (η.app A),
103103
exact mem_ess_image_of_unit_is_iso A,
104104
end
105105

‎src/category_theory/closed/cartesian.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -306,8 +306,8 @@ lemma strict_initial {I : C} (t : is_initial I) (f : A ⟶ I) : is_iso f :=
306306
begin
307307
haveI : mono (limits.prod.lift (𝟙 A) f ≫ (zero_mul t).hom) := mono_comp _ _,
308308
rw [zero_mul_hom, prod.lift_snd] at _inst,
309-
haveI: split_epi f := ⟨t.to _, t.hom_ext _ _⟩,
310-
apply is_iso_of_mono_of_split_epi
309+
haveI: is_split_epi f := is_split_epi.mk' ⟨t.to _, t.hom_ext _ _⟩,
310+
apply is_iso_of_mono_of_is_split_epi
311311
end
312312

313313
instance to_initial_is_iso [has_initial C] (f : A ⟶ ⊥_ C) : is_iso f :=

‎src/category_theory/closed/ideal.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -143,8 +143,8 @@ begin
143143
ir.hom_equiv_apply_eq, assoc, assoc, prod_comparison_natural_assoc, L.map_id,
144144
← prod.map_id_comp_assoc, ir.left_triangle_components, prod.map_id_id, id_comp],
145145
apply is_iso.hom_inv_id_assoc },
146-
haveI : split_mono (η.app (A ⟹ i.obj B)) := ⟨_, this⟩,
147-
apply mem_ess_image_of_unit_split_mono,
146+
haveI : is_split_mono (η.app (A ⟹ i.obj B)) := is_split_mono.mk' ⟨_, this⟩,
147+
apply mem_ess_image_of_unit_is_split_mono,
148148
end
149149

150150
variables [exponential_ideal i]

‎src/category_theory/epi_mono.lean‎

Lines changed: 109 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -33,94 +33,146 @@ instance op_epi_of_mono {A B : C} (f : A ⟶ B) [mono f] : epi f.op :=
3333
⟨λ Z g h eq, quiver.hom.unop_inj ((cancel_mono f).1 (quiver.hom.op_inj eq))⟩
3434

3535
/--
36-
A split monomorphism is a morphism `f : X ⟶ Y` admitting a retraction `retraction f : Y ⟶ X`
36+
A split monomorphism is a morphism `f : X ⟶ Y` with a given retraction `retraction f : Y ⟶ X`
3737
such that `f ≫ retraction f = 𝟙 X`.
3838
3939
Every split monomorphism is a monomorphism.
4040
-/
41-
@[ext]
42-
class split_mono {X Y : C} (f : X ⟶ Y) :=
41+
@[ext, nolint has_nonempty_instance]
42+
structure split_mono {X Y : C} (f : X ⟶ Y) :=
4343
(retraction : Y ⟶ X)
4444
(id' : f ≫ retraction = 𝟙 X . obviously)
4545

46+
restate_axiom split_mono.id'
47+
attribute [simp, reassoc] split_mono.id
48+
49+
/-- `is_split_mono f` is the assertion that `f` admits a retraction -/
50+
class is_split_mono {X Y : C} (f : X ⟶ Y) : Prop :=
51+
(exists_split_mono : nonempty (split_mono f))
52+
53+
/-- A constructor for `is_split_mono f` taking a `split_mono f` as an argument -/
54+
lemma is_split_mono.mk' {X Y : C} {f : X ⟶ Y} (sm : split_mono f) :
55+
is_split_mono f := ⟨nonempty.intro sm⟩
56+
4657
/--
47-
A split epimorphism is a morphism `f : X ⟶ Y` admitting a section `section_ f : Y ⟶ X`
58+
A split epimorphism is a morphism `f : X ⟶ Y` with a given section `section_ f : Y ⟶ X`
4859
such that `section_ f ≫ f = 𝟙 Y`.
4960
(Note that `section` is a reserved keyword, so we append an underscore.)
5061
5162
Every split epimorphism is an epimorphism.
5263
-/
53-
@[ext]
54-
class split_epi {X Y : C} (f : X ⟶ Y) :=
64+
@[ext, nolint has_nonempty_instance]
65+
structure split_epi {X Y : C} (f : X ⟶ Y) :=
5566
(section_ : Y ⟶ X)
5667
(id' : section_ ≫ f = 𝟙 Y . obviously)
5768

69+
restate_axiom split_epi.id'
70+
attribute [simp, reassoc] split_epi.id
71+
72+
/-- `is_split_epi f` is the assertion that `f` admits a section -/
73+
class is_split_epi {X Y : C} (f : X ⟶ Y) : Prop :=
74+
(exists_split_epi : nonempty (split_epi f))
75+
76+
/-- A constructor for `is_split_epi f` taking a `split_epi f` as an argument -/
77+
lemma is_split_epi.mk' {X Y : C} {f : X ⟶ Y} (se : split_epi f) :
78+
is_split_epi f := ⟨nonempty.intro se⟩
79+
5880
/-- The chosen retraction of a split monomorphism. -/
59-
def retraction {X Y : C} (f : X ⟶ Y) [split_mono f] : Y ⟶ X := split_mono.retraction f
81+
noncomputable def retraction {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : Y ⟶ X :=
82+
hf.exists_split_mono.some.retraction
83+
6084
@[simp, reassoc]
61-
lemma split_mono.id {X Y : C} (f : X ⟶ Y) [split_mono f] : f ≫ retraction f = 𝟙 X :=
62-
split_mono.id'
85+
lemma is_split_mono.id {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : f ≫ retraction f = 𝟙 X :=
86+
hf.exists_split_mono.some.id
87+
88+
/-- The retraction of a split monomorphism has an obvious section. -/
89+
def split_mono.split_epi {X Y : C} {f : X ⟶ Y} (sm : split_mono f) : split_epi (sm.retraction) :=
90+
{ section_ := f, }
91+
6392
/-- The retraction of a split monomorphism is itself a split epimorphism. -/
64-
instance retraction_split_epi {X Y : C} (f : X ⟶ Y) [split_mono f] : split_epi (retraction f) :=
65-
{ section_ := f }
93+
instance retraction_is_split_epi {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] :
94+
is_split_epi (retraction f) :=
95+
is_split_epi.mk' (split_mono.split_epi _)
6696

6797
/-- A split mono which is epi is an iso. -/
68-
lemma is_iso_of_epi_of_split_mono {X Y : C} (f : X ⟶ Y) [split_mono f] [epi f] : is_iso f :=
98+
lemma is_iso_of_epi_of_is_split_mono {X Y : C} (f : X ⟶ Y) [is_split_mono f] [epi f] : is_iso f :=
6999
⟨⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩⟩
70100

71101
/--
72102
The chosen section of a split epimorphism.
73103
(Note that `section` is a reserved keyword, so we append an underscore.)
74104
-/
75-
def section_ {X Y : C} (f : X ⟶ Y) [split_epi f] : Y ⟶ X := split_epi.section_ f
105+
noncomputable def section_ {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : Y ⟶ X :=
106+
hf.exists_split_epi.some.section_
107+
76108
@[simp, reassoc]
77-
lemma split_epi.id {X Y : C} (f : X ⟶ Y) [split_epi f] : section_ f ≫ f = 𝟙 Y :=
78-
split_epi.id'
109+
lemma is_split_epi.id {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : section_ f ≫ f = 𝟙 Y :=
110+
hf.exists_split_epi.some.id
111+
112+
/-- The section of a split epimorphism has an obvious retraction. -/
113+
def split_epi.split_mono {X Y : C} {f : X ⟶ Y} (se : split_epi f) : split_mono (se.section_) :=
114+
{ retraction := f, }
115+
79116
/-- The section of a split epimorphism is itself a split monomorphism. -/
80-
instance section_split_mono {X Y : C} (f : X ⟶ Y) [split_epi f] : split_mono (section_ f) :=
81-
{ retraction := f }
117+
instance section_is_split_mono {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] :
118+
is_split_mono (section_ f) :=
119+
is_split_mono.mk' (split_epi.split_mono _)
82120

83121
/-- A split epi which is mono is an iso. -/
84-
lemma is_iso_of_mono_of_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [split_epi f] : is_iso f :=
122+
lemma is_iso_of_mono_of_is_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [is_split_epi f] : is_iso f :=
85123
⟨⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩⟩
86124

87125
/-- Every iso is a split mono. -/
88126
@[priority 100]
89-
noncomputable
90-
instance split_mono.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_mono f :=
91-
{ retraction := inv f }
127+
instance is_split_mono.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : is_split_mono f :=
128+
is_split_mono.mk' { retraction := inv f }
92129

93130
/-- Every iso is a split epi. -/
94131
@[priority 100]
95-
noncomputable
96-
instance split_epi.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_epi f :=
97-
{ section_ := inv f }
132+
instance is_split_epi.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : is_split_epi f :=
133+
is_split_epi.mk' { section_ := inv f }
134+
135+
lemma split_mono.mono {X Y : C} {f : X ⟶ Y} (sm : split_mono f) : mono f :=
136+
{ right_cancellation := λ Z g h w, begin replace w := w =≫ sm.retraction, simpa using w, end }
98137

99138
/-- Every split mono is a mono. -/
100139
@[priority 100]
101-
instance split_mono.mono {X Y : C} (f : X ⟶ Y) [split_mono f] : mono f :=
102-
{ right_cancellation := λ Z g h w, begin replace w := w =≫ retraction f, simpa using w, end }
140+
instance is_split_mono.mono {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] : mono f :=
141+
hf.exists_split_mono.some.mono
142+
143+
lemma split_epi.epi {X Y : C} {f : X ⟶ Y} (se : split_epi f) : epi f :=
144+
{ left_cancellation := λ Z g h w, begin replace w := se.section_ ≫= w, simpa using w, end }
103145

104146
/-- Every split epi is an epi. -/
105147
@[priority 100]
106-
instance split_epi.epi {X Y : C} (f : X ⟶ Y) [split_epi f] : epi f :=
107-
{ left_cancellation := λ Z g h w, begin replace w := section_ f ≫= w, simpa using w, end }
148+
instance is_split_epi.epi {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] : epi f :=
149+
hf.exists_split_epi.some.epi
150+
151+
/-- Every split mono whose retraction is mono is an iso. -/
152+
lemma is_iso.of_mono_retraction' {X Y : C} {f : X ⟶ Y} (hf : split_mono f)
153+
[mono $ hf.retraction] : is_iso f :=
154+
⟨⟨hf.retraction, ⟨by simp, (cancel_mono_id $ hf.retraction).mp (by simp)⟩⟩⟩
108155

109156
/-- Every split mono whose retraction is mono is an iso. -/
110-
lemma is_iso.of_mono_retraction {X Y : C} {f : X ⟶ Y} [split_mono f] [mono $ retraction f]
111-
: is_iso f :=
112-
⟨⟨retraction f, ⟨by simp, (cancel_mono_id $ retraction f).mp (by simp)⟩⟩⟩
157+
lemma is_iso.of_mono_retraction {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f]
158+
[hf' : mono $ retraction f] : is_iso f :=
159+
@is_iso.of_mono_retraction' _ _ _ _ _ hf.exists_split_mono.some hf'
113160

114161
/-- Every split epi whose section is epi is an iso. -/
115-
lemma is_iso.of_epi_section {X Y : C} {f : X ⟶ Y} [split_epi f] [epi $ section_ f]
116-
: is_iso f :=
117-
⟨⟨section_ f, ⟨(cancel_epi_id $ section_ f).mp (by simp), by simp⟩⟩⟩
162+
lemma is_iso.of_epi_section' {X Y : C} {f : X ⟶ Y} (hf : split_epi f)
163+
[epi $ hf.section_] : is_iso f :=
164+
⟨⟨hf.section_, ⟨(cancel_epi_id $ hf.section_).mp (by simp), by simp⟩⟩⟩
165+
166+
/-- Every split epi whose section is epi is an iso. -/
167+
lemma is_iso.of_epi_section {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f]
168+
[hf' : epi $ section_ f] : is_iso f :=
169+
@is_iso.of_epi_section' _ _ _ _ _ hf.exists_split_epi.some hf'
118170

119171
/-- A category where every morphism has a `trunc` retraction is computably a groupoid. -/
120172
-- FIXME this has unnecessarily become noncomputable!
121173
noncomputable
122174
def groupoid.of_trunc_split_mono
123-
(all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (split_mono f)) :
175+
(all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (is_split_mono f)) :
124176
groupoid.{v₁} C :=
125177
begin
126178
apply groupoid.of_is_iso,
@@ -135,36 +187,48 @@ variables (C)
135187

136188
/-- A split mono category is a category in which every monomorphism is split. -/
137189
class split_mono_category :=
138-
(split_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [mono f], split_mono f)
190+
(is_split_mono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [mono f], is_split_mono f)
139191

140192
/-- A split epi category is a category in which every epimorphism is split. -/
141193
class split_epi_category :=
142-
(split_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [epi f], split_epi f)
194+
(is_split_epi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [epi f], is_split_epi f)
143195

144196
end
145197

146198
/-- In a category in which every monomorphism is split, every monomorphism splits. This is not an
147199
instance because it would create an instance loop. -/
148-
def split_mono_of_mono [split_mono_category C] {X Y : C} (f : X ⟶ Y) [mono f] : split_mono f :=
149-
split_mono_category.split_mono_of_mono _
200+
lemma is_split_mono_of_mono [split_mono_category C] {X Y : C} (f : X ⟶ Y) [mono f] :
201+
is_split_mono f :=
202+
split_mono_category.is_split_mono_of_mono _
150203

151204
/-- In a category in which every epimorphism is split, every epimorphism splits. This is not an
152205
instance because it would create an instance loop. -/
153-
def split_epi_of_epi [split_epi_category C] {X Y : C} (f : X ⟶ Y) [epi f] : split_epi f :=
154-
split_epi_category.split_epi_of_epi _
206+
lemma is_split_epi_of_epi [split_epi_category C] {X Y : C} (f : X ⟶ Y) [epi f] :
207+
is_split_epi f := split_epi_category.is_split_epi_of_epi _
155208

156209
section
157210
variables {D : Type u₂} [category.{v₂} D]
158211

159212
/-- Split monomorphisms are also absolute monomorphisms. -/
160-
instance {X Y : C} (f : X ⟶ Y) [split_mono f] (F : C ⥤ D) : split_mono (F.map f) :=
161-
{ retraction := F.map (retraction f),
213+
@[simps]
214+
def split_mono.map {X Y : C} {f : X ⟶ Y} (sm : split_mono f) (F : C ⥤ D ) :
215+
split_mono (F.map f) :=
216+
{ retraction := F.map (sm.retraction),
162217
id' := by { rw [←functor.map_comp, split_mono.id, functor.map_id], } }
163218

164219
/-- Split epimorphisms are also absolute epimorphisms. -/
165-
instance {X Y : C} (f : X ⟶ Y) [split_epi f] (F : C ⥤ D) : split_epi (F.map f) :=
166-
{ section_ := F.map (section_ f),
220+
@[simps]
221+
def split_epi.map {X Y : C} {f : X ⟶ Y} (se : split_epi f) (F : C ⥤ D ) :
222+
split_epi (F.map f) :=
223+
{ section_ := F.map (se.section_),
167224
id' := by { rw [←functor.map_comp, split_epi.id, functor.map_id], } }
225+
226+
instance {X Y : C} (f : X ⟶ Y) [hf : is_split_mono f] (F : C ⥤ D) : is_split_mono (F.map f) :=
227+
is_split_mono.mk' (hf.exists_split_mono.some.map F)
228+
229+
instance {X Y : C} (f : X ⟶ Y) [hf : is_split_epi f] (F : C ⥤ D) : is_split_epi (F.map f) :=
230+
is_split_epi.mk' (hf.exists_split_epi.some.map F)
231+
168232
end
169233

170234
end category_theory

‎src/category_theory/functor/epi_mono.lean‎

Lines changed: 2 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -171,19 +171,9 @@ section
171171

172172
variables (F : C ⥤ D) {X Y : C} (f : X ⟶ Y)
173173

174-
/-- Split epimorphisms are preserved by the application of any functor. -/
175-
@[simps]
176-
def map_split_epi (s : split_epi f) : split_epi (F.map f) :=
177-
⟨F.map s.section_, by { rw [← F.map_comp, ← F.map_id], congr' 1, apply split_epi.id, }⟩
178-
179-
/-- Split monomorphisms are preserved by the application of any functor. -/
180-
@[simps]
181-
def map_split_mono (s : split_mono f) : split_mono (F.map f) :=
182-
⟨F.map s.retraction, by { rw [← F.map_comp, ← F.map_id], congr' 1, apply split_mono.id, }⟩
183-
184174
/-- If `F` is a fully faithful functor, split epimorphisms are preserved and reflected by `F`. -/
185175
def split_epi_equiv [full F] [faithful F] : split_epi f ≃ split_epi (F.map f) :=
186-
{ to_fun := F.map_split_epi f,
176+
{ to_fun := λ f, f.map F,
187177
inv_fun := λ s, begin
188178
refine ⟨F.preimage s.section_, _⟩,
189179
apply F.map_injective,
@@ -195,7 +185,7 @@ def split_epi_equiv [full F] [faithful F] : split_epi f ≃ split_epi (F.map f)
195185

196186
/-- If `F` is a fully faithful functor, split monomorphisms are preserved and reflected by `F`. -/
197187
def split_mono_equiv [full F] [faithful F] : split_mono f ≃ split_mono (F.map f) :=
198-
{ to_fun := F.map_split_mono f,
188+
{ to_fun := λ f, f.map F,
199189
inv_fun := λ s, begin
200190
refine ⟨F.preimage s.retraction, _⟩,
201191
apply F.map_injective,

‎src/category_theory/generator.lean‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -278,9 +278,10 @@ begin
278278
haveI : mono t := (is_coseparating_iff_mono 𝒢).1 h𝒢 A,
279279
exact subobject.of_le_mk _ (pullback.fst : pullback s t ⟶ _) bot_le ≫ pullback.snd },
280280
{ generalize : default = g,
281-
suffices : split_epi (equalizer.ι f g),
281+
suffices : is_split_epi (equalizer.ι f g),
282282
{ exactI eq_of_epi_equalizer },
283-
exact ⟨subobject.of_le_mk _ (equalizer.ι f g ≫ subobject.arrow _) bot_le, by { ext, simp }⟩ }
283+
exact is_split_epi.mk' ⟨subobject.of_le_mk _ (equalizer.ι f g ≫ subobject.arrow _)
284+
bot_le, by { ext, simp }⟩ }
284285
end
285286

286287
/-- An ingredient of the proof of the Special Adjoint Functor Theorem: a cocomplete well-copowered

‎src/category_theory/limits/constructions/weakly_initial.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ begin
5656
{ rw [category.assoc, category.assoc],
5757
apply wide_equalizer.condition (id : endos → endos) (h ≫ e ≫ i) },
5858
rw [category.comp_id, cancel_mono_id i] at this,
59-
haveI : split_epi e := ⟨i ≫ h, this⟩,
59+
haveI : is_split_epi e := is_split_epi.mk' ⟨i ≫ h, this⟩,
6060
rw ←cancel_epi e,
6161
apply equalizer.condition },
6262
exactI has_initial_of_unique (wide_equalizer (id : endos → endos)),

0 commit comments

Comments
 (0)