Skip to content

Commit 6aa35a6

Browse files
mattrobballmattrobball
committed
feat: port CategoryTheory.Limits.Shapes.SplitCoequalizer (#2655)
1 parent c76cd45 commit 6aa35a6

File tree

2 files changed

+193
-0
lines changed

2 files changed

+193
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -299,6 +299,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
299299
import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
300300
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
301301
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
302+
import Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
302303
import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
303304
import Mathlib.CategoryTheory.Limits.Shapes.Terminal
304305
import Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

‎Mathlib/CategoryTheory/Limits/Shapes/SplitCoequalizer.lean‎

Lines changed: 192 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,192 @@
1+
/-
2+
Copyright (c) 2020 Bhavik Mehta. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Bhavik Mehta
5+
6+
! This file was ported from Lean 3 source module category_theory.limits.shapes.split_coequalizer
7+
! leanprover-community/mathlib commit 024a4231815538ac739f52d08dd20a55da0d6b23
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
12+
13+
/-!
14+
# Split coequalizers
15+
16+
We define what it means for a triple of morphisms `f g : X ⟶ Y`, `π : Y ⟶ Z` to be a split
17+
coequalizer: there is a section `s` of `π` and a section `t` of `g`, which additionally satisfy
18+
`t ≫ f = π ≫ s`.
19+
20+
In addition, we show that every split coequalizer is a coequalizer
21+
(`CategoryTheory.IsSplitCoequalizer.isCoequalizer`) and absolute
22+
(`CategoryTheory.IsSplitCoequalizer.map`)
23+
24+
A pair `f g : X ⟶ Y` has a split coequalizer if there is a `Z` and `π : Y ⟶ Z` making `f,g,π` a
25+
split coequalizer.
26+
A pair `f g : X ⟶ Y` has a `G`-split coequalizer if `G f, G g` has a split coequalizer.
27+
28+
These definitions and constructions are useful in particular for the monadicity theorems.
29+
30+
## TODO
31+
32+
Dualise to split equalizers.
33+
-/
34+
35+
36+
namespace CategoryTheory
37+
38+
universe v v₂ u u₂
39+
40+
variable {C : Type u} [Category.{v} C]
41+
42+
variable {D : Type u₂} [Category.{v₂} D]
43+
44+
variable (G : C ⥤ D)
45+
46+
variable {X Y : C} (f g : X ⟶ Y)
47+
48+
/-- A split coequalizer diagram consists of morphisms
49+
50+
f π
51+
X ⇉ Y → Z
52+
g
53+
54+
satisfying `f ≫ π = g ≫ π` together with morphisms
55+
56+
t s
57+
X ← Y ← Z
58+
59+
satisfying `s ≫ π = 𝟙 Z`, `t ≫ g = 𝟙 Y` and `t ≫ f = π ≫ s`.
60+
61+
The name "coequalizer" is appropriate, since any split coequalizer is a coequalizer, see
62+
`Category_theory.IsSplitCoequalizer.isCoequalizer`.
63+
Split coequalizers are also absolute, since a functor preserves all the structure above.
64+
-/
65+
structure IsSplitCoequalizer {Z : C} (π : Y ⟶ Z) where
66+
/-- A map from the coequalizer to `Y` -/
67+
rightSection : Z ⟶ Y
68+
/-- A map in the opposite direction to `f` and `g` -/
69+
leftSection : Y ⟶ X
70+
/-- Composition of `π` with `f` and with `g` agree -/
71+
condition : f ≫ π = g ≫ π
72+
/-- `rightSection` splits `π` -/
73+
rightSection_π : rightSection ≫ π = 𝟙 Z
74+
/-- `leftSection` splits `g` -/
75+
leftSection_bottom : leftSection ≫ g = 𝟙 Y
76+
/-- `leftSection` composed with `f` is `pi` composed with `rightSection` -/
77+
leftSection_top : leftSection ≫ f = π ≫ rightSection
78+
#align category_theory.is_split_coequalizer CategoryTheory.IsSplitCoequalizer
79+
#align category_theory.is_split_coequalizer.right_section CategoryTheory.IsSplitCoequalizer.rightSection
80+
#align category_theory.is_split_coequalizer.left_section CategoryTheory.IsSplitCoequalizer.leftSection
81+
#align category_theory.is_split_coequalizer.right_section_π CategoryTheory.IsSplitCoequalizer.rightSection_π
82+
#align category_theory.is_split_coequalizer.left_section_bottom CategoryTheory.IsSplitCoequalizer.leftSection_bottom
83+
#align category_theory.is_split_coequalizer.left_section_top CategoryTheory.IsSplitCoequalizer.leftSection_top
84+
85+
instance {X : C} : Inhabited (IsSplitCoequalizer (𝟙 X) (𝟙 X) (𝟙 X)) where
86+
default := ⟨𝟙 X, 𝟙 X, rfl, Category.id_comp _, Category.id_comp _, rfl⟩
87+
88+
open IsSplitCoequalizer
89+
90+
attribute [reassoc] condition
91+
92+
attribute [reassoc (attr := simp)] rightSection_π leftSection_bottom leftSection_top
93+
94+
variable {f g}
95+
96+
/-- Split coequalizers are absolute: they are preserved by any functor. -/
97+
@[simps]
98+
def IsSplitCoequalizer.map {Z : C} {π : Y ⟶ Z} (q : IsSplitCoequalizer f g π) (F : C ⥤ D) :
99+
IsSplitCoequalizer (F.map f) (F.map g) (F.map π)
100+
where
101+
rightSection := F.map q.rightSection
102+
leftSection := F.map q.leftSection
103+
condition := by rw [← F.map_comp, q.condition, F.map_comp]
104+
rightSection_π := by rw [← F.map_comp, q.rightSection_π, F.map_id]
105+
leftSection_bottom := by rw [← F.map_comp, q.leftSection_bottom, F.map_id]
106+
leftSection_top := by rw [← F.map_comp, q.leftSection_top, F.map_comp]
107+
#align category_theory.is_split_coequalizer.map CategoryTheory.IsSplitCoequalizer.map
108+
109+
section
110+
111+
open Limits
112+
113+
/-- A split coequalizer clearly induces a cofork. -/
114+
@[simps! pt]
115+
def IsSplitCoequalizer.asCofork {Z : C} {h : Y ⟶ Z} (t : IsSplitCoequalizer f g h) :
116+
Cofork f g := Cofork.ofπ h t.condition
117+
#align category_theory.is_split_coequalizer.as_cofork CategoryTheory.IsSplitCoequalizer.asCofork
118+
119+
@[simp]
120+
theorem IsSplitCoequalizer.asCofork_π {Z : C} {h : Y ⟶ Z} (t : IsSplitCoequalizer f g h) :
121+
t.asCofork.π = h := rfl
122+
#align category_theory.is_split_coequalizer.as_cofork_π CategoryTheory.IsSplitCoequalizer.asCofork_π
123+
124+
/--
125+
The cofork induced by a split coequalizer is a coequalizer, justifying the name. In some cases it
126+
is more convenient to show a given cofork is a coequalizer by showing it is split.
127+
-/
128+
def IsSplitCoequalizer.isCoequalizer {Z : C} {h : Y ⟶ Z} (t : IsSplitCoequalizer f g h) :
129+
IsColimit t.asCofork :=
130+
Cofork.IsColimit.mk' _ fun s =>
131+
⟨t.rightSection ≫ s.π, by
132+
dsimp
133+
rw [← t.leftSection_top_assoc, s.condition, t.leftSection_bottom_assoc], fun hm => by
134+
simp [← hm]⟩
135+
#align category_theory.is_split_coequalizer.is_coequalizer CategoryTheory.IsSplitCoequalizer.isCoequalizer
136+
137+
end
138+
139+
variable (f g)
140+
141+
/--
142+
The pair `f,g` is a split pair if there is a `h : Y ⟶ Z` so that `f, g, h` forms a split coequalizer
143+
in `C`.
144+
-/
145+
class HasSplitCoequalizer : Prop where
146+
/-- There is some split coequalizer -/
147+
splittable : ∃ (Z : C)(h : Y ⟶ Z), Nonempty (IsSplitCoequalizer f g h)
148+
#align category_theory.has_split_coequalizer CategoryTheory.HasSplitCoequalizer
149+
150+
/--
151+
The pair `f,g` is a `G`-split pair if there is a `h : G Y ⟶ Z` so that `G f, G g, h` forms a split
152+
coequalizer in `D`.
153+
-/
154+
abbrev Functor.IsSplitPair : Prop :=
155+
HasSplitCoequalizer (G.map f) (G.map g)
156+
#align category_theory.functor.is_split_pair CategoryTheory.Functor.IsSplitPair
157+
158+
/-- Get the coequalizer object from the typeclass `IsSplitPair`. -/
159+
noncomputable def HasSplitCoequalizer.coequalizerOfSplit [HasSplitCoequalizer f g] : C :=
160+
(@splittable _ _ _ _ f g).choose
161+
#align category_theory.has_split_coequalizer.coequalizer_of_split CategoryTheory.HasSplitCoequalizer.coequalizerOfSplit
162+
163+
/-- Get the coequalizer morphism from the typeclass `IsSplitPair`. -/
164+
noncomputable def HasSplitCoequalizer.coequalizerπ [HasSplitCoequalizer f g] :
165+
Y ⟶ HasSplitCoequalizer.coequalizerOfSplit f g :=
166+
(@splittable _ _ _ _ f g).choose_spec.choose
167+
#align category_theory.has_split_coequalizer.coequalizer_π CategoryTheory.HasSplitCoequalizer.coequalizerπ
168+
169+
/-- The coequalizer morphism `coequalizeπ` gives a split coequalizer on `f,g`. -/
170+
noncomputable def HasSplitCoequalizer.isSplitCoequalizer [HasSplitCoequalizer f g] :
171+
IsSplitCoequalizer f g (HasSplitCoequalizer.coequalizerπ f g) :=
172+
Classical.choice (@splittable _ _ _ _ f g).choose_spec.choose_spec
173+
#align category_theory.has_split_coequalizer.is_split_coequalizer CategoryTheory.HasSplitCoequalizer.isSplitCoequalizer
174+
175+
/-- If `f, g` is split, then `G f, G g` is split. -/
176+
instance map_is_split_pair [HasSplitCoequalizer f g] : HasSplitCoequalizer (G.map f) (G.map g)
177+
where splittable :=
178+
⟨_, _, ⟨IsSplitCoequalizer.map (HasSplitCoequalizer.isSplitCoequalizer f g) _⟩⟩
179+
#align category_theory.map_is_split_pair CategoryTheory.map_is_split_pair
180+
181+
namespace Limits
182+
183+
/-- If a pair has a split coequalizer, it has a coequalizer. -/
184+
instance (priority := 1) hasCoequalizer_of_hasSplitCoequalizer [HasSplitCoequalizer f g] :
185+
HasCoequalizer f g :=
186+
HasColimit.mk ⟨_, (HasSplitCoequalizer.isSplitCoequalizer f g).isCoequalizer⟩
187+
#align category_theory.limits.has_coequalizer_of_has_split_coequalizer CategoryTheory.Limits.hasCoequalizer_of_hasSplitCoequalizer
188+
189+
end Limits
190+
191+
end CategoryTheory
192+

0 commit comments

Comments
 (0)
⚡