Skip to content

Commit 59c724d

Browse files
committed
doc: fix typo in pullback diagram (#29141)
The label of an arrow `fst` was incorrectly marked as `snd` in a pullback square appearing in header documentation. Co-authored-by: jlh18 <josephhua73@yahoo.com>
1 parent 272e8f7 commit 59c724d

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -21,13 +21,13 @@ pullacks.
2121
* `pullback f g`: Given a `HasPullback f g` instance, this function returns the choice of a limit
2222
object corresponding to the pullback of `f` and `g`. It fits into the following diagram:
2323
```
24-
pullback f g ---pullback.snd f g---> Y
24+
pullback f g ---pullback.fst f g---> X
2525
| |
2626
| |
27-
pullback.snd f g g
27+
pullback.snd f g f
2828
| |
2929
v v
30-
X --------------f--------------> Z
30+
Y --------------g--------------> Z
3131
```
3232
3333
* `HasPushout f g`: this is an abbreviation for `HasColimit (span f g)`, and is a typeclass used to
@@ -39,10 +39,10 @@ pullback.snd f g g
3939
```
4040
X --------------f--------------> Y
4141
| |
42-
g pushout.inr f g
42+
g pushout.inl f g
4343
| |
4444
v v
45-
Z ---pushout.inl f g---> pushout f g
45+
Z ---pushout.inr f g---> pushout f g
4646
```
4747
4848
# Main results & API

0 commit comments

Comments
 (0)