feat(CategoryTheory/Limits/Shapes): add WalkingArrow category

[VictorBoscaro]

Summary

Adds CategoryTheory.Limits.WalkingArrow, the small category with two objects zero/one and a single non-identity morphism arrow : zero ⟶ one, at Mathlib/CategoryTheory/Limits/Shapes/WalkingArrow.lean. The SmallCategory instance is provided via an explicit WalkingArrowHom type family mirroring the design of WalkingParallelPairHom in Equalizers.lean. Functors WalkingArrow ⥤ C correspond to the data of a single morphism in C, i.e. to objects of the arrow category Arrow C (Mathlib.CategoryTheory.Comma.Arrow); the equivalence of categories is deferred to a follow-up PR.

Mathematical context

WalkingArrow is the freely generated category on a single non-identity morphism. It complements the existing small-fixture family — WalkingPair (two objects, no non-identity morphisms), WalkingParallelPair (two parallel non-identity morphisms), WalkingCospan, WalkingSpan — by providing the smallest non-discrete member: a single object-to-object arrow. The object names zero/one and the constructor naming style follow the WalkingParallelPair convention already in Equalizers.lean.

Where this could be used

• diagramIsoArrow shape-rewriting: Mirrors diagramIsoParallelPair (Mathlib.CategoryTheory.Limits.Shapes.Equalizers, line 251). A diagramIsoArrow would canonically rewrite any WalkingArrow ⥤ C to Arrow.mk-form, enabling hasLimit_of_iso/hasColimit_of_iso for arrow-shaped diagrams in the same style as the equalizer case.
• Functorial factorization: FunctorialFactorizationData (Mathlib.CategoryTheory.MorphismProperty.Factorization) stores a functor Arrow C ⥤ C together with natural transformations from/to Arrow.leftFunc and Arrow.rightFunc. The pending (WalkingArrow ⥤ C) ≌ Arrow C would let those natural transformations be expressed as evaluations at zero/one, simplifying transport lemmas for weak factorization systems.
• Small-object functor extensionality: Arrow.functor_ext (Mathlib.CategoryTheory.Comma.Arrow, line 421) is invoked multiple times in the small-object iteration proofs (Mathlib.CategoryTheory.SmallObject.Iteration.Basic). With WalkingArrow, the same extensionality principle can be stated shape-theoretically as agreement on the image of WalkingArrowHom.arrow, giving a uniform pattern across the Walking* family.
• ComposableArrows C 1 ≃ Arrow C unification: ComposableArrows.arrowEquiv (Mathlib.CategoryTheory.ComposableArrows.Basic, line 312) establishes ComposableArrows C 1 ≃ Arrow C at the type level; ComposableArrows C 1 is Fin 2 ⥤ C. A future WalkingArrow ≌ Fin 2 instance would make the categorical equivalence (WalkingArrow ⥤ C) ≌ Arrow C its canonical lifting, unifying the three presentations of a single morphism.

Notes

• Naming follows the Walking* convention: WalkingArrow (type, UpperCamelCase), WalkingArrowHom (morphism family), walkingArrowHomCategory (instance, lowerCamelCase), walkingArrowHom_id (theorem, snake_case).
• set_option genSizeOfSpec false applied to WalkingArrowHom to suppress the spurious sizeOf_spec lemma that triggers the simpNF linter on indexed inductives (same pattern as WalkingParallelPairHom).
• API is minimal — WalkingArrow ≌ Fin 2, the opposite functor, and the Arrow-C equivalence are left to follow-up PRs so that this PR is reviewable in one pass.
• No @[simp] lemmas for comp cases beyond walkingArrowHom_id and walkingArrowHom_comp_arrow_id; pattern is asymmetric (the arrow constructor has no further composition). Happy to add if preferred.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary b467b1be11

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Limits.Shapes.WalkingArrow (new file)	272

---

Declarations diff

+ WalkingArrow
+ WalkingArrowHom
+ WalkingArrowHom.assoc
+ WalkingArrowHom.comp
+ WalkingArrowHom.comp_id
+ WalkingArrowHom.id_comp
+ instance : Inhabited (WalkingArrowHom zero one)
+ walkingArrowHomCategory
+ walkingArrowHom_comp_arrow_id
+ walkingArrowHom_id

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.