From 0ad528f8c105bc4df65a59a3dc753a171c1a7372 Mon Sep 17 00:00:00 2001 From: Pedro Cortes Date: Sat, 18 Apr 2026 17:02:38 -0300 Subject: [PATCH 1/2] =?UTF-8?q?feat(CategoryTheory/Monoidal):=20tensor?= =?UTF-8?q?=CE=BC=5Fbraid=5Fswap=20and=20tensor-product=20IsCommComonObj?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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). --- Mathlib.lean | 1 + .../Monoidal/Symmetric/TensorBraidSwap.lean | 71 +++++++++++++++++++ 2 files changed, 72 insertions(+) create mode 100644 Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean diff --git a/Mathlib.lean b/Mathlib.lean index 1d25f1feb37561..9d5134575b9cda 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3073,6 +3073,7 @@ public import Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory public import Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence public import Mathlib.CategoryTheory.Monoidal.Skeleton public import Mathlib.CategoryTheory.Monoidal.Subcategory +public import Mathlib.CategoryTheory.Monoidal.Symmetric.TensorBraidSwap public import Mathlib.CategoryTheory.Monoidal.Tor public import Mathlib.CategoryTheory.Monoidal.Transport public import Mathlib.CategoryTheory.Monoidal.Types.Basic diff --git a/Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean b/Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean new file mode 100644 index 00000000000000..ff374b1a42a918 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Pedro Cortes. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Pedro Cortes +-/ +module + +public import Mathlib.CategoryTheory.Monoidal.Braided.Basic +public import Mathlib.CategoryTheory.Monoidal.CommComon_ + +/-! +# Tensor-braid swap coherence in symmetric monoidal categories + +The canonical rearrangement `tensorμ` intertwines the braiding on `A ⊗ Y` +with the pair of braidings on `A` and `Y` in any symmetric monoidal +category. This is the sibling of `CategoryTheory.MonObj.mul_braiding` +(`Mathlib.CategoryTheory.Monoidal.Mon_`), and yields the tensor-product +`IsCommComonObj` instance. + +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. +-/ + +@[expose] public section + +universe v u + +namespace CategoryTheory + +open MonoidalCategory BraidedCategory + +variable {C : Type u} [Category.{v} C] [MonoidalCategory C] [SymmetricCategory C] + +/-- **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_`). -/ +@[reassoc] +theorem MonoidalCategory.tensorμ_braid_swap (A Y : C) : + tensorμ A A Y Y ≫ (β_ (A ⊗ Y) (A ⊗ Y)).hom = + ((β_ A A).hom ⊗ₘ (β_ Y Y).hom) ≫ tensorμ A A Y Y := by + 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 + +open scoped ComonObj + +/-- 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`. -/ +instance (A B : C) [ComonObj A] [ComonObj B] + [IsCommComonObj A] [IsCommComonObj B] : IsCommComonObj (A ⊗ B) where + comul_comm := by + rw [Comon.tensorObj_comul, Category.assoc, + MonoidalCategory.tensorμ_braid_swap, + ← Category.assoc, tensorHom_comp_tensorHom, + IsCommComonObj.comul_comm A, IsCommComonObj.comul_comm B] + +end CategoryTheory From db62ead939bc534fc4b388b2d2c6bc54d5605369 Mon Sep 17 00:00:00 2001 From: Pedro Cortes Date: Thu, 23 Apr 2026 22:18:17 -0300 Subject: [PATCH 2/2] Address review: inline into existing files, drop docstrings, adopt suggested proofs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - tensorμ_braid_swap moved into Braided/Basic.lean under a new [SymmetricCategory C] section (no instance diamond after all). - IsCommComonObj (A ⊗ B) instance moved into CommComon_.lean under a new [SymmetricCategory C] section. - Deleted the new file Symmetric/TensorBraidSwap.lean and its registration in Mathlib.lean. - Dropped docstrings on both declarations. - Adopted Dagur's suggested proof bodies verbatim. --- Mathlib.lean | 1 - .../Monoidal/Braided/Basic.lean | 16 +++++ .../CategoryTheory/Monoidal/CommComon_.lean | 12 ++++ .../Monoidal/Symmetric/TensorBraidSwap.lean | 71 ------------------- 4 files changed, 28 insertions(+), 72 deletions(-) delete mode 100644 Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean diff --git a/Mathlib.lean b/Mathlib.lean index 9d5134575b9cda..1d25f1feb37561 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3073,7 +3073,6 @@ public import Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory public import Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence public import Mathlib.CategoryTheory.Monoidal.Skeleton public import Mathlib.CategoryTheory.Monoidal.Subcategory -public import Mathlib.CategoryTheory.Monoidal.Symmetric.TensorBraidSwap public import Mathlib.CategoryTheory.Monoidal.Tor public import Mathlib.CategoryTheory.Monoidal.Transport public import Mathlib.CategoryTheory.Monoidal.Types.Basic diff --git a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean index 735c177d7f0ef5..384ad0c06874ae 100644 --- a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean @@ -777,6 +777,22 @@ lemma tensorμ_comp_μ_tensorHom_μ_comp_μ (F : C ⥤ D) [F.LaxBraided] (W X Y end Tensor +section Symmetric + +variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory C] [SymmetricCategory C] + +@[reassoc] +theorem tensorμ_braid_swap (A Y : C) : + tensorμ A A Y Y ≫ (β_ (A ⊗ Y) (A ⊗ Y)).hom = + ((β_ A A).hom ⊗ₘ (β_ Y Y).hom) ≫ tensorμ A A Y Y := by + 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] + +end Symmetric + end MonoidalCategory instance : BraidedCategory Cᵒᵖ where diff --git a/Mathlib/CategoryTheory/Monoidal/CommComon_.lean b/Mathlib/CategoryTheory/Monoidal/CommComon_.lean index 3969d39b1dd1e6..0383de7f1be89a 100644 --- a/Mathlib/CategoryTheory/Monoidal/CommComon_.lean +++ b/Mathlib/CategoryTheory/Monoidal/CommComon_.lean @@ -98,4 +98,16 @@ end end CommComon +section Symmetric + +variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] [SymmetricCategory C] + +instance (A B : C) [ComonObj A] [ComonObj B] + [IsCommComonObj A] [IsCommComonObj B] : IsCommComonObj (A ⊗ B) where + comul_comm := by + rw [Comon.tensorObj_comul, Category.assoc, MonoidalCategory.tensorμ_braid_swap] + simp + +end Symmetric + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean b/Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean deleted file mode 100644 index ff374b1a42a918..00000000000000 --- a/Mathlib/CategoryTheory/Monoidal/Symmetric/TensorBraidSwap.lean +++ /dev/null @@ -1,71 +0,0 @@ -/- -Copyright (c) 2026 Pedro Cortes. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Pedro Cortes --/ -module - -public import Mathlib.CategoryTheory.Monoidal.Braided.Basic -public import Mathlib.CategoryTheory.Monoidal.CommComon_ - -/-! -# Tensor-braid swap coherence in symmetric monoidal categories - -The canonical rearrangement `tensorμ` intertwines the braiding on `A ⊗ Y` -with the pair of braidings on `A` and `Y` in any symmetric monoidal -category. This is the sibling of `CategoryTheory.MonObj.mul_braiding` -(`Mathlib.CategoryTheory.Monoidal.Mon_`), and yields the tensor-product -`IsCommComonObj` instance. - -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. --/ - -@[expose] public section - -universe v u - -namespace CategoryTheory - -open MonoidalCategory BraidedCategory - -variable {C : Type u} [Category.{v} C] [MonoidalCategory C] [SymmetricCategory C] - -/-- **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_`). -/ -@[reassoc] -theorem MonoidalCategory.tensorμ_braid_swap (A Y : C) : - tensorμ A A Y Y ≫ (β_ (A ⊗ Y) (A ⊗ Y)).hom = - ((β_ A A).hom ⊗ₘ (β_ Y Y).hom) ≫ tensorμ A A Y Y := by - 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 - -open scoped ComonObj - -/-- 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`. -/ -instance (A B : C) [ComonObj A] [ComonObj B] - [IsCommComonObj A] [IsCommComonObj B] : IsCommComonObj (A ⊗ B) where - comul_comm := by - rw [Comon.tensorObj_comul, Category.assoc, - MonoidalCategory.tensorμ_braid_swap, - ← Category.assoc, tensorHom_comp_tensorHom, - IsCommComonObj.comul_comm A, IsCommComonObj.comul_comm B] - -end CategoryTheory