Documentation Verification Report

LinearFunctor

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

Statistics

Metric	Count
Definitions `mapLinearMap`	1
Theorems `inverseLinear`, `map_smul`, `coe_mapLinearMap`, `fullSubcategoryInclusionLinear`, `inducedFunctorLinear`, `instLinearComp`, `instLinearId`, `intLinear`, `linear_comp_iff_of_full_of_essSurj`, `linear_iff`, `linear_of_full_essSurj_comp`, `linear_of_iso`, `mapLinearMap_apply`, `map_smul`, `map_units_smul`, `natLinear`, `ratLinear`	17
Total	18

CategoryTheory.Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inverseLinear` 📖	mathematical	—	`CategoryTheory.Functor.Linear` `inverse`	—	`CategoryTheory.Functor.map_injective` `faithful_functor` `fun_inv_map` `CategoryTheory.Linear.smul_comp` `CategoryTheory.Linear.comp_smul` `CategoryTheory.Functor.map_smul`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`mapLinearMap` 📖	CompOp	2 math math: `coe_mapLinearMap`, `mapLinearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mapLinearMap` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `obj` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.Linear.homModule` `LinearMap.instFunLike` `mapLinearMap` `map`	—	—
`fullSubcategoryInclusionLinear` 📖	mathematical	—	`Linear` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Preadditive.fullSubcategory` `CategoryTheory.Linear.fullSubcategory` `CategoryTheory.ObjectProperty.ι`	—	—
`inducedFunctorLinear` 📖	mathematical	—	`Linear` `CategoryTheory.InducedCategory` `CategoryTheory.InducedCategory.instCategory` `CategoryTheory.Preadditive.inducedCategory` `CategoryTheory.Linear.inducedCategory` `CategoryTheory.inducedFunctor`	—	—
`instLinearComp` 📖	mathematical	—	`Linear` `comp`	—	`map_smul`
`instLinearId` 📖	mathematical	—	`Linear` `id`	—	—
`intLinear` 📖	mathematical	—	`Linear` `Int.instSemiring` `CategoryTheory.Linear.preadditiveIntLinear`	—	`AddMonoidHom.map_zsmul`
`linear_comp_iff_of_full_of_essSurj` 📖	mathematical	—	`Linear` `comp`	—	`linear_of_full_essSurj_comp` `instLinearComp`
`linear_iff` 📖	mathematical	—	`Linear` `map` `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.CategoryStruct.id` `obj`	—	`Linear.map_smul` `map_id` `CategoryTheory.Linear.smul_comp` `CategoryTheory.Category.id_comp` `map_comp`
`linear_of_full_essSurj_comp` 📖	mathematical	—	`Linear`	—	`map_surjective` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc` `map_smul` `map_comp` `CategoryTheory.Linear.smul_comp` `CategoryTheory.Linear.comp_smul` `CategoryTheory.whisker_eq` `CategoryTheory.eq_whisker`
`linear_of_iso` 📖	mathematical	—	`Linear`	—	`CategoryTheory.NatIso.naturality_1` `map_smul` `CategoryTheory.Linear.smul_comp` `CategoryTheory.NatTrans.naturality` `CategoryTheory.Linear.comp_smul` `CategoryTheory.Iso.inv_hom_id_app_assoc`
`mapLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `obj` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CategoryTheory.Linear.homModule` `LinearMap.instFunLike` `mapLinearMap` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.toZeroHom` `mapAddHom`	—	—
`map_smul` 📖	mathematical	—	`map` `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` `obj`	—	`Linear.map_smul`
`map_units_smul` 📖	mathematical	—	`map` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Units.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `CategoryTheory.Preadditive.homGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `CategoryTheory.Linear.homModule` `obj`	—	`map_smul`
`natLinear` 📖	mathematical	—	`Linear` `Nat.instSemiring` `CategoryTheory.Linear.preadditiveNatLinear`	—	`AddMonoidHom.map_nsmul`
`ratLinear` 📖	mathematical	—	`Linear` `Rat.semiring`	—	`LinearMap.map_smul`

CategoryTheory.Functor.Linear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_smul` 📖	mathematical	—	`CategoryTheory.Functor.map` `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.Functor.obj`	—	—

---

← Back to Index