[Merged by Bors] - feat(Kernel/Category): Stoch is a Markov category

Mathlib.lean

@@ -2516,6 +2516,7 @@ public import Mathlib.CategoryTheory.ConnectedComponents
 public import Mathlib.CategoryTheory.CopyDiscardCategory.Basic
 public import Mathlib.CategoryTheory.CopyDiscardCategory.Cartesian
 public import Mathlib.CategoryTheory.CopyDiscardCategory.Deterministic
+public import Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
 public import Mathlib.CategoryTheory.Core
 public import Mathlib.CategoryTheory.Countable
 public import Mathlib.CategoryTheory.Dialectica.Basic
@@ -3019,6 +3020,7 @@ public import Mathlib.CategoryTheory.Monoidal.Tor
 public import Mathlib.CategoryTheory.Monoidal.Transport
 public import Mathlib.CategoryTheory.Monoidal.Types.Basic
 public import Mathlib.CategoryTheory.Monoidal.Types.Coyoneda
+public import Mathlib.CategoryTheory.Monoidal.Widesubcategory
 public import Mathlib.CategoryTheory.MorphismProperty.Basic
 public import Mathlib.CategoryTheory.MorphismProperty.Comma
 public import Mathlib.CategoryTheory.MorphismProperty.CommaSites
@@ -5994,6 +5996,8 @@ public import Mathlib.Probability.Independence.Kernel.IndepFun
 public import Mathlib.Probability.Independence.Process
 public import Mathlib.Probability.Independence.ZeroOne
 public import Mathlib.Probability.Kernel.Basic
+public import Mathlib.Probability.Kernel.Category.SFinKer
+public import Mathlib.Probability.Kernel.Category.Stoch
 public import Mathlib.Probability.Kernel.CompProdEqIff
 public import Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous
 public import Mathlib.Probability.Kernel.Composition.Comp

Mathlib/CategoryTheory/CopyDiscardCategory/Widesubcategory.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+module
+
+public import Mathlib.CategoryTheory.Monoidal.Widesubcategory
+
+/-!
+# Copy-discard structures on wide subcategories
+
+Given a monoidal category `C`, a morphism property `P : MorphismProperty C` satisfying
+`P.IsMonoidalStable` and a comonoid object `c : C`, we introduce a condition `P.
+IsStableUnderComonoid c` saying that `c` inherits a comonoid object structure in the category of
+`WideSubcategory P`. If `C` is a copy-discard category, if `P` is also stable under braiding and
+that this condition `P. IsStableUnderComonoid` holds for all objects `c : C`, we show that
+`WideSubcategory P` is also a copy-discard category.
+-/
+
+@[expose] public section
+
+namespace CategoryTheory.MorphismProperty
+
+open scoped ComonObj
+
+variable {C : Type*} [Category* C] (P : MorphismProperty C) [MonoidalCategory C]
+
+/-- A braided-stable morphism property stable under comonoid counit and comultiplication. -/
+class IsStableUnderComonoid (P : MorphismProperty C) (c : C) [ComonObj c] : Prop where
+  counit_mem (P) : P ε[c]
+  comul_mem (P) : P Δ[c]
+
+export IsStableUnderComonoid (counit_mem comul_mem)
+
+@[simps]
+instance [P.IsMonoidalStable] (c : WideSubcategory P) [ComonObj c.obj]
+    [P.IsStableUnderComonoid c.obj] : ComonObj c where
+  counit := ⟨ε[c.obj], P.counit_mem⟩
+  comul := ⟨Δ[c.obj], P.comul_mem⟩
+
+instance [BraidedCategory C] [P.IsStableUnderBraiding] (c : WideSubcategory P) [ComonObj c.obj]
+    [IsCommComonObj c.obj] [P.IsStableUnderComonoid c.obj] : IsCommComonObj c where
+  comul_comm := by
+    ext
+    exact IsCommComonObj.comul_comm _
+
+open CopyDiscardCategory in
+attribute [local simp] copy_tensor discard_tensor copy_unit discard_unit in
+instance [CopyDiscardCategory C] [P.IsStableUnderBraiding] [∀ c, P.IsStableUnderComonoid c] :
+    CopyDiscardCategory (WideSubcategory P) where
+
+end CategoryTheory.MorphismProperty

Mathlib/CategoryTheory/Monoidal/Widesubcategory.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2026 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré
+-/
+
+module
+
+public import Mathlib.CategoryTheory.CopyDiscardCategory.Basic
+public import Mathlib.CategoryTheory.Localization.Monoidal.Basic
+public import Mathlib.CategoryTheory.Widesubcategory
+
+/-!
+# Monoidal structures on wide subcategories
+
+Given a monoidal category `C` and a morphism property `P : MorphismProperty C`,
+this file introduces conditions on `P` ensuring that `WideSubcategory P` inherits
+additional structures.
+
+We define stability classes under associators, unitors, and braidings, and use
+them to construct monoidal, braided, and symmetric structures on
+`WideSubcategory P`.
+
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open scoped MonoidalCategory ComonObj
+
+variable {C : Type*} [Category* C] (P : MorphismProperty C) [MonoidalCategory C]
+
+namespace MorphismProperty
+
+/-- A morphism property stable under associator isomorphisms of a monoidal category. -/
+class IsStableUnderAssociator (P : MorphismProperty C) : Prop where
+  associator_hom_mem (P) (c c' c'' : C) : P (α_ c c' c'').hom
+  associator_inv_mem (P) (c c' c'' : C) : P (α_ c c' c'').inv
+
+export IsStableUnderAssociator (associator_hom_mem associator_inv_mem)
+
+/-- A morphism property stable under left and right unitor isomorphisms. -/
+class IsStableUnderUnitor (P : MorphismProperty C) : Prop where
+  leftUnitor_hom_mem (P) (c : C) : P ((λ_ c).hom)
+  leftUnitor_inv_mem (P) (c : C) : P ((λ_ c).inv)
+  rightUnitor_hom_mem (P) (c : C) : P ((ρ_ c).hom)
+  rightUnitor_inv_mem (P) (c : C) : P ((ρ_ c).inv)
+
+export IsStableUnderUnitor (leftUnitor_hom_mem leftUnitor_inv_mem rightUnitor_hom_mem
+  rightUnitor_inv_mem)
+
+/-- A morphism property stable under tensoring, associators, and unitors. -/
+class IsMonoidalStable : Prop extends IsMonoidal P, IsStableUnderAssociator P,
+    IsStableUnderUnitor P
+
+/-- A monoidal-stable morphism property also stable under braiding isomorphisms. -/
+class IsStableUnderBraiding [BraidedCategory C] (P : MorphismProperty C) : Prop
+    extends IsMonoidalStable P where
+  braiding_hom_mem (P) (c c' : C) : P (β_ c c').hom
+  braiding_inv_mem (P) (c c' : C) : P (β_ c c').inv
+
+export IsStableUnderBraiding (braiding_hom_mem braiding_inv_mem)
+
+end MorphismProperty
+
+namespace WideSubcategory
+
+@[simps]
+instance [P.IsMonoidalStable] : MonoidalCategoryStruct (WideSubcategory P) where
+  tensorObj c c' := ⟨c.obj ⊗ c'.obj⟩
+  whiskerLeft c _ _ f := ⟨c.obj ◁ f.1, P.whiskerLeft_mem _ _ f.2⟩
+  whiskerRight f c' := ⟨f.1 ▷ c'.obj, P.whiskerRight_mem _ f.2 _⟩
+  tensorUnit := ⟨𝟙_ C⟩
+  associator _ _ _ :=
+    isoMk (α_ _ _ _) (P.associator_hom_mem _ _ _) (P.associator_inv_mem _ _ _)
+  leftUnitor _ :=
+    isoMk (λ_ _) (P.leftUnitor_hom_mem _) (P.leftUnitor_inv_mem _)
+  rightUnitor _ :=
+    isoMk (ρ_ _) (P.rightUnitor_hom_mem _) (P.rightUnitor_inv_mem _)
+  tensorHom f g := ⟨f.1 ⊗ₘ g.1, P.tensorHom_mem _ _ f.2 g.2⟩
+
+instance [P.IsMonoidalStable] : MonoidalCategory (WideSubcategory P) :=
+  Monoidal.induced (wideSubcategoryInclusion P)
+    { εIso := Iso.refl _
+      μIso _ _ := Iso.refl _ }
+
+instance [BraidedCategory C] [P.IsStableUnderBraiding] :
+    BraidedCategory (WideSubcategory P) where
+  braiding _ _ :=
+    isoMk (β_ _ _) (P.braiding_hom_mem _ _) (P.braiding_inv_mem _ _)
+
+variable {P} in
+open MonoidalCategory in
+@[simp]
+lemma tensorμ_hom [BraidedCategory C] [P.IsStableUnderBraiding] (X Y Z T : WideSubcategory P) :
+    (tensorμ X Y Z T).hom = tensorμ _ _ _ _ := rfl
+
+instance [SymmetricCategory C] [P.IsStableUnderBraiding] :
+    SymmetricCategory (WideSubcategory P) where
+  symmetry c c' := by
+    ext
+    exact SymmetricCategory.symmetry _ _
+
+end WideSubcategory
+
+end CategoryTheory

Mathlib/CategoryTheory/Widesubcategory.lean

@@ -53,10 +53,21 @@ instance InducedWideCategory.hasCoeToSort {α : Sort*} [CoeSort D α] :
     CoeSort (InducedWideCategory D F P) α :=
   ⟨fun c => F c⟩
 
+variable {F P} in
+/-- The type of morphisms in `InducedWideCategory D F P` between `X` and `Y`
+is a 2-field structure consisting of a morphism `F X ⟶ F Y` in `D` that satisfies
+the property `P`. -/
+@[ext]
+structure InducedWideCategory.Hom (X Y : InducedWideCategory D F P) where
+  /-- The underlying morphism. -/
+  hom : F X ⟶ F Y
+  /-- The property that the morphism satisfies. -/
+  property : P hom
+
 @[simps!]
 instance InducedWideCategory.category :
     Category (InducedWideCategory D F P) where
-  Hom X Y := {f : F X ⟶ F Y | P f}
+  Hom X Y := Hom X Y
   id X := ⟨𝟙 (F X), P.id_mem (F X)⟩
   comp {_ _ _} f g := ⟨f.1 ≫ g.1, P.comp_mem _ _ f.2 g.2⟩
 
@@ -92,6 +103,11 @@ structure WideSubcategory (_P : MorphismProperty C) [IsMultiplicative _P] where
 instance WideSubcategory.category : Category.{v₁} (WideSubcategory P) :=
   InducedWideCategory.category WideSubcategory.obj P
 
+@[ext]
+lemma WideSubcategory.hom_ext {X Y : WideSubcategory P} {f g : X ⟶ Y} (h : f.hom = g.hom) :
+    f = g :=
+  InducedWideCategory.Hom.ext h
+
 @[simp]
 lemma WideSubcategory.id_def (X : WideSubcategory P) : (CategoryStruct.id X).1 = 𝟙 X.obj := rfl
 
@@ -118,6 +134,14 @@ theorem wideSubcategoryInclusion.map {X Y} {f : X ⟶ Y} :
 instance wideSubcategory.faithful : (wideSubcategoryInclusion P).Faithful :=
   inferInstanceAs (wideInducedFunctor WideSubcategory.obj P).Faithful
 
+variable {P} in
+/-- Build an isomorphism in `WideSubcategory P` from an isomorphism in `C`. -/
+@[simps!]
+def isoMk {X Y : WideSubcategory P} (e : X.obj ≅ Y.obj)
+    (h₁ : P e.hom) (h₂ : P e.inv) : X ≅ Y where
+  hom := ⟨e.hom, h₁⟩
+  inv := ⟨e.inv, h₂⟩
+
 end WideSubcategory
 
 end CategoryTheory