Basic

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

Statistics

Metric	Count
Definitions homLinearEquiv, comp, fullSubcategory, homCongr, homModule, inducedCategory, instAlgebraEnd, instModuleEnd, leftComp, preadditiveIntLinear, preadditiveNatLinear, rightComp	12
Theorems homLinearEquiv_apply, homLinearEquiv_symm_apply_hom, comp_apply, comp_smul, comp_units_smul, homCongr_apply, homCongr_symm_apply, instEpiHSMulHomOfInvertible, instMonoHSMulHomOfInvertible, leftComp_apply, rightComp_apply, smul_comp, units_smul_comp	13
Total	25

CategoryTheory.InducedCategory

Definitions

Name	Category	Theorems
homLinearEquiv 📖	CompOp	2 math math: homLinearEquiv_apply, homLinearEquiv_symm_apply_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.InducedCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Preadditive.inducedCategory CategoryTheory.Linear.homModule CategoryTheory.Linear.inducedCategory EquivLike.toFunLike LinearEquiv.instEquivLike homLinearEquiv Hom.hom	—	RingHomInvPair.ids
homLinearEquiv_symm_apply_hom 📖	mathematical	—	Hom.hom DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.InducedCategory instCategory AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Preadditive.inducedCategory CategoryTheory.Linear.homModule CategoryTheory.Linear.inducedCategory EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm homLinearEquiv	—	RingHomInvPair.ids

CategoryTheory.Linear

Definitions

Name	Category	Theorems
comp 📖	CompOp	1 math math: comp_apply
fullSubcategory 📖	CompOp	8 math math: CategoryTheory.Functor.fullSubcategoryInclusionLinear, FDRep.instFiniteDimensionalHom, FGModuleCat.instFiniteHom, CategoryTheory.ObjectProperty.instMonoidalLinearFullSubcategory, FDRep.simple_iff_end_is_rank_one, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, FDRep.scalar_product_char_eq_finrank_equivariant, FDRep.finrank_hom_simple_simple
homCongr 📖	CompOp	2 math math: homCongr_apply, homCongr_symm_apply
homModule 📖	CompOp	91 math math: CategoryTheory.ShortComplex.opcyclesMap_smul, CategoryTheory.ShortComplex.homologyMap_smul, CategoryTheory.linearCoyoneda_map_app, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, instMonoHSMulHomOfInvertible, CategoryTheory.Functor.coe_mapLinearMap, CategoryTheory.finrank_hom_simple_simple_le_one, CategoryTheory.ShortComplex.Homotopy.smul_h₁, CategoryTheory.InducedCategory.homLinearEquiv_apply, CategoryTheory.linearYoneda_obj_map, comp_apply, CategoryTheory.finrank_hom_simple_simple_eq_one_iff, CategoryTheory.Quotient.Linear.smul_eq, CategoryTheory.Abelian.Ext.smul_hom, CategoryTheory.ShortComplex.Homotopy.smul_h₂, units_smul_comp, leftComp_apply, CategoryTheory.Functor.Linear.map_smul, CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φH, Action.smul_hom, CategoryTheory.Pretriangulated.Triangle.smul_hom₂, FDRep.instFiniteDimensionalHom, CategoryTheory.Abelian.Ext.mk₀_smul, CategoryTheory.ShortComplex.Homotopy.smul_h₀, CategoryTheory.ShortComplex.Homotopy.smul_h₃, CategoryTheory.ShortComplex.cyclesMap_smul, FGModuleCat.instFiniteHom, CategoryTheory.finrank_endomorphism_eq_one, CategoryTheory.linearYoneda_map_app, HomologicalComplex.units_smul_f_apply, CategoryTheory.Functor.map_smul, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, comp_units_smul, CategoryTheory.finrank_hom_simple_simple_eq_zero_iff, CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, CategoryTheory.ShortComplex.smul_τ₃, CategoryTheory.endomorphism_simple_eq_smul_id, CategoryTheory.ShiftedHom.comp_smul, homCongr_apply, CategoryTheory.ShortComplex.cyclesMap'_smul, comp_smul, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH, CategoryTheory.finrank_hom_simple_simple, CochainComplex.HomComplex.Cochain.units_smul_v, HomologicalComplex.smul_f_apply, CategoryTheory.Functor.map_units_smul, CategoryTheory.linearCoyoneda_obj_map, FDRep.simple_iff_end_is_rank_one, CochainComplex.HomComplex.Cochain.smul_v, CategoryTheory.ShortComplex.homologyMap'_smul, CategoryTheory.NatTrans.appLinearMap_apply, CategoryTheory.ShiftedHom.map_smul, CategoryTheory.Free.lift_map_single, CategoryTheory.Abelian.Ext.smul_eq_comp_mk₀, homCongr_symm_apply, CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φK, ChainComplex.linearYonedaObj_d, Homotopy.smul_hom, CategoryTheory.MonoidalLinear.smul_whiskerRight, CategoryTheory.MonoidalLinear.whiskerLeft_smul, CategoryTheory.Pretriangulated.Triangle.smul_hom₃, CategoryTheory.linearYoneda_obj_obj_isModule, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φQ, CategoryTheory.NatTrans.app_smul, CategoryTheory.Free.lift_map, CategoryTheory.Abelian.Ext.mk₀_linearEquiv₀_apply, instEpiHSMulHomOfInvertible, ModuleCat.ofHom₂_compr₂, CategoryTheory.finrank_endomorphism_simple_eq_one, CategoryTheory.ShortComplex.smul_τ₁, CategoryTheory.ShortComplex.smul_τ₂, CategoryTheory.Abelian.Ext.linearEquiv₀_symm_apply, CategoryTheory.Functor.linear_iff, CategoryTheory.ShortComplex.rightHomologyMap'_smul, CategoryTheory.ShortComplex.rightHomologyMap_smul, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, toCatCenter_apply_app, FDRep.scalar_product_char_eq_finrank_equivariant, CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom, CategoryTheory.ShiftedHom.smul_comp, CategoryTheory.linearCoyoneda_obj_obj_isModule, rightComp_apply, CategoryTheory.ShiftedHom.mk₀_smul, smul_comp, CategoryTheory.Pretriangulated.Triangle.smul_hom₁, CategoryTheory.ShortComplex.leftHomologyMap_smul, CategoryTheory.ShortComplex.opcyclesMap'_smul, CategoryTheory.ShortComplex.leftHomologyMap'_smul, CategoryTheory.Functor.mapLinearMap_apply, FDRep.finrank_hom_simple_simple
inducedCategory 📖	CompOp	3 math math: CategoryTheory.InducedCategory.homLinearEquiv_apply, CategoryTheory.Functor.inducedFunctorLinear, CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom
instAlgebraEnd 📖	CompOp	—
instModuleEnd 📖	CompOp	2 math math: CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply
leftComp 📖	CompOp	6 math math: CategoryTheory.linearCoyoneda_map_app, CategoryTheory.linearYoneda_obj_map, comp_apply, leftComp_apply, CategoryTheory.linearYoneda_map_app, ChainComplex.linearYonedaObj_d
preadditiveIntLinear 📖	CompOp	1 math math: CategoryTheory.Functor.intLinear
preadditiveNatLinear 📖	CompOp	1 math math: CategoryTheory.Functor.natLinear
rightComp 📖	CompOp	5 math math: CategoryTheory.linearCoyoneda_map_app, CategoryTheory.linearYoneda_map_app, CategoryTheory.linearCoyoneda_obj_map, ModuleCat.ofHom₂_compr₂, rightComp_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup homModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike comp leftComp	—	smulCommClass_self
comp_smul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver 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 homModule	—	—
comp_units_smul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Quiver.Hom CategoryTheory.CategoryStruct.toQuiver 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 homModule	—	comp_smul
homCongr_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup homModule EquivLike.toFunLike LinearEquiv.instEquivLike homCongr CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	RingHomInvPair.ids
homCongr_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup homModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm homCongr CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom CategoryTheory.Iso.inv	—	RingHomInvPair.ids
instEpiHSMulHomOfInvertible 📖	mathematical	—	CategoryTheory.Epi 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 homModule	—	smul_smul invOf_mul_self' one_smul CategoryTheory.cancel_epi comp_smul smul_comp
instMonoHSMulHomOfInvertible 📖	mathematical	—	CategoryTheory.Mono 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 homModule	—	smul_smul invOf_mul_self' one_smul CategoryTheory.cancel_mono smul_comp comp_smul
leftComp_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup homModule LinearMap.instFunLike leftComp CategoryTheory.CategoryStruct.comp	—	—
rightComp_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup homModule LinearMap.instFunLike rightComp CategoryTheory.CategoryStruct.comp	—	—
smul_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver 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 homModule	—	—
units_smul_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Quiver.Hom CategoryTheory.CategoryStruct.toQuiver 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 homModule	—	smul_comp

---

← Back to Index