Documentation Verification Report

Transport

📁 Source: Mathlib/CategoryTheory/Monoidal/Transport.lean

Statistics

Metric	Count
Definitions `InducingFunctorData`, `εIso`, `μIso`, `Transported`, `instMonoidalCategory`, `instMonoidalCategoryStruct`, `equivalenceTransported`, `fromInducedCoreMonoidal`, `fromInducedMonoidal`, `induced`, `instCategoryTransported`, `instInhabitedTransported`, `instMonoidalTransportedFunctorEquivalenceTransported`, `instMonoidalTransportedFunctorSymmEquivalenceTransported`, `instMonoidalTransportedInverseEquivalenceTransported`, `instMonoidalTransportedInverseSymmEquivalenceTransported`, `transport`, `transportStruct`	18
Theorems `associator_eq`, `leftUnitor_eq`, `rightUnitor_eq`, `tensorHom_eq`, `whiskerLeft_eq`, `whiskerRight_eq`, `instIsMonoidalTransportedCounitEquivalenceTransported`, `instIsMonoidalTransportedSymmEquivalenceTransported`, `instIsMonoidalUnitTransportedEquivalenceTransported`, `transportStruct_associator`, `transportStruct_leftUnitor`, `transportStruct_rightUnitor`, `transportStruct_tensorHom`, `transportStruct_tensorObj`, `transportStruct_tensorUnit`, `transportStruct_whiskerLeft`, `transportStruct_whiskerRight`	17
Total	35

CategoryTheory.Monoidal

Definitions

Name	Category	Theorems
`InducingFunctorData` 📖	CompData	—
`Transported` 📖	CompOp	3 math math: `instIsMonoidalUnitTransportedEquivalenceTransported`, `instIsMonoidalTransportedCounitEquivalenceTransported`, `instIsMonoidalTransportedSymmEquivalenceTransported`
`equivalenceTransported` 📖	CompOp	3 math math: `instIsMonoidalUnitTransportedEquivalenceTransported`, `instIsMonoidalTransportedCounitEquivalenceTransported`, `instIsMonoidalTransportedSymmEquivalenceTransported`
`fromInducedCoreMonoidal` 📖	CompOp	—
`fromInducedMonoidal` 📖	CompOp	—
`induced` 📖	CompOp	—
`instCategoryTransported` 📖	CompOp	3 math math: `instIsMonoidalUnitTransportedEquivalenceTransported`, `instIsMonoidalTransportedCounitEquivalenceTransported`, `instIsMonoidalTransportedSymmEquivalenceTransported`
`instInhabitedTransported` 📖	CompOp	—
`instMonoidalTransportedFunctorEquivalenceTransported` 📖	CompOp	2 math math: `instIsMonoidalUnitTransportedEquivalenceTransported`, `instIsMonoidalTransportedCounitEquivalenceTransported`
`instMonoidalTransportedFunctorSymmEquivalenceTransported` 📖	CompOp	1 math math: `instIsMonoidalTransportedSymmEquivalenceTransported`
`instMonoidalTransportedInverseEquivalenceTransported` 📖	CompOp	2 math math: `instIsMonoidalUnitTransportedEquivalenceTransported`, `instIsMonoidalTransportedCounitEquivalenceTransported`
`instMonoidalTransportedInverseSymmEquivalenceTransported` 📖	CompOp	1 math math: `instIsMonoidalTransportedSymmEquivalenceTransported`
`transport` 📖	CompOp	—
`transportStruct` 📖	CompOp	8 math math: `transportStruct_associator`, `transportStruct_tensorHom`, `transportStruct_tensorObj`, `transportStruct_tensorUnit`, `transportStruct_whiskerRight`, `transportStruct_leftUnitor`, `transportStruct_rightUnitor`, `transportStruct_whiskerLeft`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsMonoidalTransportedCounitEquivalenceTransported` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `Transported` `instCategoryTransported` `Transported.instMonoidalCategory` `CategoryTheory.Functor.comp` `CategoryTheory.Equivalence.inverse` `equivalenceTransported` `CategoryTheory.Equivalence.functor` `CategoryTheory.Functor.id` `CategoryTheory.Equivalence.counit` `CategoryTheory.Functor.LaxMonoidal.comp` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `instMonoidalTransportedInverseEquivalenceTransported` `instMonoidalTransportedFunctorEquivalenceTransported` `CategoryTheory.Functor.LaxMonoidal.id`	—	`CategoryTheory.Iso.instIsMonoidalInvFunctor` `CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit` `instIsMonoidalTransportedSymmEquivalenceTransported`
`instIsMonoidalTransportedSymmEquivalenceTransported` 📖	mathematical	—	`CategoryTheory.Equivalence.IsMonoidal` `Transported` `instCategoryTransported` `Transported.instMonoidalCategory` `CategoryTheory.Equivalence.symm` `equivalenceTransported` `instMonoidalTransportedFunctorSymmEquivalenceTransported` `instMonoidalTransportedInverseSymmEquivalenceTransported`	—	`CategoryTheory.Adjunction.instIsMonoidal`
`instIsMonoidalUnitTransportedEquivalenceTransported` 📖	mathematical	—	`CategoryTheory.NatTrans.IsMonoidal` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `Transported` `instCategoryTransported` `CategoryTheory.Equivalence.functor` `equivalenceTransported` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Equivalence.unit` `CategoryTheory.Functor.LaxMonoidal.id` `CategoryTheory.Functor.LaxMonoidal.comp` `Transported.instMonoidalCategory` `CategoryTheory.Functor.Monoidal.toLaxMonoidal` `instMonoidalTransportedFunctorEquivalenceTransported` `instMonoidalTransportedInverseEquivalenceTransported`	—	`CategoryTheory.Iso.instIsMonoidalInvFunctor` `CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit` `instIsMonoidalTransportedSymmEquivalenceTransported`
`transportStruct_associator` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.associator` `transportStruct` `CategoryTheory.Functor.mapIso` `CategoryTheory.Equivalence.functor` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Iso.trans` `CategoryTheory.Functor.id` `CategoryTheory.MonoidalCategory.whiskerRightIso` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.symm` `CategoryTheory.Iso.app` `CategoryTheory.Equivalence.unitIso` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	—	—
`transportStruct_leftUnitor` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.leftUnitor` `transportStruct` `CategoryTheory.Iso.trans` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.functor` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Equivalence.inverse` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor.mapIso` `CategoryTheory.Functor.id` `CategoryTheory.MonoidalCategory.whiskerRightIso` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.symm` `CategoryTheory.Iso.app` `CategoryTheory.Equivalence.unitIso` `CategoryTheory.Equivalence.counitIso`	—	—
`transportStruct_rightUnitor` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.rightUnitor` `transportStruct` `CategoryTheory.Iso.trans` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.functor` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Equivalence.inverse` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor.mapIso` `CategoryTheory.Functor.id` `CategoryTheory.MonoidalCategory.whiskerLeftIso` `CategoryTheory.Iso.symm` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.app` `CategoryTheory.Equivalence.unitIso` `CategoryTheory.Equivalence.counitIso`	—	—
`transportStruct_tensorHom` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorHom` `transportStruct` `CategoryTheory.Functor.map` `CategoryTheory.Equivalence.functor` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.inverse`	—	—
`transportStruct_tensorObj` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `transportStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.functor` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Equivalence.inverse`	—	—
`transportStruct_tensorUnit` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorUnit` `transportStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.functor` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`transportStruct_whiskerLeft` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `transportStruct` `CategoryTheory.Functor.map` `CategoryTheory.Equivalence.functor` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.inverse`	—	—
`transportStruct_whiskerRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerRight` `transportStruct` `CategoryTheory.Functor.map` `CategoryTheory.Equivalence.functor` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Equivalence.inverse`	—	—

CategoryTheory.Monoidal.InducingFunctorData

Definitions

Name	Category	Theorems
`εIso` 📖	CompOp	5 math math: `rightUnitor_eq`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `CoalgCat.MonoidalCategory.inducingFunctorData_εIso`, `leftUnitor_eq`, `BialgCat.MonoidalCategory.inducingFunctorData_εIso`
`μIso` 📖	CompOp	9 math math: `rightUnitor_eq`, `associator_eq`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`, `CoalgCat.MonoidalCategory.inducingFunctorData_μIso`, `tensorHom_eq`, `whiskerRight_eq`, `BialgCat.MonoidalCategory.inducingFunctorData_μIso`, `whiskerLeft_eq`, `leftUnitor_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_eq` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.symm` `μIso` `CategoryTheory.MonoidalCategory.tensorIso` `CategoryTheory.Iso.refl`	—	—
`leftUnitor_eq` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.symm` `μIso` `CategoryTheory.MonoidalCategory.tensorIso` `εIso` `CategoryTheory.Iso.refl`	—	—
`rightUnitor_eq` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.symm` `μIso` `CategoryTheory.MonoidalCategory.tensorIso` `CategoryTheory.Iso.refl` `εIso`	—	—
`tensorHom_eq` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `μIso` `CategoryTheory.Iso.hom`	—	—
`whiskerLeft_eq` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `μIso` `CategoryTheory.Iso.hom`	—	—
`whiskerRight_eq` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `μIso` `CategoryTheory.Iso.hom`	—	—

CategoryTheory.Monoidal.Transported

Definitions

Name	Category	Theorems
`instMonoidalCategory` 📖	CompOp	3 math math: `CategoryTheory.Monoidal.instIsMonoidalUnitTransportedEquivalenceTransported`, `CategoryTheory.Monoidal.instIsMonoidalTransportedCounitEquivalenceTransported`, `CategoryTheory.Monoidal.instIsMonoidalTransportedSymmEquivalenceTransported`
`instMonoidalCategoryStruct` 📖	CompOp	—

---

← Back to Index