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	4 math math: CategoryTheory.Functor.fullSubcategoryInclusionLinear, FGModuleCat.instFiniteHom, CategoryTheory.ObjectProperty.instMonoidalLinearFullSubcategory, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG
homCongr 📖	CompOp	2 math math: homCongr_apply, homCongr_symm_apply
homModule 📖	CompOp	121 math math: CategoryTheory.ShortComplex.opcyclesMap_smul, Rep.resCoindHomEquiv_symm_apply_hom, Rep.resCoindHomEquiv_apply_hom, CategoryTheory.ShortComplex.homologyMap_smul, CategoryTheory.linearCoyoneda_map_app, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, Rep.MonoidalClosed.linearHomEquiv_symm_hom, instMonoHSMulHomOfInvertible, CategoryTheory.Functor.coe_mapLinearMap, CategoryTheory.finrank_hom_simple_simple_le_one, CategoryTheory.ShortComplex.Homotopy.smul_h₁, CategoryTheory.InducedCategory.homLinearEquiv_apply, Rep.diagonalHomEquiv_symm_apply, CategoryTheory.linearYoneda_obj_map, comp_apply, CategoryTheory.finrank_hom_simple_simple_eq_one_iff, CategoryTheory.Abelian.Ext.smul_hom, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, 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₂, Rep.MonoidalClosed.linearHomEquivComm_hom, FDRep.instFiniteDimensionalHom, Rep.coindVEquiv_symm_apply_coe, 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, Rep.resIndAdjunction_homEquiv_symm_apply, Rep.coindMap'_hom, Rep.freeLiftLEquiv_apply, 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, Rep.resIndAdjunction_homEquiv_apply, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, CategoryTheory.ShortComplex.smul_τ₃, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, Rep.leftRegularHomEquiv_symm_apply, CategoryTheory.endomorphism_simple_eq_smul_id, Rep.coindResAdjunction_homEquiv_apply, CategoryTheory.ShiftedHom.comp_smul, Representation.coind'_apply_apply, Rep.coindIso_inv_hom_hom, homCongr_apply, CategoryTheory.ShortComplex.cyclesMap'_smul, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, comp_smul, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH, 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, Rep.coindResAdjunction_homEquiv_symm_apply, Rep.coindVEquiv_apply_hom, Rep.leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, 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, Rep.MonoidalClosed.linearHomEquiv_hom, CategoryTheory.MonoidalLinear.smul_whiskerRight, CategoryTheory.MonoidalLinear.whiskerLeft_smul, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, 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, Rep.leftRegularHomEquiv_apply, ModuleCat.ofHom₂_compr₂, CategoryTheory.finrank_endomorphism_simple_eq_one, CategoryTheory.ShortComplex.smul_τ₁, CategoryTheory.ShortComplex.smul_τ₂, CategoryTheory.Abelian.Ext.linearEquiv₀_symm_apply, Rep.diagonalHomEquiv_apply, CategoryTheory.Functor.linear_iff, Rep.freeLiftLEquiv_symm_apply, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, CategoryTheory.ShortComplex.rightHomologyMap'_smul, Rep.indResHomEquiv_apply_hom, CategoryTheory.ShortComplex.rightHomologyMap_smul, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, toCatCenter_apply_app, FDRep.scalar_product_char_eq_finrank_equivariant, Representation.linHom.invariantsEquivRepHom_apply_hom, CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom, Rep.coindIso_hom_hom_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, Rep.indResHomEquiv_symm_apply_hom, 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	6 math math: CategoryTheory.linearCoyoneda_map_app, CategoryTheory.linearYoneda_map_app, Rep.coindMap'_hom, 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