Documentation Verification Report

SFinKer

📁 Source: Mathlib/Probability/Kernel/Category/SFinKer.lean

Statistics

Metric	Count
Definitions `SFinKer`, `hom`, `carrier`, `instLargeCategory`, `str`, `instCoeSortSFinKerType`, `instComonObjSFinKer`, `instCopyDiscardCategorySFinKer`, `instMonoidalCategorySFinKer`, `instSymmetricCategorySFinKer`	10
Theorems `ext`, `ext_iff`, `property`, `comp_hom`, `hom_ext`, `hom_ext_iff`, `id_hom`, `instIsSFiniteKernelCarrierHom`, `associator_hom_hom`, `associator_inv_hom`, `braiding_hom_hom`, `braiding_inv_hom`, `comul_hom`, `counit_hom`, `leftUnitor_hom_hom`, `leftUnitor_inv_hom`, `rightUnitor_hom_hom`, `rightUnitor_inv_hom`, `tensorHom_def`, `tensorObj_carrier`, `tensorObj_str`, `tensorUnit_carrier`, `tensorUnit_str`, `whiskerLeft_hom`, `whiskerRight_hom`	25
Total	35

SFinKer

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	20 math math: `associator_inv_hom`, `leftUnitor_hom_hom`, `instIsSFiniteKernelCarrierHom`, `Hom.property`, `associator_hom_hom`, `tensorObj_str`, `leftUnitor_inv_hom`, `comul_hom`, `rightUnitor_inv_hom`, `comp_hom`, `instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory`, `tensorUnit_carrier`, `id_hom`, `tensorObj_carrier`, `counit_hom`, `whiskerRight_hom`, `rightUnitor_hom_hom`, `braiding_hom_hom`, `braiding_inv_hom`, `whiskerLeft_hom`
`instLargeCategory` 📖	CompOp	22 math math: `associator_inv_hom`, `instIsStableUnderComonoidSFinKerStochHom`, `leftUnitor_hom_hom`, `tensorUnit_str`, `associator_hom_hom`, `tensorObj_str`, `instIsStableUnderBraidingSFinKerStochHom`, `leftUnitor_inv_hom`, `comul_hom`, `tensorHom_def`, `rightUnitor_inv_hom`, `comp_hom`, `instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory`, `tensorUnit_carrier`, `id_hom`, `tensorObj_carrier`, `counit_hom`, `whiskerRight_hom`, `rightUnitor_hom_hom`, `braiding_hom_hom`, `braiding_inv_hom`, `whiskerLeft_hom`
`str` 📖	CompOp	19 math math: `associator_inv_hom`, `leftUnitor_hom_hom`, `tensorUnit_str`, `instIsSFiniteKernelCarrierHom`, `Hom.property`, `associator_hom_hom`, `tensorObj_str`, `leftUnitor_inv_hom`, `comul_hom`, `rightUnitor_inv_hom`, `comp_hom`, `instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory`, `id_hom`, `counit_hom`, `whiskerRight_hom`, `rightUnitor_hom_hom`, `braiding_hom_hom`, `braiding_inv_hom`, `whiskerLeft_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `SFinKer` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `ProbabilityTheory.Kernel.comp` `carrier` `str`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`id_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `SFinKer` `CategoryTheory.Category.toCategoryStruct` `instLargeCategory` `ProbabilityTheory.Kernel.id` `carrier` `str`	—	—
`instIsSFiniteKernelCarrierHom` 📖	mathematical	—	`ProbabilityTheory.IsSFiniteKernel` `carrier` `str` `Hom.hom`	—	`Hom.property`

SFinKer.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	19 math math: `associator_inv_hom`, `leftUnitor_hom_hom`, `SFinKer.instIsSFiniteKernelCarrierHom`, `property`, `associator_hom_hom`, `leftUnitor_inv_hom`, `comul_hom`, `rightUnitor_inv_hom`, `SFinKer.comp_hom`, `instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory`, `ext_iff`, `SFinKer.id_hom`, `counit_hom`, `whiskerRight_hom`, `rightUnitor_hom_hom`, `braiding_hom_hom`, `braiding_inv_hom`, `SFinKer.hom_ext_iff`, `whiskerLeft_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom`	—	—	—
`ext_iff` 📖	mathematical	—	`hom`	—	`ext`
`property` 📖	mathematical	—	`ProbabilityTheory.IsSFiniteKernel` `SFinKer.carrier` `SFinKer.str` `hom`	—	—

(root)

Definitions

Name	Category	Theorems
`SFinKer` 📖	CompData	22 math math: `associator_inv_hom`, `instIsStableUnderComonoidSFinKerStochHom`, `leftUnitor_hom_hom`, `tensorUnit_str`, `associator_hom_hom`, `tensorObj_str`, `instIsStableUnderBraidingSFinKerStochHom`, `leftUnitor_inv_hom`, `comul_hom`, `tensorHom_def`, `rightUnitor_inv_hom`, `SFinKer.comp_hom`, `instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory`, `tensorUnit_carrier`, `SFinKer.id_hom`, `tensorObj_carrier`, `counit_hom`, `whiskerRight_hom`, `rightUnitor_hom_hom`, `braiding_hom_hom`, `braiding_inv_hom`, `whiskerLeft_hom`
`instCoeSortSFinKerType` 📖	CompOp	—
`instComonObjSFinKer` 📖	CompOp	3 math math: `instIsStableUnderComonoidSFinKerStochHom`, `comul_hom`, `counit_hom`
`instCopyDiscardCategorySFinKer` 📖	CompOp	—
`instMonoidalCategorySFinKer` 📖	CompOp	19 math math: `associator_inv_hom`, `instIsStableUnderComonoidSFinKerStochHom`, `leftUnitor_hom_hom`, `tensorUnit_str`, `associator_hom_hom`, `tensorObj_str`, `instIsStableUnderBraidingSFinKerStochHom`, `leftUnitor_inv_hom`, `comul_hom`, `tensorHom_def`, `rightUnitor_inv_hom`, `tensorUnit_carrier`, `tensorObj_carrier`, `counit_hom`, `whiskerRight_hom`, `rightUnitor_hom_hom`, `braiding_hom_hom`, `braiding_inv_hom`, `whiskerLeft_hom`
`instSymmetricCategorySFinKer` 📖	CompOp	3 math math: `instIsStableUnderBraidingSFinKerStochHom`, `braiding_hom_hom`, `braiding_inv_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_hom_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `SFinKer.of` `SFinKer.carrier` `Prod.instMeasurableSpace` `SFinKer.str` `CategoryTheory.Iso.hom` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `ProbabilityTheory.Kernel.map` `ProbabilityTheory.Kernel.id`	—	—
`associator_inv_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `SFinKer.of` `SFinKer.carrier` `Prod.instMeasurableSpace` `SFinKer.str` `CategoryTheory.Iso.inv` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `ProbabilityTheory.Kernel.map` `ProbabilityTheory.Kernel.id`	—	—
`braiding_hom_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `CategoryTheory.Iso.hom` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.SymmetricCategory.toBraidedCategory` `instSymmetricCategorySFinKer` `ProbabilityTheory.Kernel.swap` `SFinKer.carrier` `SFinKer.str`	—	—
`braiding_inv_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `CategoryTheory.Iso.inv` `CategoryTheory.BraidedCategory.braiding` `CategoryTheory.SymmetricCategory.toBraidedCategory` `instSymmetricCategorySFinKer` `ProbabilityTheory.Kernel.swap` `SFinKer.carrier` `SFinKer.str`	—	—
`comul_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `CategoryTheory.ComonObj.comul` `instComonObjSFinKer` `ProbabilityTheory.Kernel.copy` `SFinKer.carrier` `SFinKer.str`	—	—
`counit_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `CategoryTheory.ComonObj.counit` `instComonObjSFinKer` `ProbabilityTheory.Kernel.discard` `SFinKer.carrier` `SFinKer.str`	—	—
`leftUnitor_hom_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `SFinKer.of` `SFinKer.carrier` `PUnit.instMeasurableSpace` `Prod.instMeasurableSpace` `SFinKer.str` `CategoryTheory.Iso.hom` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `ProbabilityTheory.Kernel.map` `ProbabilityTheory.Kernel.id`	—	—
`leftUnitor_inv_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `SFinKer.of` `SFinKer.carrier` `PUnit.instMeasurableSpace` `Prod.instMeasurableSpace` `SFinKer.str` `CategoryTheory.Iso.inv` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `ProbabilityTheory.Kernel.map` `ProbabilityTheory.Kernel.id`	—	—
`rightUnitor_hom_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `SFinKer.of` `SFinKer.carrier` `PUnit.instMeasurableSpace` `Prod.instMeasurableSpace` `SFinKer.str` `CategoryTheory.Iso.hom` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `ProbabilityTheory.Kernel.map` `ProbabilityTheory.Kernel.id`	—	—
`rightUnitor_inv_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `SFinKer.of` `SFinKer.carrier` `PUnit.instMeasurableSpace` `Prod.instMeasurableSpace` `SFinKer.str` `CategoryTheory.Iso.inv` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `ProbabilityTheory.Kernel.map` `ProbabilityTheory.Kernel.id`	—	—
`tensorHom_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorHom` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`tensorObj_carrier` 📖	mathematical	—	`SFinKer.carrier` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer`	—	—
`tensorObj_str` 📖	mathematical	—	`SFinKer.str` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `Prod.instMeasurableSpace` `SFinKer.carrier`	—	—
`tensorUnit_carrier` 📖	mathematical	—	`SFinKer.carrier` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer`	—	—
`tensorUnit_str` 📖	mathematical	—	`SFinKer.str` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `PUnit.instMeasurableSpace`	—	—
`whiskerLeft_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `SFinKer.of` `SFinKer.carrier` `Prod.instMeasurableSpace` `SFinKer.str` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `ProbabilityTheory.Kernel.parallelComp` `ProbabilityTheory.Kernel.id`	—	—
`whiskerRight_hom` 📖	mathematical	—	`SFinKer.Hom.hom` `SFinKer.of` `SFinKer.carrier` `Prod.instMeasurableSpace` `SFinKer.str` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `SFinKer` `SFinKer.instLargeCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategorySFinKer` `ProbabilityTheory.Kernel.parallelComp` `ProbabilityTheory.Kernel.id`	—	—

---

← Back to Index