Skip to content

doc(CategoryTheory): fix typos#38413

Open
yuanyi-350 wants to merge 40 commits intoleanprover-community:masterfrom
yuanyi-350:cat-doc2
Open

doc(CategoryTheory): fix typos#38413
yuanyi-350 wants to merge 40 commits intoleanprover-community:masterfrom
yuanyi-350:cat-doc2

Conversation

@yuanyi-350
Copy link
Copy Markdown
Collaborator

@yuanyi-350 yuanyi-350 commented Apr 23, 2026

In this PR, we used a Codex agent to scan the CategoryTheory directory to check for typos in the docstrings. We picked out some of the more obvious errors to fix in this PR.

Co-authored-by: @LehengChen


Open in Gitpod

yuanyi-350 and others added 30 commits April 13, 2026 10:18
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0015
target_path: Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0015

(cherry picked from commit 2771f28e0e6bd5eee3f35719ef3fcf59583f7fe6)
(cherry picked from commit a93f654)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0018
target_path: Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0018

(cherry picked from commit e0ce8805bd54e1d376b6a305c22a1595693063b4)
(cherry picked from commit 88b989a)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0020
target_path: Mathlib/CategoryTheory/Abelian/Injective/Basic.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0020

(cherry picked from commit d9d4bb83054307bf7969662aaea1830dc6f66f97)
(cherry picked from commit c30a323)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0036
target_path: Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0036

(cherry picked from commit 0bc033118d636b0419c597b08811a2e4da3eb0e8)
(cherry picked from commit f3069ac)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0046
target_path: Mathlib/CategoryTheory/Action/Continuous.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0046

(cherry picked from commit 17243d3480c3d162c0f3c79a293a67920c386007)
(cherry picked from commit e2a6dfb)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0053
target_path: Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0053

(cherry picked from commit 6d0d2227661b750c8578333e7afc0698449757fa)
(cherry picked from commit 10a4894)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0069
target_path: Mathlib/CategoryTheory/Adjunction/Triple.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0069

(cherry picked from commit c21d7125fa7116faa0eb57fd515d2d6b24dde2a7)
(cherry picked from commit 5b21d37)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0141
target_path: Mathlib/CategoryTheory/Center/Localization.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0141

(cherry picked from commit 03fe833273a94b0f6c856053080abf7f7ac5a976)
(cherry picked from commit 0a0fbc9)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0183
target_path: Mathlib/CategoryTheory/Discrete/SumsProducts.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0183

(cherry picked from commit e5dd7b16a72d35eb76782128e29e04eecb7ea928)
(cherry picked from commit 7b1f4f2)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0200
target_path: Mathlib/CategoryTheory/Enriched/Limits/HasConicalPullbacks.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0200

(cherry picked from commit d403a9cb2cc860c38a6fdf4bd589582894fc4494)
(cherry picked from commit e030567)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0215
target_path: Mathlib/CategoryTheory/FiberedCategory/Fiber.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0215

(cherry picked from commit 536ca90957d4724276cb45b9dd7b9304e928765c)
(cherry picked from commit 7686710)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0226
target_path: Mathlib/CategoryTheory/FinCategory/AsType.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0226

(cherry picked from commit 4c2ca3df242a5bf4eb1e32ce4ff2be9b8bd69ff1)
(cherry picked from commit 390342e)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0231
target_path: Mathlib/CategoryTheory/Functor/Const.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0231

(cherry picked from commit 9e14766bbbc128d85c2ac6caeb58a3120f507860)
(cherry picked from commit 76ee3e5)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0238
target_path: Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0238

(cherry picked from commit 87555544ec960c8327c1647b0536d51957ff6b22)
(cherry picked from commit 1c3cb96)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0249
target_path: Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0249

(cherry picked from commit 7e920a8d3f03086c574bab69a809ef4075c157c2)
(cherry picked from commit ec7d346)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0251
target_path: Mathlib/CategoryTheory/Functor/OfSequence.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0251

(cherry picked from commit 0425689b537d5db792aee20b2c780714879d34fd)
(cherry picked from commit 8826680)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0255
target_path: Mathlib/CategoryTheory/Functor/Trifunctor.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0255

(cherry picked from commit cbbb501356ae7dcc67d7b17dd82865260e466706)
(cherry picked from commit 890cacc)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0277
target_path: Mathlib/CategoryTheory/GradedObject/Bifunctor.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0277

(cherry picked from commit c78fcaacb9b0e887e27dac1da93f79602dcc7a37)
(cherry picked from commit ebda03c)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0285
target_path: Mathlib/CategoryTheory/Groupoid/Basic.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0285

(cherry picked from commit 040850742379cf2ecee7d197a4f2662145a6e5e2)
(cherry picked from commit a32dc1f)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0307
target_path: Mathlib/CategoryTheory/IsomorphismClasses.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0307

(cherry picked from commit 78812bfc44e9151acb3b76faca0a1240c49768c7)
(cherry picked from commit 26e2edc)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0309
target_path: Mathlib/CategoryTheory/Join/Final.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0309

(cherry picked from commit bef213aa5deb619829fc14b03f72987b6791150a)
(cherry picked from commit 37242a4)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0340
target_path: Mathlib/CategoryTheory/Limits/ExactFunctor.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0340

(cherry picked from commit 621eaa1079ed6ba77a5917178bce2f7506a9337c)
(cherry picked from commit abaf42f)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0341
target_path: Mathlib/CategoryTheory/Limits/Filtered.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0341

(cherry picked from commit 9d32330a853ad40d4f0d1b7f01300a6d7e1750d0)
(cherry picked from commit ad71410)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0373
target_path: Mathlib/CategoryTheory/Limits/Opposites.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0373

(cherry picked from commit 453638ea5f9069bdfdd22fd38c0f9de3cc7a69cd)
(cherry picked from commit e438206)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0394
target_path: Mathlib/CategoryTheory/Limits/Preserves/Shapes/Images.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0394

(cherry picked from commit 55fa62249a14e16c8cfcaebaace3f29ee00aed29)
(cherry picked from commit 04c146f)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0446
target_path: Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0446

(cherry picked from commit 7d9ed6358a7b115744bec4520f5a159e271b4694)
(cherry picked from commit 22ab947)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0450
target_path: Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0450

(cherry picked from commit 0f859a762dcbdc9713f0ebb5daae566279304c58)
(cherry picked from commit d0662a6)
LehengChen and others added 9 commits April 22, 2026 22:21
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0462
target_path: Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0462

(cherry picked from commit 731cc6d17102955a144fdae2e73b935d39cab3ee)
(cherry picked from commit 63fc09e)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0470
target_path: Mathlib/CategoryTheory/Limits/SmallComplete.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0470

(cherry picked from commit 994af14b67b90e4b536fc97d6cbc38be85dc7ad8)
(cherry picked from commit f8a638b)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0485
target_path: Mathlib/CategoryTheory/Limits/Types/Yoneda.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0485

(cherry picked from commit fbb5a536c3099499a3a68e7d369f135baad81f72)
(cherry picked from commit 075fd60)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0501
target_path: Mathlib/CategoryTheory/Localization/DerivabilityStructure/Basic.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0501

(cherry picked from commit 11405ef2416efca9c8b5d9d3d65d3b67490d448e)
(cherry picked from commit aba7f81)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0523
target_path: Mathlib/CategoryTheory/Localization/SmallShiftedHom.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0523

(cherry picked from commit f6e33b995e7d5a253033d47dce48447c760654d5)
(cherry picked from commit a4505f0)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0529
target_path: Mathlib/CategoryTheory/LocallyCartesianClosed/Over.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0529

(cherry picked from commit c7c1618380570fc0efeb65bd5d2fa5fc7be75a24)
(cherry picked from commit c7ca156)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0546
target_path: Mathlib/CategoryTheory/Monoidal/Action/End.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0546

(cherry picked from commit 370a39091a1eb44655fc294703202c2f68a21afe)
(cherry picked from commit c475c79)
task_id: docstring-repair-categorytheory-v1-fullscan-20260422-0552
target_path: Mathlib/CategoryTheory/Monoidal/Braided/Multifunctor.lean
artifact_path: /AI4M/users/lhchen/shouyi/results/candidates/docstring-repair-categorytheory-v1-fullscan-20260422-0552

(cherry picked from commit 7d76ae6ff64517b116d3f8ce1bc0ca77bbebbc78)
(cherry picked from commit a76c359)
@github-actions github-actions Bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Apr 23, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 23, 2026

PR summary c290b55c6e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.


No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@yuanyi-350 yuanyi-350 requested a review from chrisflav April 23, 2026 14:42
@yuanyi-350 yuanyi-350 added LLM-generated PRs with substantial input from LLMs - review accordingly codex OpenAI Codex wrote (parts of) this PR. t-category-theory Category theory documentation Improvements or additions to documentation labels Apr 23, 2026
@grunweg grunweg changed the title doc(Categorytheory): fix typos doc(CategoryTheory): fix typos Apr 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

codex OpenAI Codex wrote (parts of) this PR. documentation Improvements or additions to documentation LLM-generated PRs with substantial input from LLMs - review accordingly t-category-theory Category theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants