feat(CategoryTheory/Monoidal): tensorμ_braid_swap and tensor-product IsCommComonObj#38314
Conversation
…IsCommComonObj Adds two symmetric-monoidal coherence results in a new file `Mathlib.CategoryTheory.Monoidal.Symmetric.TensorBraidSwap`: * `MonoidalCategory.tensorμ_braid_swap` — the canonical rearrangement `tensorμ A A Y Y : (A ⊗ A) ⊗ (Y ⊗ Y) ⟶ (A ⊗ Y) ⊗ (A ⊗ 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) which closes a structurally adjacent equation by the same simp + slice recipe. * Tensor-product instance for `IsCommComonObj`: if `A` and `B` carry commutative comonoid structures in a symmetric monoidal category, so does `A ⊗ B`. Reduces commutativity of `Δ[A ⊗ B]` via `tensorμ_braid_swap` to the pointwise hypotheses on `A` and `B`. ## Placement rationale These live in a new `Symmetric/` subdirectory rather than being appended to `Braided/Basic.lean` because the latter's top-level `variable [BraidedCategory C]` creates an instance diamond with any locally-added `[SymmetricCategory C]`. On Lean v4.30.0-rc2 that diamond blocks `rw [SymmetricCategory.symmetry]` motive extraction through `A ◁ _ ▷ Y` — even though the pattern is literally present in the target, the two distinct `BraidedCategory C` instances (outer variable vs `SymmetricCategory.toBraidedCategory`) cause the rewrite to fail. A clean file with only `[SymmetricCategory C]` as its variable avoids this. ## Downstream consumers The tensor-product `IsCommComonObj` instance is load-bearing for the `markovcat` library (external, https://github.com/pedroscortes/markovcat) formalising Markov categories — specifically for proving symmetry of the Fritz-Klingler conditional-independence predicate. Refs: Fritz 2020 *Adv. Math.* 370; Fritz-Klingler, *JMLR* 24(46) (2023).
github-actions
Bot
added
the
new-contributor
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 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. |
PR summary 8f4785ceefImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
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 No changes to technical debt.This script lives in the
|
Did you use AI to generate this PR? |
dagurtomas
added
awaiting-author
hi @dagurtomas! quick context: I'm finishing my masters in cs at the Federal University of Espírito Santo, working on categorical foundations of causal inference. these two lemmas came up as a genuine gap while I was building markovcat (still private while my thesis is in progress), a Lean 4 library formalizing Fritz 2020 arkov categories and Fritz–Klingler 2023 d-separation. I expect a handful of similar coherence gaps will keep surfacing as I push further into the formalization, so I'll probably be sending a few more PRs of this flavor over the next year or two. |
dagurtomas
left a comment
dagurtomas
left a comment
There was a problem hiding this comment.
There is no need for a new file, you can just put these two declarations in Monoidal/Braided/Basic.lean and Monoidal/CommComon_.lean.
This looks very AI-generated (the wordiness of the docstrings and the heavy use of markdown in both docstrings and PR description). I'll give you the benefit of the doubt this time, but I ask you to please be honest with disclosing AI use.
| Placed in its own file to avoid an instance-diamond issue in `Braided/Basic.lean`, | ||
| where the ambient `[BraidedCategory C]` variable clashes with the | ||
| `[SymmetricCategory C]`-derived `BraidedCategory` instance, confusing | ||
| `rw [SymmetricCategory.symmetry]` motive extraction on Lean v4.30.0-rc2. |
There was a problem hiding this comment.
There is no diamond, SymmetricCategory extends BraidedCategory. You just need to make sure not to have both assumptions [BraidedCategory C] and [SymmetricCategory C] around, so just put it in its own section with only a
[SymmetricCategory C] assumption.
| /-- **Symmetric-monoidal tensor-braid swap coherence.** | ||
| The canonical rearrangement `tensorμ` intertwines the braiding on `A ⊗ Y` | ||
| with the pair of braidings on `A` and `Y`. Both sides implement the | ||
| permutation `(a₁, a₂, y₁, y₂) ↦ (a₂, y₂, a₁, y₁)`. Sibling of | ||
| `MonObj.mul_braiding` (`Mathlib.CategoryTheory.Monoidal.Mon_`). -/ |
There was a problem hiding this comment.
This docstring is unnecessary
| simp only [tensorμ, Category.assoc, | ||
| BraidedCategory.braiding_tensor_right_hom, | ||
| BraidedCategory.braiding_tensor_left_hom, comp_whiskerRight, | ||
| whisker_assoc, whiskerLeft_comp, pentagon_assoc, | ||
| pentagon_inv_hom_hom_hom_inv_assoc, Iso.inv_hom_id_assoc, | ||
| whiskerLeft_hom_inv_assoc] | ||
| slice_lhs 3 4 => rw [← whiskerLeft_comp, ← comp_whiskerRight, | ||
| SymmetricCategory.symmetry] | ||
| simp only [id_whiskerRight, whiskerLeft_id, Category.id_comp, Category.assoc, | ||
| tensorHom_def, tensor_whiskerLeft, whiskerRight_tensor] | ||
| monoidal |
There was a problem hiding this comment.
| simp only [tensorμ, Category.assoc, | |
| BraidedCategory.braiding_tensor_right_hom, | |
| BraidedCategory.braiding_tensor_left_hom, comp_whiskerRight, | |
| whisker_assoc, whiskerLeft_comp, pentagon_assoc, | |
| pentagon_inv_hom_hom_hom_inv_assoc, Iso.inv_hom_id_assoc, | |
| whiskerLeft_hom_inv_assoc] | |
| slice_lhs 3 4 => rw [← whiskerLeft_comp, ← comp_whiskerRight, | |
| SymmetricCategory.symmetry] | |
| simp only [id_whiskerRight, whiskerLeft_id, Category.id_comp, Category.assoc, | |
| tensorHom_def, tensor_whiskerLeft, whiskerRight_tensor] | |
| monoidal | |
| -- simp? [tensorμ] says: | |
| simp only [tensorμ, braiding_tensor_right_hom, braiding_tensor_left_hom, comp_whiskerRight, | |
| whisker_assoc, Category.assoc, whiskerLeft_comp, pentagon_assoc, | |
| pentagon_inv_hom_hom_hom_inv_assoc, Iso.inv_hom_id_assoc, whiskerLeft_hom_inv_assoc] | |
| slice_lhs 3 4 => rw [← whiskerLeft_comp, ← comp_whiskerRight, SymmetricCategory.symmetry] | |
| simp [tensorHom_def] |
| rw [Comon.tensorObj_comul, Category.assoc, | ||
| MonoidalCategory.tensorμ_braid_swap, | ||
| ← Category.assoc, tensorHom_comp_tensorHom, | ||
| IsCommComonObj.comul_comm A, IsCommComonObj.comul_comm B] |
There was a problem hiding this comment.
| rw [Comon.tensorObj_comul, Category.assoc, | |
| MonoidalCategory.tensorμ_braid_swap, | |
| ← Category.assoc, tensorHom_comp_tensorHom, | |
| IsCommComonObj.comul_comm A, IsCommComonObj.comul_comm B] | |
| rw [Comon.tensorObj_comul, Category.assoc, MonoidalCategory.tensorμ_braid_swap] | |
| simp |
| /-- The tensor product of two commutative comonoid objects is again a | ||
| commutative comonoid object. The proof reduces the commutativity | ||
| equation for `Δ[A ⊗ B]` to `tensorμ_braid_swap` plus the two pointwise | ||
| commutativity hypotheses `IsCommComonObj.comul_comm A`, `.comul_comm B`. -/ |
There was a problem hiding this comment.
This docstring is unnecessary
2 participants
Summary
Two symmetric-monoidal coherence results in a new file
Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean:MonoidalCategory.tensorμ_braid_swap— canonical rearrangementtensorμ A A Y Yintertwines the braiding onA ⊗ Ywith thepair of braidings on
AandY. Sibling ofCategoryTheory.MonObj.mul_braiding(
Mathlib.CategoryTheory.Monoidal.Mon_, line 759).Tensor-product instance for
IsCommComonObj: ifA, Bcarrycommutative comonoid structures in a symmetric monoidal category,
so does
A ⊗ B. Reducescomul_commforΔ[A ⊗ B]viatensorμ_braid_swapto the pointwise hypotheses. Fills a gapin
Mathlib/CategoryTheory/Monoidal/CommComon_.lean, whichcurrently provides only the unit instance
(
instCommComonObjUnit) and the auto-instance for cartesiancategories (
instIsCommComonObjOfCartesian).Placement rationale
Placed in a new
Symmetric/subdirectory rather than appendedto
Braided/Basic.leanbecause the latter's top-levelvariable [BraidedCategory C]creates an instance diamondagainst any locally-added
[SymmetricCategory C]. On v4.30.0-rc2this diamond blocks
rw [SymmetricCategory.symmetry]motiveextraction through
A ◁ _ ▷ Y— the pattern is literally presentin the target, but the two distinct
BraidedCategory Cinstances(outer variable vs
SymmetricCategory.toBraidedCategory) causethe rewrite to fail. A new file with only
[SymmetricCategory C]as its variable avoids this.Downstream consumer
The
IsCommComonObjtensor-product instance is load-bearing forthe 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).master; single commit; 72 insertions acrosstwo files (new file + one-line
Mathlib.leanregistration).Opening as draft to let CI run before requesting review.