feat(CategoryTheory/Monoidal): tensorμ_braid_swap and tensor-product IsCommComonObj

[pedroscortes]

---

Summary

Two symmetric-monoidal coherence results in a new file
Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean:

1. MonoidalCategory.tensorμ_braid_swap — canonical rearrangement
   tensorμ A A Y Y intertwines the braiding on A ⊗ Y with the
   pair of braidings on A and Y. Sibling of
   CategoryTheory.MonObj.mul_braiding
   (Mathlib.CategoryTheory.Monoidal.Mon_, line 759).

2. Tensor-product instance for IsCommComonObj: if A, B carry
   commutative comonoid structures in a symmetric monoidal category,
   so does A ⊗ B. Reduces comul_comm for Δ[A ⊗ B] via
   tensorμ_braid_swap to the pointwise hypotheses. Fills a gap
   in Mathlib/CategoryTheory/Monoidal/CommComon_.lean, which
   currently provides only the unit instance
   (instCommComonObjUnit) and the auto-instance for cartesian
   categories (instIsCommComonObjOfCartesian).

Placement rationale

Placed in a new Symmetric/ subdirectory rather than appended
to Braided/Basic.lean because the latter's top-level
variable [BraidedCategory C] creates an instance diamond
against any locally-added [SymmetricCategory C]. On v4.30.0-rc2
this diamond blocks rw [SymmetricCategory.symmetry] motive
extraction through A ◁ _ ▷ Y — the pattern is literally present
in the target, but the two distinct BraidedCategory C instances
(outer variable vs SymmetricCategory.toBraidedCategory) cause
the rewrite to fail. A new file with only
[SymmetricCategory C] as its variable avoids this.

Downstream consumer

The IsCommComonObj tensor-product instance is load-bearing for
the external library
markovcat (formalising
Fritz–Klingler Markov categories), specifically for symmetry of
the conditional-independence predicate on compound objects.

Checks

• lake build Mathlib.CategoryTheory.Monoidal.Symmetric.TensorBraidSwap — green.
• lake exe lint-style — clean (exit 0).
• Rebased onto current master; single commit; 72 insertions across
  two files (new file + one-line Mathlib.lean registration).

Opening as draft to let CI run before requesting review.

[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 0f2d2ac8ba

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Monoidal.Symmetric.TensorBraidSwap (new file)	471

---

Declarations diff

+ MonoidalCategory.tensorμ_braid_swap
+ instance (A B : C) [ComonObj A] [ComonObj B]

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.

You can run this locally as

./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).