Documentation Verification Report

Linear

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

Statistics

Metric	Count
Definitions `Linear`, `Linear`, `MonoidalLinear`	3
Theorems `ofFaithful`, `smul_whiskerRight`, `whiskerLeft_smul`, `monoidalLinearOfFaithful`, `tensorLeft_linear`, `tensorRight_linear`, `tensoringLeft_linear`, `tensoringRight_linear`	8
Total	11

CategoryTheory

Definitions

Name	Category	Theorems
`Linear` 📖	CompData	—
`MonoidalLinear` 📖	CompData	5 math math: `ObjectProperty.instMonoidalLinearFullSubcategory`, `monoidalLinearOfFaithful`, `ModuleCat.instMonoidalLinear`, `MonoidalLinear.ofFaithful`, `Action.instMonoidalLinear`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monoidalLinearOfFaithful` 📖	mathematical	—	`MonoidalLinear`	—	`MonoidalLinear.ofFaithful`
`tensorLeft_linear` 📖	mathematical	—	`Functor.Linear` `MonoidalCategory.tensorLeft`	—	`MonoidalLinear.whiskerLeft_smul`
`tensorRight_linear` 📖	mathematical	—	`Functor.Linear` `MonoidalCategory.tensorRight`	—	`MonoidalLinear.smul_whiskerRight`
`tensoringLeft_linear` 📖	mathematical	—	`Functor.Linear` `Functor.obj` `Functor` `Functor.category` `MonoidalCategory.tensoringLeft`	—	`MonoidalLinear.whiskerLeft_smul`
`tensoringRight_linear` 📖	mathematical	—	`Functor.Linear` `Functor.obj` `Functor` `Functor.category` `MonoidalCategory.tensoringRight`	—	`MonoidalLinear.smul_whiskerRight`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`Linear` 📖	CompData	55 math math: `MoritaEquivalence.linear`, `CategoryTheory.ShortComplex.cyclesFunctor_linear`, `fullSubcategoryInclusionLinear`, `CategoryTheory.Localization.instLinearLocalization'Q'`, `mapHomologicalComplex_linear`, `CochainComplex.instLinearIntFunctorSingleFunctors`, `CategoryTheory.Localization.functor_linear_iff`, `inducedFunctorLinear`, `intLinear`, `CategoryTheory.tensorLeft_linear`, `CategoryTheory.Quotient.linear_functor`, `ratLinear`, `Rep.instLinearModuleCatObjFunctorCoinvariantsTensor`, `CategoryTheory.ShortComplex.opcyclesFunctor_linear`, `CategoryTheory.ShortComplex.rightHomologyFunctor_linear`, `CategoryTheory.tensoringRight_linear`, `ContinuousCohomology.instLinearActionTopModuleCatInvariants`, `DerivedCategory.instLinearCochainComplexIntQ`, `instLinearComp`, `natLinear`, `CategoryTheory.Free.lift_linear`, `CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor`, `Rep.instLinearModuleCatCoinvariantsFunctor`, `mapAction_linear`, `HomotopyCategory.instLinearIntUpShiftFunctor`, `CochainComplex.instLinearIntShiftFunctor`, `CategoryTheory.tensoringLeft_linear`, `HomotopyCategory.instLinearIntUpSingleFunctor`, `ModuleCat.Algebra.instLinearRestrictScalars`, `CategoryTheory.Localization.functor_linear`, `CategoryTheory.tensorRight_linear`, `instLinearId`, `Rep.instLinearModuleCatInvariantsFunctor`, `DerivedCategory.instLinearShiftFunctorInt`, `CategoryTheory.Equivalence.inverseLinear`, `CategoryTheory.instLinearHomotopyCategoryMapHomotopyCategory`, `CategoryTheory.Localization.instLinearLocalizationQ`, `FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG`, `ContinuousCohomology.instLinearActionTopModuleCatI`, `CategoryTheory.ShortComplex.homologyFunctor_linear`, `linear_of_full_essSurj_comp`, `Action.forget_linear`, `linear_of_iso`, `linear_iff`, `Action.functorCategoryEquivalence_linear`, `DerivedCategory.instLinearSingleFunctor`, `DerivedCategory.instLinearHomotopyCategoryIntUpQh`, `ModuleCat.instLinearUliftFunctor`, `Action.res_linear`, `Action.forget₂_linear`, `instLinearDerivedCategoryMapDerivedCategory`, `ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear`, `CategoryTheory.ShortComplex.leftHomologyFunctor_linear`, `HomotopyCategory.instLinearHomologicalComplexQuotient`, `linear_comp_iff_of_full_of_essSurj`

CategoryTheory.MonoidalLinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFaithful` 📖	mathematical	—	`CategoryTheory.MonoidalLinear`	—	`CategoryTheory.Functor.map_injective` `CategoryTheory.Functor.Monoidal.map_whiskerLeft` `CategoryTheory.Functor.map_smul` `whiskerLeft_smul` `CategoryTheory.Linear.smul_comp` `CategoryTheory.Functor.LaxMonoidal.μ_natural_right` `CategoryTheory.Linear.comp_smul` `CategoryTheory.Functor.Monoidal.δ_μ_assoc` `CategoryTheory.Functor.Monoidal.map_whiskerRight` `smul_whiskerRight` `CategoryTheory.Functor.LaxMonoidal.μ_natural_left`
`smul_whiskerRight` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Linear.homModule` `CategoryTheory.MonoidalCategoryStruct.tensorObj`	—	—
`whiskerLeft_smul` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Linear.homModule` `CategoryTheory.MonoidalCategoryStruct.tensorObj`	—	—

---

← Back to Index