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

Commit b5128b8

Browse files
kim-emkim-em
committed
feat(category_theory/limits): pullback squares (#14220)
Per [zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/pushout.20of.20biprod.2Efst.20and.20biprod.2Esnd.20is.20zero). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent 94644b7 commit b5128b8

File tree

2 files changed

+348
-0
lines changed

2 files changed

+348
-0
lines changed

‎src/category_theory/limits/shapes/comm_sq.lean‎

Lines changed: 310 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,310 @@
1+
/-
2+
Copyright (c) 2022 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison
5+
-/
6+
import category_theory.limits.shapes.pullbacks
7+
import category_theory.limits.shapes.zero_morphisms
8+
9+
/-!
10+
# Pullback and pushout squares
11+
12+
We provide another API for pullbacks and pushouts.
13+
14+
`is_pullback fst snd f g` is the proposition that
15+
```
16+
P --fst--> X
17+
| |
18+
snd f
19+
| |
20+
v v
21+
Y ---g---> Z
22+
23+
```
24+
is a pullback square.
25+
26+
(And similarly for `is_pushout`.)
27+
28+
We provide the glue to go back and forth to the usual `is_limit` API for pullbacks, and prove
29+
`is_pullback (pullback.fst : pullback f g ⟶ X) (pullback.snd : pullback f g ⟶ Y) f g`
30+
for the usual `pullback f g` provided by the `has_limit` API.
31+
32+
We don't attempt to restate everything we know about pullbacks in this language,
33+
but do restate the pasting lemmas.
34+
35+
## Future work
36+
Bicartesian squares, and
37+
show that the pullback and pushout squares for a biproduct are bicartesian.
38+
-/
39+
40+
open category_theory
41+
42+
namespace category_theory.limits
43+
44+
variables {C : Type*} [category C]
45+
46+
/-- The proposition that a square
47+
```
48+
W ---f---> X
49+
| |
50+
g h
51+
| |
52+
v v
53+
Y ---i---> Z
54+
55+
```
56+
is a commuting square.
57+
-/
58+
structure comm_sq {W X Y Z : C} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z) : Prop :=
59+
(w : f ≫ h = g ≫ i)
60+
61+
attribute [reassoc] comm_sq.w
62+
63+
namespace comm_sq
64+
65+
lemma flip {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
66+
(p : comm_sq f g h i) : comm_sq g f i h := ⟨p.w.symm⟩
67+
68+
lemma of_arrow {f g : arrow C} (h : f ⟶ g) : comm_sq f.hom h.left h.right g.hom := ⟨h.w.symm⟩
69+
70+
end comm_sq
71+
72+
/-- The proposition that a square
73+
```
74+
P --fst--> X
75+
| |
76+
snd f
77+
| |
78+
v v
79+
Y ---g---> Z
80+
81+
```
82+
is a pullback square.
83+
-/
84+
structure is_pullback
85+
{P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z)
86+
extends comm_sq fst snd f g : Prop :=
87+
(is_limit' : nonempty (is_limit (pullback_cone.mk _ _ w)))
88+
89+
/-- The proposition that a square
90+
```
91+
Z ---f---> X
92+
| |
93+
g inl
94+
| |
95+
v v
96+
Y --inr--> P
97+
98+
```
99+
is a pushout square.
100+
-/
101+
structure is_pushout
102+
{Z X Y P : C} (f : Z ⟶ X) (g : Z ⟶ Y) (inl : X ⟶ P) (inr : Y ⟶ P)
103+
extends comm_sq f g inl inr : Prop :=
104+
(is_colimit' : nonempty (is_colimit (pushout_cocone.mk _ _ w)))
105+
106+
/-!
107+
We begin by providing some glue between `is_pullback` and the `is_limit` and `has_limit` APIs.
108+
(And similarly for `is_pushout`.)
109+
-/
110+
111+
namespace is_pullback
112+
113+
variables {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z}
114+
115+
/--
116+
The `pullback_cone f g` implicit in the statement that we have a `is_pullback fst snd f g`.
117+
-/
118+
def cone (h : is_pullback fst snd f g) : pullback_cone f g := pullback_cone.mk _ _ h.w
119+
120+
/--
121+
The cone obtained from `is_pullback fst snd f g` is a limit cone.
122+
-/
123+
noncomputable def is_limit (h : is_pullback fst snd f g) : is_limit h.cone :=
124+
h.is_limit'.some
125+
126+
/-- If `c` is a limiting pullback cone, then we have a `is_pullback c.fst c.snd f g`. -/
127+
lemma of_is_limit {c : pullback_cone f g} (h : limits.is_limit c) :
128+
is_pullback c.fst c.snd f g :=
129+
{ w := c.condition,
130+
is_limit' := ⟨is_limit.of_iso_limit h
131+
(limits.pullback_cone.ext (iso.refl _) (by tidy) (by tidy))⟩, }
132+
133+
/-- The pullback provided by `has_pullback f g` fits into a `is_pullback`. -/
134+
lemma of_has_pullback (f : X ⟶ Z) (g : Y ⟶ Z) [has_pullback f g] :
135+
is_pullback (pullback.fst : pullback f g ⟶ X) (pullback.snd : pullback f g ⟶ Y) f g :=
136+
of_is_limit (limit.is_limit (cospan f g))
137+
138+
end is_pullback
139+
140+
namespace is_pushout
141+
142+
variables {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P}
143+
144+
/--
145+
The `pushout_cocone f g` implicit in the statement that we have a `is_pushout f g inl inr`.
146+
-/
147+
def cocone (h : is_pushout f g inl inr) : pushout_cocone f g := pushout_cocone.mk _ _ h.w
148+
149+
/--
150+
The cocone obtained from `is_pushout f g inl inr` is a colimit cocone.
151+
-/
152+
noncomputable def is_colimit (h : is_pushout f g inl inr) : is_colimit h.cocone :=
153+
h.is_colimit'.some
154+
155+
/-- If `c` is a colimiting pushout cocone, then we have a `is_pushout f g c.inl c.inr`. -/
156+
lemma of_is_colimit {c : pushout_cocone f g} (h : limits.is_colimit c) :
157+
is_pushout f g c.inl c.inr :=
158+
{ w := c.condition,
159+
is_colimit' := ⟨is_colimit.of_iso_colimit h
160+
(limits.pushout_cocone.ext (iso.refl _) (by tidy) (by tidy))⟩, }
161+
162+
/-- The pushout provided by `has_pushout f g` fits into a `is_pushout`. -/
163+
lemma of_has_pushout (f : Z ⟶ X) (g : Z ⟶ Y) [has_pushout f g] :
164+
is_pushout f g (pushout.inl : X ⟶ pushout f g) (pushout.inr : Y ⟶ pushout f g) :=
165+
of_is_colimit (colimit.is_colimit (span f g))
166+
167+
end is_pushout
168+
169+
namespace is_pullback
170+
171+
variables {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z}
172+
173+
lemma flip (h : is_pullback fst snd f g) : is_pullback snd fst g f :=
174+
of_is_limit (@pullback_cone.flip_is_limit _ _ _ _ _ _ _ _ _ _ h.w.symm h.is_limit)
175+
176+
section
177+
178+
variables [has_zero_object C] [has_zero_morphisms C]
179+
open_locale zero_object
180+
181+
/-- The square with `0 : 0 ⟶ 0` on the left and `𝟙 X` on the right is a pullback square. -/
182+
lemma zero_left (X : C) : is_pullback (0 : 0 ⟶ X) (0 : 0 ⟶ 0) (𝟙 X) (0 : 0 ⟶ X) :=
183+
{ w := by simp,
184+
is_limit' :=
185+
⟨{ lift := λ s, 0,
186+
fac' := λ s, by simpa using @pullback_cone.equalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _)
187+
(by simpa using (pullback_cone.condition s).symm), }⟩ }
188+
189+
/-- The square with `0 : 0 ⟶ 0` on the top and `𝟙 X` on the bottom is a pullback square. -/
190+
lemma zero_top (X : C) : is_pullback (0 : 0 ⟶ 0) (0 : 0 ⟶ X) (0 : 0 ⟶ X) (𝟙 X) :=
191+
(zero_left X).flip
192+
193+
end
194+
195+
/-- Paste two pullback squares "vertically" to obtain another pullback square. -/
196+
-- Objects here are arranged in a 3x2 grid, and indexed by their xy coordinates.
197+
-- Morphisms are named `hᵢⱼ` for a horizontal morphism starting at `(i,j)`,
198+
-- and `vᵢⱼ` for a vertical morphism starting at `(i,j)`.
199+
lemma paste_vert {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
200+
{h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂}
201+
{v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂}
202+
(s : is_pullback h₁₁ v₁₁ v₁₂ h₂₁) (t : is_pullback h₂₁ v₂₁ v₂₂ h₃₁) :
203+
is_pullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ :=
204+
(of_is_limit
205+
(big_square_is_pullback _ _ _ _ _ _ _ s.w t.w t.is_limit s.is_limit))
206+
207+
/-- Paste two pullback squares "horizontally" to obtain another pullback square. -/
208+
lemma paste_horiz {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
209+
{h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃}
210+
{v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃}
211+
(s : is_pullback h₁₁ v₁₁ v₁₂ h₂₁) (t : is_pullback h₁₂ v₁₂ v₁₃ h₂₂) :
212+
is_pullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) :=
213+
(paste_vert s.flip t.flip).flip
214+
215+
/-- Given a pullback square assembled from a commuting square on the top and
216+
a pullback square on the bottom, the top square is a pullback square. -/
217+
lemma of_bot {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
218+
{h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂}
219+
{v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂}
220+
(s : is_pullback h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁) (p : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁)
221+
(t : is_pullback h₂₁ v₂₁ v₂₂ h₃₁) :
222+
is_pullback h₁₁ v₁₁ v₁₂ h₂₁ :=
223+
of_is_limit (left_square_is_pullback _ _ _ _ _ _ _ p _ t.is_limit s.is_limit)
224+
225+
/-- Given a pullback square assembled from a commuting square on the left and
226+
a pullback square on the right, the left square is a pullback square. -/
227+
lemma of_right {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
228+
{h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃}
229+
{v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃}
230+
(s : is_pullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)) (p : h₁₁ ≫ v₁₂ = v₁₁ ≫ h₂₁)
231+
(t : is_pullback h₁₂ v₁₂ v₁₃ h₂₂) :
232+
is_pullback h₁₁ v₁₁ v₁₂ h₂₁ :=
233+
(of_bot s.flip p.symm t.flip).flip
234+
235+
end is_pullback
236+
237+
namespace is_pushout
238+
239+
variables {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P}
240+
241+
lemma flip (h : is_pushout f g inl inr) : is_pushout g f inr inl :=
242+
of_is_colimit (@pushout_cocone.flip_is_colimit _ _ _ _ _ _ _ _ _ _ h.w.symm h.is_colimit)
243+
244+
section
245+
246+
variables [has_zero_object C] [has_zero_morphisms C]
247+
open_locale zero_object
248+
249+
/-- The square with `0 : 0 ⟶ 0` on the right and `𝟙 X` on the left is a pushout square. -/
250+
lemma zero_right (X : C) : is_pushout (0 : X ⟶ 0) (𝟙 X) (0 : 0 ⟶ 0) (0 : X ⟶ 0) :=
251+
{ w := by simp,
252+
is_colimit' :=
253+
⟨{ desc := λ s, 0,
254+
fac' := λ s, begin
255+
have c := @pushout_cocone.coequalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _) (by simp)
256+
(by simpa using (pushout_cocone.condition s)),
257+
dsimp at c,
258+
simpa using c,
259+
end }⟩ }
260+
261+
/-- The square with `0 : 0 ⟶ 0` on the bottom and `𝟙 X` on the top is a pushout square. -/
262+
lemma zero_bot (X : C) : is_pushout (𝟙 X) (0 : X ⟶ 0) (0 : X ⟶ 0) (0 : 0 ⟶ 0) :=
263+
(zero_right X).flip
264+
265+
end
266+
267+
/-- Paste two pushout squares "vertically" to obtain another pushout square. -/
268+
-- Objects here are arranged in a 3x2 grid, and indexed by their xy coordinates.
269+
-- Morphisms are named `hᵢⱼ` for a horizontal morphism starting at `(i,j)`,
270+
-- and `vᵢⱼ` for a vertical morphism starting at `(i,j)`.
271+
lemma paste_vert {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
272+
{h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂}
273+
{v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂}
274+
(s : is_pushout h₁₁ v₁₁ v₁₂ h₂₁) (t : is_pushout h₂₁ v₂₁ v₂₂ h₃₁) :
275+
is_pushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ :=
276+
(of_is_colimit
277+
(big_square_is_pushout _ _ _ _ _ _ _ s.w t.w t.is_colimit s.is_colimit))
278+
279+
/-- Paste two pushout squares "horizontally" to obtain another pushout square. -/
280+
lemma paste_horiz {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
281+
{h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃}
282+
{v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃}
283+
(s : is_pushout h₁₁ v₁₁ v₁₂ h₂₁) (t : is_pushout h₁₂ v₁₂ v₁₃ h₂₂) :
284+
is_pushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) :=
285+
(paste_vert s.flip t.flip).flip
286+
287+
/-- Given a pushout square assembled from a pushout square on the top and
288+
a commuting square on the bottom, the bottom square is a pushout square. -/
289+
lemma of_bot {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C}
290+
{h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂}
291+
{v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂}
292+
(s : is_pushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁) (p : h₂₁ ≫ v₂₂ = v₂₁ ≫ h₃₁)
293+
(t : is_pushout h₁₁ v₁₁ v₁₂ h₂₁) :
294+
is_pushout h₂₁ v₂₁ v₂₂ h₃₁ :=
295+
of_is_colimit (right_square_is_pushout _ _ _ _ _ _ _ _ p t.is_colimit s.is_colimit)
296+
297+
/-- Given a pushout square assembled from a pushout square on the left and
298+
a commuting square on the right, the right square is a pushout square. -/
299+
lemma of_right {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C}
300+
{h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃}
301+
{v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃}
302+
(s : is_pushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂)) (p : h₁₂ ≫ v₁₃ = v₁₂ ≫ h₂₂)
303+
(t : is_pushout h₁₁ v₁₁ v₁₂ h₂₁) :
304+
is_pushout h₁₂ v₁₂ v₁₃ h₂₂ :=
305+
(of_bot s.flip p.symm t.flip).flip
306+
307+
end is_pushout
308+
309+
310+
end category_theory.limits

‎src/category_theory/limits/shapes/pullbacks.lean‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -405,6 +405,12 @@ abbreviation fst (t : pullback_cone f g) : t.X ⟶ X := t.π.app walking_cospan.
405405
/-- The second projection of a pullback cone. -/
406406
abbreviation snd (t : pullback_cone f g) : t.X ⟶ Y := t.π.app walking_cospan.right
407407

408+
@[simp] lemma condition_one (t : pullback_cone f g) : t.π.app walking_cospan.one = t.fst ≫ f :=
409+
begin
410+
have w := t.π.naturality walking_cospan.hom.inl,
411+
dsimp at w, simpa using w,
412+
end
413+
408414
/-- This is a slightly more convenient method to verify that a pullback cone is a limit cone. It
409415
only asks for a proof of facts that carry any mathematical content -/
410416
def is_limit_aux (t : pullback_cone f g) (lift : Π (s : pullback_cone f g), s.X ⟶ t.X)
@@ -476,6 +482,19 @@ lemma mono_fst_of_is_pullback_of_mono {t : pullback_cone f g} (ht : is_limit t)
476482
mono t.fst :=
477483
⟨λ W h k i, is_limit.hom_ext ht i (by simp [←cancel_mono g, ←t.condition, reassoc_of i])⟩
478484

485+
/-- To construct an isomorphism of pullback cones, it suffices to construct an isomorphism
486+
of the cone points and check it commutes with `fst` and `snd`. -/
487+
def ext {s t : pullback_cone f g} (i : s.X ≅ t.X)
488+
(w₁ : s.fst = i.hom ≫ t.fst) (w₂ : s.snd = i.hom ≫ t.snd) :
489+
s ≅ t :=
490+
begin
491+
apply cones.ext i,
492+
rintro (⟨⟩|⟨⟨⟩⟩),
493+
{ rw [condition_one, condition_one, w₁, category.assoc], },
494+
{ exact w₁, },
495+
{ exact w₂, },
496+
end
497+
479498
/-- If `t` is a limit pullback cone over `f` and `g` and `h : W ⟶ X` and `k : W ⟶ Y` are such that
480499
`h ≫ f = k ≫ g`, then we have `l : W ⟶ t.X` satisfying `l ≫ fst t = h` and `l ≫ snd t = k`.
481500
-/
@@ -583,6 +602,12 @@ abbreviation inl (t : pushout_cocone f g) : Y ⟶ t.X := t.ι.app walking_span.l
583602
/-- The second inclusion of a pushout cocone. -/
584603
abbreviation inr (t : pushout_cocone f g) : Z ⟶ t.X := t.ι.app walking_span.right
585604

605+
@[simp] lemma condition_zero (t : pushout_cocone f g) : t.ι.app walking_span.zero = f ≫ t.inl :=
606+
begin
607+
have w := t.ι.naturality walking_span.hom.fst,
608+
dsimp at w, simpa using w.symm,
609+
end
610+
586611
/-- This is a slightly more convenient method to verify that a pushout cocone is a colimit cocone.
587612
It only asks for a proof of facts that carry any mathematical content -/
588613
def is_colimit_aux (t : pushout_cocone f g) (desc : Π (s : pushout_cocone f g), t.X ⟶ s.X)
@@ -660,6 +685,19 @@ lemma epi_inl_of_is_pushout_of_epi {t : pushout_cocone f g} (ht : is_colimit t)
660685
epi t.inl :=
661686
⟨λ W h k i, is_colimit.hom_ext ht i (by simp [←cancel_epi g, ←t.condition_assoc, i])⟩
662687

688+
/-- To construct an isomorphism of pushout cocones, it suffices to construct an isomorphism
689+
of the cocone points and check it commutes with `inl` and `inr`. -/
690+
def ext {s t : pushout_cocone f g} (i : s.X ≅ t.X)
691+
(w₁ : s.inl ≫ i.hom = t.inl) (w₂ : s.inr ≫ i.hom = t.inr) :
692+
s ≅ t :=
693+
begin
694+
apply cocones.ext i,
695+
rintro (⟨⟩|⟨⟨⟩⟩),
696+
{ rw [condition_zero, condition_zero, category.assoc, w₁], },
697+
{ exact w₁, },
698+
{ exact w₂, },
699+
end
700+
663701
/--
664702
This is a more convenient formulation to show that a `pushout_cocone` constructed using
665703
`pushout_cocone.mk` is a colimit cocone.

0 commit comments

Comments
 (0)