Semi

📁 Source: Mathlib/Algebra/Category/ModuleCat/Semi.lean

Statistics

Metric	Count
Definitions toLinearEquivₛ, toModuleIsoₛ, SemimoduleCat, instModuleCarrier, hom, hom, hom', hom₂, instModule, carrier, hasForgetToAddCommMonoid, homAddEquiv, homEquiv, homLinearEquiv, instAddCommMonoidHom, instAddHom, instCoeSortType, instConcreteCategoryLinearMapIdCarrier, instHasZeroMorphisms, instInhabited, instSMulHom, instSMulNatHom, instZeroHom, isAddCommMonoid, isModule, moduleCategory, of, ofHom, ofHom₂, «term↟_», linearEquivIsoModuleIsoₛ	31
Theorems toModuleIsoₛ_hom, toModuleIsoₛ_inv, comp_id_semiModuleCat, id_semiModuleCat_comp, instIsScalarTowerCarrier, instSMulCommClassCarrier, ext, ext_iff, hom₂_apply, hom₂_ofHom₂, conj_eq_conj, homCongr_eq_arrowCongr, coe_of, comp_apply, forget_map, forget_obj, forget₂_map, forget₂_obj, forget₂_obj_moduleCat_of, homAddEquiv_apply, homAddEquiv_symm_apply_hom, homLinearEquiv_apply, homLinearEquiv_symm_apply, hom_add, hom_bijective, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_injective, hom_inv_apply, hom_nsmul, hom_ofHom, hom_smul, hom_sum, hom_surjective, hom_zero, hom_zsmul, id_apply, instHasZeroObject, instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, instReflectsIsomorphismsForgetLinearMapIdCarrier, inv_hom_apply, isZero_iff_subsingleton, isZero_of_iff_subsingleton, isZero_of_subsingleton, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, ofHom₂_hom_apply_hom, ofHom₂_hom₂, of_coe, subsingleton_of_isZero, linearEquivIsoModuleIsoₛ_hom, linearEquivIsoModuleIsoₛ_inv	56
Total	87

CategoryTheory.Iso

Definitions

Name	Category	Theorems
toLinearEquivₛ 📖	CompOp	3 math math: SemimoduleCat.Iso.homCongr_eq_arrowCongr, SemimoduleCat.Iso.conj_eq_conj, linearEquivIsoModuleIsoₛ_inv

LinearEquiv

Definitions

Name	Category	Theorems
toModuleIsoₛ 📖	CompOp	3 math math: linearEquivIsoModuleIsoₛ_hom, toModuleIsoₛ_hom, toModuleIsoₛ_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toModuleIsoₛ_hom 📖	mathematical	—	CategoryTheory.Iso.hom SemimoduleCat SemimoduleCat.moduleCategory SemimoduleCat.of toModuleIsoₛ SemimoduleCat.ofHom toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids	—	RingHomInvPair.ids
toModuleIsoₛ_inv 📖	mathematical	—	CategoryTheory.Iso.inv SemimoduleCat SemimoduleCat.moduleCategory SemimoduleCat.of toModuleIsoₛ SemimoduleCat.ofHom toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids symm	—	RingHomInvPair.ids

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_id_semiModuleCat 📖	mathematical	—	comp SemimoduleCat.carrier SemimoduleCat.isAddCommMonoid SemimoduleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids SemimoduleCat.Hom.hom CategoryTheory.CategoryStruct.id SemimoduleCat CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory	—	—
id_semiModuleCat_comp 📖	mathematical	—	comp SemimoduleCat.carrier SemimoduleCat.isAddCommMonoid SemimoduleCat.isModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids SemimoduleCat.Hom.hom CategoryTheory.CategoryStruct.id SemimoduleCat CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory	—	—

SemimoduleCat

Definitions

Name	Category	Theorems
carrier 📖	CompOp	68 math math: MonoidalCategory.triangle, Hom.hom₂_apply, of_coe, instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, MonoidalCategory.rightUnitor_hom_apply, Iso.homCongr_eq_arrowCongr, hom_zsmul, hom_nsmul, hom_inv_rightUnitor, instReflectsIsomorphismsForgetLinearMapIdCarrier, forget_obj, isZero_iff_subsingleton, MonoidalCategory.tensorHom_tmul, ofHom₂_hom_apply_hom, MonoidalCategory.whiskerRight_apply, homLinearEquiv_apply, Algebra.instIsScalarTowerCarrier, MonoidalCategory.rightUnitor_inv_apply, forget₂_obj_moduleCat_of, instInvertibleCarrierOutSemimoduleCatValSkeleton, hom_hom_rightUnitor, coe_of, hom_inv_apply, ofHom_hom, hom_inv_leftUnitor, hom_tensorHom, MonoidalCategory.tensorμ_apply, homAddEquiv_apply, hom_inv_associator, MonoidalCategory.braiding_hom_apply, MonoidalCategory.braiding_inv_apply, subsingleton_of_isZero, Algebra.instSMulCommClassCarrier, id_apply, hom_whiskerLeft, hom_zero, hom_injective, MonoidalCategory.associator_inv_apply, MonoidalCategory.whiskerLeft_apply, hom_bijective, Iso.conj_eq_conj, hom_whiskerRight, hom_hom_associator, MonoidalCategory.leftUnitor_naturality, MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, inv_hom_apply, LinearMap.id_semiModuleCat_comp, forget_map, MonoidalCategory.leftUnitor_inv_apply, LinearMap.comp_id_semiModuleCat, hom_hom_leftUnitor, hom_comp, hom_add, MonoidalCategory.rightUnitor_naturality, ofHom_apply, homLinearEquiv_symm_apply, MonoidalCategory.leftUnitor_hom_apply, hom_smul, hom_sum, comp_apply, forget₂_obj, hom_id, forget₂_map, hom_surjective, homAddEquiv_symm_apply_hom, MonoidalCategory.associator_hom_apply, MonoidalCategory.tensorUnit_carrier, MonoidalCategory.id_tensorHom_id
hasForgetToAddCommMonoid 📖	CompOp	4 math math: instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, forget₂_obj_moduleCat_of, forget₂_obj, forget₂_map
homAddEquiv 📖	CompOp	4 math math: homLinearEquiv_apply, homAddEquiv_apply, homLinearEquiv_symm_apply, homAddEquiv_symm_apply_hom
homEquiv 📖	CompOp	—
homLinearEquiv 📖	CompOp	3 math math: Hom.hom₂_apply, homLinearEquiv_apply, homLinearEquiv_symm_apply
instAddCommMonoidHom 📖	CompOp	5 math math: Hom.hom₂_apply, ofHom₂_hom_apply_hom, homLinearEquiv_apply, homLinearEquiv_symm_apply, hom_sum
instAddHom 📖	CompOp	5 math math: homLinearEquiv_apply, homAddEquiv_apply, hom_add, homLinearEquiv_symm_apply, homAddEquiv_symm_apply_hom
instCoeSortType 📖	CompOp	—
instConcreteCategoryLinearMapIdCarrier 📖	CompOp	25 math math: instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, MonoidalCategory.rightUnitor_hom_apply, instReflectsIsomorphismsForgetLinearMapIdCarrier, forget_obj, MonoidalCategory.tensorHom_tmul, MonoidalCategory.whiskerRight_apply, MonoidalCategory.rightUnitor_inv_apply, forget₂_obj_moduleCat_of, MonoidalCategory.tensorLift_tmul, hom_inv_apply, MonoidalCategory.tensorμ_apply, MonoidalCategory.braiding_hom_apply, MonoidalCategory.braiding_inv_apply, id_apply, MonoidalCategory.associator_inv_apply, MonoidalCategory.whiskerLeft_apply, inv_hom_apply, forget_map, MonoidalCategory.leftUnitor_inv_apply, ofHom_apply, MonoidalCategory.leftUnitor_hom_apply, comp_apply, forget₂_obj, forget₂_map, MonoidalCategory.associator_hom_apply
instHasZeroMorphisms 📖	CompOp	—
instInhabited 📖	CompOp	—
instSMulHom 📖	CompOp	1 math math: hom_smul
instSMulNatHom 📖	CompOp	2 math math: hom_zsmul, hom_nsmul
instZeroHom 📖	CompOp	1 math math: hom_zero
isAddCommMonoid 📖	CompOp	72 math math: MonoidalCategory.triangle, Hom.hom₂_apply, of_coe, instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, MonoidalCategory.rightUnitor_hom_apply, Iso.homCongr_eq_arrowCongr, CommRing.Pic.mul_eq_tensor, hom_zsmul, hom_nsmul, hom_inv_rightUnitor, instReflectsIsomorphismsForgetLinearMapIdCarrier, forget_obj, MonoidalCategory.tensorHom_tmul, ofHom₂_hom_apply_hom, MonoidalCategory.whiskerRight_apply, homLinearEquiv_apply, Algebra.instIsScalarTowerCarrier, MonoidalCategory.rightUnitor_inv_apply, forget₂_obj_moduleCat_of, instInvertibleCarrierOutSemimoduleCatValSkeleton, CommRing.Pic.inv_eq_dual, hom_hom_rightUnitor, CommRing.Pic.mk_eq_iff, CommRing.Pic.mk_eq_self, MonoidalCategory.tensorUnit_isAddCommMonoid, CommRing.Pic.mapAlgebra_apply, CommRing.Pic.ext_iff, CommRing.Pic.instFreeAsModuleOfNat, hom_inv_apply, ofHom_hom, hom_inv_leftUnitor, hom_tensorHom, MonoidalCategory.tensorμ_apply, homAddEquiv_apply, hom_inv_associator, MonoidalCategory.braiding_hom_apply, MonoidalCategory.braiding_inv_apply, Algebra.instSMulCommClassCarrier, id_apply, hom_whiskerLeft, hom_zero, hom_injective, MonoidalCategory.associator_inv_apply, MonoidalCategory.whiskerLeft_apply, hom_bijective, Iso.conj_eq_conj, hom_whiskerRight, hom_hom_associator, MonoidalCategory.leftUnitor_naturality, MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, inv_hom_apply, LinearMap.id_semiModuleCat_comp, forget_map, MonoidalCategory.leftUnitor_inv_apply, LinearMap.comp_id_semiModuleCat, hom_hom_leftUnitor, hom_comp, hom_add, MonoidalCategory.rightUnitor_naturality, ofHom_apply, homLinearEquiv_symm_apply, MonoidalCategory.leftUnitor_hom_apply, hom_smul, hom_sum, comp_apply, forget₂_obj, hom_id, forget₂_map, hom_surjective, homAddEquiv_symm_apply_hom, MonoidalCategory.associator_hom_apply, MonoidalCategory.id_tensorHom_id
isModule 📖	CompOp	72 math math: MonoidalCategory.triangle, Hom.hom₂_apply, of_coe, instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, MonoidalCategory.rightUnitor_hom_apply, Iso.homCongr_eq_arrowCongr, CommRing.Pic.mul_eq_tensor, hom_zsmul, hom_nsmul, hom_inv_rightUnitor, instReflectsIsomorphismsForgetLinearMapIdCarrier, forget_obj, MonoidalCategory.tensorHom_tmul, ofHom₂_hom_apply_hom, MonoidalCategory.whiskerRight_apply, homLinearEquiv_apply, Algebra.instIsScalarTowerCarrier, MonoidalCategory.rightUnitor_inv_apply, forget₂_obj_moduleCat_of, instInvertibleCarrierOutSemimoduleCatValSkeleton, CommRing.Pic.inv_eq_dual, hom_hom_rightUnitor, CommRing.Pic.mk_eq_iff, CommRing.Pic.mk_eq_self, CommRing.Pic.mapAlgebra_apply, CommRing.Pic.ext_iff, CommRing.Pic.instFreeAsModuleOfNat, hom_inv_apply, ofHom_hom, hom_inv_leftUnitor, hom_tensorHom, MonoidalCategory.tensorμ_apply, homAddEquiv_apply, hom_inv_associator, MonoidalCategory.braiding_hom_apply, MonoidalCategory.braiding_inv_apply, Algebra.instSMulCommClassCarrier, id_apply, hom_whiskerLeft, hom_zero, hom_injective, MonoidalCategory.associator_inv_apply, MonoidalCategory.whiskerLeft_apply, hom_bijective, Iso.conj_eq_conj, hom_whiskerRight, hom_hom_associator, MonoidalCategory.leftUnitor_naturality, MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, inv_hom_apply, LinearMap.id_semiModuleCat_comp, forget_map, MonoidalCategory.leftUnitor_inv_apply, LinearMap.comp_id_semiModuleCat, hom_hom_leftUnitor, MonoidalCategory.tensorUnit_isModule, hom_comp, hom_add, MonoidalCategory.rightUnitor_naturality, ofHom_apply, homLinearEquiv_symm_apply, MonoidalCategory.leftUnitor_hom_apply, hom_smul, hom_sum, comp_apply, forget₂_obj, hom_id, forget₂_map, hom_surjective, homAddEquiv_symm_apply_hom, MonoidalCategory.associator_hom_apply, MonoidalCategory.id_tensorHom_id
moduleCategory 📖	CompOp	94 math math: MonoidalCategory.triangle, Hom.hom₂_apply, instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, MonoidalCategory.rightUnitor_hom_apply, Iso.homCongr_eq_arrowCongr, CommRing.Pic.mul_eq_tensor, hom_zsmul, hom_nsmul, MonoidalCategory.associator_naturality, hom_inv_rightUnitor, instReflectsIsomorphismsForgetLinearMapIdCarrier, forget_obj, isZero_iff_subsingleton, MonoidalCategory.tensorHom_tmul, ofHom₂_hom_apply_hom, MonoidalCategory.whiskerRight_apply, MonoidalCategory.braiding_naturality_right, homLinearEquiv_apply, MonoidalCategory.rightUnitor_inv_apply, forget₂_obj_moduleCat_of, instInvertibleCarrierOutSemimoduleCatValSkeleton, CommRing.Pic.inv_eq_dual, hom_hom_rightUnitor, CommRing.Pic.mk_eq_iff, CommRing.Pic.mk_eq_self, MonoidalCategory.tensorLift_tmul, MonoidalCategory.tensorUnit_isAddCommMonoid, CommRing.Pic.mapAlgebra_apply, CommRing.Pic.ext_iff, CommRing.Pic.instFreeAsModuleOfNat, hom_inv_apply, MonoidalCategory.whiskerLeft_def, hom_inv_leftUnitor, MonoidalCategory.tensorObj_def, hom_tensorHom, MonoidalCategory.tensorHom_comp_tensorHom, MonoidalCategory.tensorμ_apply, linearEquivIsoModuleIsoₛ_hom, homAddEquiv_apply, hom_inv_associator, MonoidalCategory.braiding_hom_apply, MonoidalCategory.braiding_inv_apply, MonoidalCategory.associator_def, id_apply, hom_whiskerLeft, hom_zero, MonoidalCategory.leftUnitor_def, LinearEquiv.toModuleIsoₛ_hom, LinearEquiv.toModuleIsoₛ_inv, MonoidalCategory.hexagon_forward, MonoidalCategory.rightUnitor_def, isZero_of_subsingleton, MonoidalCategory.associator_inv_apply, ofHom_id, MonoidalCategory.whiskerLeft_apply, Iso.conj_eq_conj, hom_whiskerRight, isZero_of_iff_subsingleton, hom_hom_associator, MonoidalCategory.leftUnitor_naturality, MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, inv_hom_apply, LinearMap.id_semiModuleCat_comp, forget_map, MonoidalCategory.leftUnitor_inv_apply, MonoidalCategory.tensorHom_def, MonoidalCategory.braiding_naturality, ofHom_comp, LinearMap.comp_id_semiModuleCat, MonoidalCategory.hexagon_reverse, hom_hom_leftUnitor, MonoidalCategory.tensorUnit_isModule, hom_comp, hom_add, MonoidalCategory.rightUnitor_naturality, ofHom_apply, homLinearEquiv_symm_apply, MonoidalCategory.leftUnitor_hom_apply, hom_smul, hom_sum, comp_apply, MonoidalCategory.whiskerRight_def, linearEquivIsoModuleIsoₛ_inv, MonoidalCategory.pentagon, forget₂_obj, hom_id, MonoidalCategory.braiding_naturality_left, forget₂_map, instHasZeroObject, homAddEquiv_symm_apply_hom, MonoidalCategory.associator_hom_apply, instSmallUnitsSkeletonSemimoduleCat, MonoidalCategory.tensorUnit_carrier, MonoidalCategory.id_tensorHom_id
of 📖	CompOp	19 math math: MonoidalCategory.triangle, Hom.hom₂_apply, of_coe, ofHom₂_hom_apply_hom, forget₂_obj_moduleCat_of, coe_of, linearEquivIsoModuleIsoₛ_hom, LinearEquiv.toModuleIsoₛ_hom, LinearEquiv.toModuleIsoₛ_inv, ofHom_id, hom_ofHom, isZero_of_iff_subsingleton, MonoidalCategory.leftUnitor_naturality, ofHom_comp, MonoidalCategory.rightUnitor_naturality, ofHom_apply, linearEquivIsoModuleIsoₛ_inv, homAddEquiv_symm_apply_hom, MonoidalCategory.id_tensorHom_id
ofHom 📖	CompOp	9 math math: Hom.hom₂_apply, ofHom_hom, LinearEquiv.toModuleIsoₛ_hom, LinearEquiv.toModuleIsoₛ_inv, ofHom_id, hom_ofHom, MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, ofHom_comp, ofHom_apply
ofHom₂ 📖	CompOp	3 math math: ofHom₂_hom_apply_hom, Hom.hom₂_ofHom₂, ofHom₂_hom₂
«term↟_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_of 📖	mathematical	—	carrier of NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemimoduleCat moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map SemimoduleCat moduleCategory CategoryTheory.types CategoryTheory.forget LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj SemimoduleCat moduleCategory CategoryTheory.types CategoryTheory.forget LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier	—	—
forget₂_map 📖	mathematical	—	CategoryTheory.Functor.map SemimoduleCat moduleCategory AddCommMonCat AddCommMonCat.instCategory CategoryTheory.forget₂ LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommMonCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommMonCat.str AddMonoidHom.instFunLike AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommMonoid AddCommMonCat.ofHom AddMonoidHomClass.toAddMonoidHom DistribMulActionSemiHomClass.toAddMonoidHomClass DFunLike.coe RingHom RingHom.instFunLike MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Hom.hom	—	—
forget₂_obj 📖	mathematical	—	CategoryTheory.Functor.obj SemimoduleCat moduleCategory AddCommMonCat AddCommMonCat.instCategory CategoryTheory.forget₂ LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommMonCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommMonCat.str AddMonoidHom.instFunLike AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommMonoid AddCommMonCat.of	—	—
forget₂_obj_moduleCat_of 📖	mathematical	—	CategoryTheory.Functor.obj SemimoduleCat moduleCategory AddCommMonCat AddCommMonCat.instCategory CategoryTheory.forget₂ LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommMonCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommMonCat.str AddMonoidHom.instFunLike AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommMonoid of AddCommMonCat.of	—	—
homAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule instAddHom LinearMap.instAdd EquivLike.toFunLike AddEquiv.instEquivLike homAddEquiv Hom.hom	—	—
homAddEquiv_symm_apply_hom 📖	mathematical	—	Hom.hom of carrier isAddCommMonoid isModule DFunLike.coe AddEquiv LinearMap RingHom.id Semiring.toNonAssocSemiring Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory LinearMap.instAdd instAddHom EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm homAddEquiv	—	—
homLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory LinearMap carrier isAddCommMonoid isModule instAddCommMonoidHom LinearMap.addCommMonoid Hom.instModule LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike homLinearEquiv Equiv.toFun AddEquiv.toEquiv instAddHom LinearMap.instAdd homAddEquiv	—	RingHomInvPair.ids
homLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap carrier isAddCommMonoid isModule Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory LinearMap.addCommMonoid instAddCommMonoidHom LinearMap.module Hom.instModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm homLinearEquiv Equiv.invFun AddEquiv.toEquiv instAddHom LinearMap.instAdd homAddEquiv	—	RingHomInvPair.ids
hom_add 📖	mathematical	—	Hom.hom Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory instAddHom LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instAdd	—	—
hom_bijective 📖	mathematical	—	Function.Bijective Hom LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule Hom.hom	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp SemimoduleCat CategoryTheory.Category.toCategoryStruct moduleCategory LinearMap.comp carrier isAddCommMonoid isModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id SemimoduleCat CategoryTheory.Category.toCategoryStruct moduleCategory LinearMap.id carrier isAddCommMonoid isModule	—	—
hom_injective 📖	mathematical	—	Hom LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule Hom.hom	—	Function.Bijective.injective hom_bijective
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemimoduleCat moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_nsmul 📖	mathematical	—	Hom.hom Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory instSMulNatHom LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule AddMonoid.toNatSMul AddCommMonoid.toAddMonoid LinearMap.addCommMonoid	—	—
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
hom_smul 📖	mathematical	—	Hom.hom Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory instSMulHom LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instSMul DistribMulAction.toDistribSMul AddCommMonoid.toAddMonoid	—	—
hom_sum 📖	mathematical	—	Hom.hom Finset.sum Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory instAddCommMonoidHom LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.addCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass hom_zero hom_add
hom_surjective 📖	mathematical	—	Hom LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule Hom.hom	—	Function.Bijective.surjective hom_bijective
hom_zero 📖	mathematical	—	Hom.hom Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory instZeroHom LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instZero	—	—
hom_zsmul 📖	mathematical	—	Hom.hom Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory instSMulNatHom LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule AddMonoid.toNatSMul AddCommMonoid.toAddMonoid LinearMap.addCommMonoid	—	hom_nsmul
id_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemimoduleCat moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
instHasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject SemimoduleCat moduleCategory	—	isZero_of_subsingleton
instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms SemimoduleCat moduleCategory AddCommMonCat AddCommMonCat.instCategory CategoryTheory.forget₂ LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommMonCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommMonCat.str AddMonoidHom.instFunLike AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommMonoid	—	CategoryTheory.Functor.map_isIso CategoryTheory.isIso_of_reflects_iso instReflectsIsomorphismsForgetLinearMapIdCarrier
instReflectsIsomorphismsForgetLinearMapIdCarrier 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms SemimoduleCat moduleCategory CategoryTheory.types CategoryTheory.forget LinearMap RingHom.id Semiring.toNonAssocSemiring carrier isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier	—	RingHomInvPair.ids Equiv.left_inv Equiv.right_inv CategoryTheory.Iso.isIso_hom
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom SemimoduleCat moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
isZero_iff_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero SemimoduleCat moduleCategory carrier	—	subsingleton_of_isZero isZero_of_subsingleton
isZero_of_iff_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero SemimoduleCat moduleCategory of	—	isZero_iff_subsingleton
isZero_of_subsingleton 📖	mathematical	—	CategoryTheory.Limits.IsZero SemimoduleCat moduleCategory	—	hom_ext LinearMap.ext map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom SemimoduleCat moduleCategory LinearMap RingHom.id Semiring.toNonAssocSemiring isAddCommMonoid isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids CategoryTheory.CategoryStruct.comp SemimoduleCat CategoryTheory.Category.toCategoryStruct moduleCategory of	—	RingHomCompTriple.ids
ofHom_hom 📖	mathematical	—	ofHom carrier isAddCommMonoid isModule Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom LinearMap.id CategoryTheory.CategoryStruct.id SemimoduleCat CategoryTheory.Category.toCategoryStruct moduleCategory of	—	—
ofHom₂_hom_apply_hom 📖	mathematical	—	Hom.hom CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring carrier Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory isAddCommMonoid instAddCommMonoidHom isModule Hom.instModule LinearMap.instFunLike of smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction ofHom₂ LinearMap.addCommMonoid LinearMap.module	—	smulCommClass_self
ofHom₂_hom₂ 📖	mathematical	—	ofHom₂ Hom.hom₂	—	smulCommClass_self
of_coe 📖	mathematical	—	of carrier isAddCommMonoid isModule	—	—
subsingleton_of_isZero 📖	mathematical	CategoryTheory.Limits.IsZero SemimoduleCat moduleCategory	carrier	—	LinearMap.id_apply hom_id CategoryTheory.Limits.IsZero.iff_id_eq_zero

SemimoduleCat.Algebra

Definitions

Name	Category	Theorems
instModuleCarrier 📖	CompOp	2 math math: instIsScalarTowerCarrier, instSMulCommClassCarrier

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsScalarTowerCarrier 📖	mathematical	—	IsScalarTower SemimoduleCat.carrier Algebra.toSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SemimoduleCat.isAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemimoduleCat.isModule CommSemiring.toSemiring instModuleCarrier	—	Algebra.smul_def SemigroupAction.mul_smul
instSMulCommClassCarrier 📖	mathematical	—	SMulCommClass SemimoduleCat.carrier SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SemimoduleCat.isAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemimoduleCat.isModule CommSemiring.toSemiring instModuleCarrier	—	smul_assoc IsScalarTower.left smul_eq_mul Algebra.commutes SemigroupAction.mul_smul

SemimoduleCat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	31 math math: SemimoduleCat.Iso.homCongr_eq_arrowCongr, SemimoduleCat.hom_zsmul, SemimoduleCat.hom_nsmul, SemimoduleCat.hom_inv_rightUnitor, SemimoduleCat.hom_ext_iff, SemimoduleCat.ofHom₂_hom_apply_hom, SemimoduleCat.hom_hom_rightUnitor, SemimoduleCat.ofHom_hom, SemimoduleCat.hom_inv_leftUnitor, SemimoduleCat.hom_tensorHom, SemimoduleCat.homAddEquiv_apply, SemimoduleCat.hom_inv_associator, SemimoduleCat.hom_whiskerLeft, SemimoduleCat.hom_zero, SemimoduleCat.hom_injective, SemimoduleCat.hom_bijective, SemimoduleCat.Iso.conj_eq_conj, SemimoduleCat.hom_ofHom, SemimoduleCat.hom_whiskerRight, SemimoduleCat.hom_hom_associator, LinearMap.id_semiModuleCat_comp, LinearMap.comp_id_semiModuleCat, SemimoduleCat.hom_hom_leftUnitor, SemimoduleCat.hom_comp, SemimoduleCat.hom_add, SemimoduleCat.hom_smul, SemimoduleCat.hom_sum, SemimoduleCat.hom_id, SemimoduleCat.forget₂_map, SemimoduleCat.hom_surjective, SemimoduleCat.homAddEquiv_symm_apply_hom
hom' 📖	CompOp	2 math math: hom₂_apply, ext_iff
hom₂ 📖	CompOp	3 math math: hom₂_apply, hom₂_ofHom₂, SemimoduleCat.ofHom₂_hom₂
instModule 📖	CompOp	4 math math: hom₂_apply, SemimoduleCat.ofHom₂_hom_apply_hom, SemimoduleCat.homLinearEquiv_apply, SemimoduleCat.homLinearEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom'	—	—	—
ext_iff 📖	mathematical	—	hom'	—	ext
hom₂_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring SemimoduleCat.carrier SemimoduleCat.isAddCommMonoid SemimoduleCat.isModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike hom₂ Quiver.Hom SemimoduleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory SemimoduleCat.instAddCommMonoidHom instModule hom' SemimoduleCat.of SemimoduleCat.ofHom LinearEquiv.toLinearMap SemimoduleCat.homLinearEquiv	—	smulCommClass_self
hom₂_ofHom₂ 📖	mathematical	—	hom₂ SemimoduleCat.ofHom₂	—	smulCommClass_self

SemimoduleCat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

SemimoduleCat.Iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conj_eq_conj 📖	mathematical	—	DFunLike.coe MulEquiv CategoryTheory.End SemimoduleCat CommSemiring.toSemiring CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory CategoryTheory.End.mul EquivLike.toFunLike MulEquiv.instEquivLike CategoryTheory.Iso.conj LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Module.End SemimoduleCat.carrier SemimoduleCat.isAddCommMonoid SemimoduleCat.isModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearEquiv.instEquivLike LinearEquiv.conj CategoryTheory.Iso.toLinearEquivₛ SemimoduleCat.Hom.hom	—	—
homCongr_eq_arrowCongr 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom SemimoduleCat CommSemiring.toSemiring CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SemimoduleCat.moduleCategory EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Iso.homCongr LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap SemimoduleCat.carrier SemimoduleCat.isAddCommMonoid SemimoduleCat.isModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearEquiv.instEquivLike LinearEquiv.arrowCongr RingHomCompTriple.ids CategoryTheory.Iso.toLinearEquivₛ SemimoduleCat.Hom.hom	—	—

(root)

Definitions

Name	Category	Theorems
SemimoduleCat 📖	CompData	94 math math: SemimoduleCat.MonoidalCategory.triangle, SemimoduleCat.Hom.hom₂_apply, SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier, SemimoduleCat.MonoidalCategory.rightUnitor_hom_apply, SemimoduleCat.Iso.homCongr_eq_arrowCongr, CommRing.Pic.mul_eq_tensor, SemimoduleCat.hom_zsmul, SemimoduleCat.hom_nsmul, SemimoduleCat.MonoidalCategory.associator_naturality, SemimoduleCat.hom_inv_rightUnitor, SemimoduleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier, SemimoduleCat.forget_obj, SemimoduleCat.isZero_iff_subsingleton, SemimoduleCat.MonoidalCategory.tensorHom_tmul, SemimoduleCat.ofHom₂_hom_apply_hom, SemimoduleCat.MonoidalCategory.whiskerRight_apply, SemimoduleCat.MonoidalCategory.braiding_naturality_right, SemimoduleCat.homLinearEquiv_apply, SemimoduleCat.MonoidalCategory.rightUnitor_inv_apply, SemimoduleCat.forget₂_obj_moduleCat_of, instInvertibleCarrierOutSemimoduleCatValSkeleton, CommRing.Pic.inv_eq_dual, SemimoduleCat.hom_hom_rightUnitor, CommRing.Pic.mk_eq_iff, CommRing.Pic.mk_eq_self, SemimoduleCat.MonoidalCategory.tensorLift_tmul, SemimoduleCat.MonoidalCategory.tensorUnit_isAddCommMonoid, CommRing.Pic.mapAlgebra_apply, CommRing.Pic.ext_iff, CommRing.Pic.instFreeAsModuleOfNat, SemimoduleCat.hom_inv_apply, SemimoduleCat.MonoidalCategory.whiskerLeft_def, SemimoduleCat.hom_inv_leftUnitor, SemimoduleCat.MonoidalCategory.tensorObj_def, SemimoduleCat.hom_tensorHom, SemimoduleCat.MonoidalCategory.tensorHom_comp_tensorHom, SemimoduleCat.MonoidalCategory.tensorμ_apply, linearEquivIsoModuleIsoₛ_hom, SemimoduleCat.homAddEquiv_apply, SemimoduleCat.hom_inv_associator, SemimoduleCat.MonoidalCategory.braiding_hom_apply, SemimoduleCat.MonoidalCategory.braiding_inv_apply, SemimoduleCat.MonoidalCategory.associator_def, SemimoduleCat.id_apply, SemimoduleCat.hom_whiskerLeft, SemimoduleCat.hom_zero, SemimoduleCat.MonoidalCategory.leftUnitor_def, LinearEquiv.toModuleIsoₛ_hom, LinearEquiv.toModuleIsoₛ_inv, SemimoduleCat.MonoidalCategory.hexagon_forward, SemimoduleCat.MonoidalCategory.rightUnitor_def, SemimoduleCat.isZero_of_subsingleton, SemimoduleCat.MonoidalCategory.associator_inv_apply, SemimoduleCat.ofHom_id, SemimoduleCat.MonoidalCategory.whiskerLeft_apply, SemimoduleCat.Iso.conj_eq_conj, SemimoduleCat.hom_whiskerRight, SemimoduleCat.isZero_of_iff_subsingleton, SemimoduleCat.hom_hom_associator, SemimoduleCat.MonoidalCategory.leftUnitor_naturality, SemimoduleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm, SemimoduleCat.inv_hom_apply, LinearMap.id_semiModuleCat_comp, SemimoduleCat.forget_map, SemimoduleCat.MonoidalCategory.leftUnitor_inv_apply, SemimoduleCat.MonoidalCategory.tensorHom_def, SemimoduleCat.MonoidalCategory.braiding_naturality, SemimoduleCat.ofHom_comp, LinearMap.comp_id_semiModuleCat, SemimoduleCat.MonoidalCategory.hexagon_reverse, SemimoduleCat.hom_hom_leftUnitor, SemimoduleCat.MonoidalCategory.tensorUnit_isModule, SemimoduleCat.hom_comp, SemimoduleCat.hom_add, SemimoduleCat.MonoidalCategory.rightUnitor_naturality, SemimoduleCat.ofHom_apply, SemimoduleCat.homLinearEquiv_symm_apply, SemimoduleCat.MonoidalCategory.leftUnitor_hom_apply, SemimoduleCat.hom_smul, SemimoduleCat.hom_sum, SemimoduleCat.comp_apply, SemimoduleCat.MonoidalCategory.whiskerRight_def, linearEquivIsoModuleIsoₛ_inv, SemimoduleCat.MonoidalCategory.pentagon, SemimoduleCat.forget₂_obj, SemimoduleCat.hom_id, SemimoduleCat.MonoidalCategory.braiding_naturality_left, SemimoduleCat.forget₂_map, SemimoduleCat.instHasZeroObject, SemimoduleCat.homAddEquiv_symm_apply_hom, SemimoduleCat.MonoidalCategory.associator_hom_apply, instSmallUnitsSkeletonSemimoduleCat, SemimoduleCat.MonoidalCategory.tensorUnit_carrier, SemimoduleCat.MonoidalCategory.id_tensorHom_id
linearEquivIsoModuleIsoₛ 📖	CompOp	2 math math: linearEquivIsoModuleIsoₛ_hom, linearEquivIsoModuleIsoₛ_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearEquivIsoModuleIsoₛ_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.types LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CategoryTheory.Iso SemimoduleCat SemimoduleCat.moduleCategory SemimoduleCat.of linearEquivIsoModuleIsoₛ LinearEquiv.toModuleIsoₛ	—	RingHomInvPair.ids
linearEquivIsoModuleIsoₛ_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.types LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids CategoryTheory.Iso SemimoduleCat SemimoduleCat.moduleCategory SemimoduleCat.of linearEquivIsoModuleIsoₛ CategoryTheory.Iso.toLinearEquivₛ	—	RingHomInvPair.ids

---

← Back to Index