Subcategory

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

Statistics

Metric	Count
Definitions ContainsUnit, IsMonoidal, IsMonoidalClosed, TensorLE, fullBraidedSubcategory, fullMonoidalClosedSubcategory, fullMonoidalSubcategory, fullSymmetricSubcategory, instBraidedFullSubcategoryι, instBraidedFullSubcategoryιOfLE, instMonoidalCategoryStructFullSubcategory, instMonoidalFullSubcategoryιOfLE, monoidalι	13
Theorems prop_unit, toContainsUnit, toTensorLE, prop_ihom, prop_tensor, associator_def, ihom_map, ihom_map_hom, ihom_obj, instMonoidalLinearFullSubcategory, instMonoidalPreadditiveFullSubcategory, leftUnitor_def, prop_ihom, prop_tensor, prop_unit, rightUnitor_def, tensorHom_def, tensorObj_obj, tensorUnit_obj, whiskerLeft_def, whiskerRight_def, ιOfLE_δ, ιOfLE_ε, ιOfLE_η, ιOfLE_μ, ι_δ, ι_ε, ι_η, ι_μ	29
Total	42

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
ContainsUnit 📖	CompData	1 math math: IsMonoidal.toContainsUnit
IsMonoidal 📖	CompData	2 math math: CategoryTheory.Sheaf.instIsMonoidalFunctorOppositeIsSheaf, FGModuleCat.instIsMonoidalModuleCatIsFG
IsMonoidalClosed 📖	CompData	1 math math: FGModuleCat.instIsMonoidalClosedModuleCatIsFG
TensorLE 📖	CompData	1 math math: IsMonoidal.toTensorLE
fullBraidedSubcategory 📖	CompOp	—
fullMonoidalClosedSubcategory 📖	CompOp	4 math math: FGModuleCat.ihom_obj, ihom_obj, ihom_map, ihom_map_hom
fullMonoidalSubcategory 📖	CompOp	27 math math: TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular, FDRep.char_tensor, TannakaDuality.FiniteGroup.forget_obj, CategoryTheory.sheafToPresheaf_μ, ι_η, ι_ε, CategoryTheory.sheafToPresheaf_δ, instMonoidalLinearFullSubcategory, TannakaDuality.FiniteGroup.forget_map, FGModuleCat.ihom_obj, ι_δ, ihom_obj, ihom_map, ι_μ, CategoryTheory.sheafToPresheaf_η, instMonoidalPreadditiveFullSubcategory, CategoryTheory.sheafToPresheaf_ε, ιOfLE_ε, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, ιOfLE_η, ιOfLE_μ, TannakaDuality.FiniteGroup.equivHom_surjective, TannakaDuality.FiniteGroup.equivHom_injective, FDRep.dualTensorIsoLinHom_hom_hom, ιOfLE_δ, ihom_map_hom, TannakaDuality.FiniteGroup.equivHom_apply
fullSymmetricSubcategory 📖	CompOp	—
instBraidedFullSubcategoryι 📖	CompOp	—
instBraidedFullSubcategoryιOfLE 📖	CompOp	—
instMonoidalCategoryStructFullSubcategory 📖	CompOp	17 math math: rightUnitor_def, tensorUnit_obj, tensorHom_def, FGModuleCat.FGModuleCatEvaluation_apply, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom, FGModuleCat.FGModuleCatCoevaluation_apply_one, tensorObj_obj, whiskerLeft_def, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val, whiskerRight_def, leftUnitor_def, FGModuleCat.tensorObj_obj, FGModuleCat.tensorUnit_obj, associator_def, FGModuleCat.FGModuleCatEvaluation_apply', CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val, CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom
instMonoidalFullSubcategoryιOfLE 📖	CompOp	4 math math: ιOfLE_ε, ιOfLE_η, ιOfLE_μ, ιOfLE_δ
monoidalι 📖	CompOp	8 math math: CategoryTheory.sheafToPresheaf_μ, ι_η, ι_ε, CategoryTheory.sheafToPresheaf_δ, ι_δ, ι_μ, CategoryTheory.sheafToPresheaf_η, CategoryTheory.sheafToPresheaf_ε

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_def 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.associator FullSubcategory FullSubcategory.category instMonoidalCategoryStructFullSubcategory isoMk CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct FullSubcategory.obj	—	—
ihom_map 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom FullSubcategory FullSubcategory.obj CategoryTheory.Functor.obj FullSubcategory.category CategoryTheory.ihom fullMonoidalSubcategory CategoryTheory.MonoidalClosed.closed fullMonoidalClosedSubcategory CategoryTheory.Functor.map	—	ihom_map_hom
ihom_map_hom 📖	mathematical	—	CategoryTheory.InducedCategory.Hom.hom FullSubcategory FullSubcategory.obj CategoryTheory.Functor.obj FullSubcategory.category CategoryTheory.ihom fullMonoidalSubcategory CategoryTheory.MonoidalClosed.closed fullMonoidalClosedSubcategory CategoryTheory.Functor.map	—	—
ihom_obj 📖	mathematical	—	FullSubcategory.obj CategoryTheory.Functor.obj FullSubcategory FullSubcategory.category CategoryTheory.ihom fullMonoidalSubcategory CategoryTheory.MonoidalClosed.closed fullMonoidalClosedSubcategory	—	—
instMonoidalLinearFullSubcategory 📖	mathematical	—	CategoryTheory.MonoidalLinear Ring.toSemiring FullSubcategory FullSubcategory.category CategoryTheory.Preadditive.fullSubcategory CategoryTheory.Linear.fullSubcategory fullMonoidalSubcategory instMonoidalPreadditiveFullSubcategory	—	CategoryTheory.MonoidalLinear.ofFaithful instMonoidalPreadditiveFullSubcategory faithful_ι CategoryTheory.Functor.fullSubcategoryInclusionLinear
instMonoidalPreadditiveFullSubcategory 📖	mathematical	—	CategoryTheory.MonoidalPreadditive FullSubcategory FullSubcategory.category CategoryTheory.Preadditive.fullSubcategory fullMonoidalSubcategory	—	CategoryTheory.monoidalPreadditive_of_faithful faithful_ι CategoryTheory.Functor.fullSubcategoryInclusion_additive
leftUnitor_def 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.leftUnitor FullSubcategory FullSubcategory.category instMonoidalCategoryStructFullSubcategory isoMk CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit	—	—
prop_ihom 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed	—	IsMonoidalClosed.prop_ihom
prop_tensor 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	TensorLE.prop_tensor
prop_unit 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	ContainsUnit.prop_unit
rightUnitor_def 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.rightUnitor FullSubcategory FullSubcategory.category instMonoidalCategoryStructFullSubcategory isoMk CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit	—	—
tensorHom_def 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom FullSubcategory FullSubcategory.category instMonoidalCategoryStructFullSubcategory homMk CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom	—	—
tensorObj_obj 📖	mathematical	—	FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorObj FullSubcategory FullSubcategory.category instMonoidalCategoryStructFullSubcategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorUnit_obj 📖	mathematical	—	FullSubcategory.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit FullSubcategory FullSubcategory.category instMonoidalCategoryStructFullSubcategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
whiskerLeft_def 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerLeft FullSubcategory FullSubcategory.category instMonoidalCategoryStructFullSubcategory homMk CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom	—	—
whiskerRight_def 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight FullSubcategory FullSubcategory.category instMonoidalCategoryStructFullSubcategory homMk CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct FullSubcategory.obj CategoryTheory.InducedCategory.Hom.hom	—	—
ιOfLE_δ 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.Functor.OplaxMonoidal.δ FullSubcategory FullSubcategory.category fullMonoidalSubcategory ιOfLE CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalFullSubcategoryιOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
ιOfLE_ε 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.Functor.LaxMonoidal.ε FullSubcategory FullSubcategory.category fullMonoidalSubcategory ιOfLE CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalFullSubcategoryιOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
ιOfLE_η 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.Functor.OplaxMonoidal.η FullSubcategory FullSubcategory.category fullMonoidalSubcategory ιOfLE CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalFullSubcategoryιOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
ιOfLE_μ 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.Functor.LaxMonoidal.μ FullSubcategory FullSubcategory.category fullMonoidalSubcategory ιOfLE CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalFullSubcategoryιOfLE CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
ι_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ FullSubcategory FullSubcategory.category fullMonoidalSubcategory ι CategoryTheory.Functor.Monoidal.toOplaxMonoidal monoidalι CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
ι_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε FullSubcategory FullSubcategory.category fullMonoidalSubcategory ι CategoryTheory.Functor.Monoidal.toLaxMonoidal monoidalι CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
ι_η 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε FullSubcategory FullSubcategory.category fullMonoidalSubcategory ι CategoryTheory.Functor.Monoidal.toLaxMonoidal monoidalι CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
ι_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ FullSubcategory FullSubcategory.category fullMonoidalSubcategory ι CategoryTheory.Functor.Monoidal.toLaxMonoidal monoidalι CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—

CategoryTheory.ObjectProperty.ContainsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prop_unit 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—

CategoryTheory.ObjectProperty.IsMonoidal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContainsUnit 📖	mathematical	—	CategoryTheory.ObjectProperty.ContainsUnit	—	—
toTensorLE 📖	mathematical	—	CategoryTheory.ObjectProperty.TensorLE	—	—

CategoryTheory.ObjectProperty.IsMonoidalClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prop_ihom 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed	—	—

CategoryTheory.ObjectProperty.TensorLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prop_tensor 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—

---

← Back to Index