ChangeOfRings

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

Statistics

Metric	Count
Definitions «term_⊗ₜ[_,_]_», distribMulAction, hasSMul, instCoeFunCarrierObj'Forall, instCoeFunCarrierObjCoextendScalarsForall, isModule, map', mulAction, obj', map, evalAt, fromExtendScalars, toRestrictScalars, map, counit, homEquiv, unit, map', obj', map', obj', fromRestriction, toRestriction, app', counit', unit', coextendScalars, extendRestrictScalarsAdj, extendScalars, extendScalarsComp, extendScalarsId, instModuleCarrierObjRestrictScalars, restrictCoextendScalarsAdj, restrictScalars, restrictScalarsComp, restrictScalarsComp', restrictScalarsComp'App, restrictScalarsCongr, restrictScalarsEquivalenceOfRingEquiv, restrictScalarsId, restrictScalarsId', restrictScalarsId'App, semilinearMapAddEquiv	43
Theorems instLinearRestrictScalars, restrictScalarsEquivalenceOfRingEquiv_linear, map'_hom_apply_apply, map_apply, smul_apply, smul_apply', map_hom_apply, evalAt_apply, fromExtendScalars_hom_apply, toRestrictScalars_hom_apply, counit_app, homEquiv_symm_apply, unit_app, hom_ext, hom_ext_iff, map'_comp, map'_id, map_tmul, smul_tmul, fromRestriction_hom_apply_apply, toRestriction_hom_apply, counit'_app, unit'_app, extendRestrictScalarsAdj_homEquiv_apply, extendRestrictScalarsAdj_unit_app_apply, extendScalarsComp_hom_app_one_tmul, extendScalarsId_hom_app_one_tmul, extendScalarsId_inv_app_apply, extendScalars_assoc, extendScalars_assoc', extendScalars_assoc_assoc, extendScalars_comp_id, extendScalars_comp_id_assoc, extendScalars_id_comp, extendScalars_id_comp_assoc, homEquiv_extendScalarsComp, homEquiv_extendScalarsId, instAdditiveRestrictScalars, instFaithfulRestrictScalars, instIsLeftAdjointExtendScalars, instIsLeftAdjointRestrictScalars, instIsRightAdjointCoextendScalars, instIsRightAdjointRestrictScalars, instPreservesMonomorphismsRestrictScalars, instReflectsIsomorphismsRestrictScalars, preservesColimit_restrictScalars, preservesLimit_restrictScalars, map_apply, smul_def, smul_def', restrictScalarsComp'App_hom_apply, restrictScalarsComp'App_hom_naturality, restrictScalarsComp'App_hom_naturality_assoc, restrictScalarsComp'App_inv_apply, restrictScalarsComp'App_inv_naturality, restrictScalarsComp'App_inv_naturality_assoc, restrictScalarsComp'_hom_app, restrictScalarsComp'_inv_app, restrictScalarsCongr_hom_app, restrictScalarsCongr_inv_app, restrictScalarsCongr_symm, restrictScalarsEquivalenceOfRingEquiv_additive, restrictScalarsId'App_hom_apply, restrictScalarsId'App_hom_naturality, restrictScalarsId'App_hom_naturality_assoc, restrictScalarsId'App_inv_apply, restrictScalarsId'App_inv_naturality, restrictScalarsId'App_inv_naturality_assoc, restrictScalarsId'_hom_app, restrictScalarsId'_inv_app, restrictScalars_isEquivalence_of_ringEquiv, sMulCommClass_mk, semilinearMapAddEquiv_apply, semilinearMapAddEquiv_symm_apply_apply	74
Total	117

ChangeOfRings

Definitions

Name	Category	Theorems
«term_⊗ₜ[_,_]_» 📖	CompOp	—

ModuleCat

Definitions

Name	Category	Theorems
coextendScalars 📖	CompOp	7 math math: instIsRightAdjointCoextendScalars, RestrictionCoextensionAdj.HomEquiv.toRestriction_hom_apply, RestrictionCoextensionAdj.counit'_app, CoextendScalars.smul_apply, RestrictionCoextensionAdj.unit'_app, RestrictionCoextensionAdj.HomEquiv.fromRestriction_hom_apply_apply, CoextendScalars.map_apply
extendRestrictScalarsAdj 📖	CompOp	4 math math: extendRestrictScalarsAdj_homEquiv_apply, homEquiv_extendScalarsComp, extendRestrictScalarsAdj_unit_app_apply, homEquiv_extendScalarsId
extendScalars 📖	CompOp	28 math math: extendScalarsId_hom_app_one_tmul, preservesFiniteLimits_extendScalars_of_flat, extendRestrictScalarsAdj_homEquiv_apply, ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_hom_apply, ExtendRestrictScalarsAdj.Counit.map_hom_apply, extendScalars_assoc_assoc, ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply, CommRingCat.moduleCatExtendScalarsPseudofunctor_map, reflectsIsomorphisms_extendScalars_of_faithfullyFlat, ExtendRestrictScalarsAdj.homEquiv_symm_apply, homEquiv_extendScalarsComp, ExtendScalars.map_tmul, extendScalars_id_comp_assoc, extendScalars_assoc', extendScalars_id_comp, ExtendRestrictScalarsAdj.counit_app, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp, extendScalarsComp_hom_app_one_tmul, instIsLeftAdjointExtendScalars, extendScalars_comp_id_assoc, extendScalars_comp_id, extendRestrictScalarsAdj_unit_app_apply, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId, extendScalarsId_inv_app_apply, homEquiv_extendScalarsId, ExtendScalars.hom_ext_iff, extendScalars_assoc, ExtendRestrictScalarsAdj.unit_app
extendScalarsComp 📖	CompOp	10 math math: extendScalars_assoc_assoc, homEquiv_extendScalarsComp, extendScalars_id_comp_assoc, extendScalars_assoc', extendScalars_id_comp, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp, extendScalarsComp_hom_app_one_tmul, extendScalars_comp_id_assoc, extendScalars_comp_id, extendScalars_assoc
extendScalarsId 📖	CompOp	8 math math: extendScalarsId_hom_app_one_tmul, extendScalars_id_comp_assoc, extendScalars_id_comp, extendScalars_comp_id_assoc, extendScalars_comp_id, CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId, extendScalarsId_inv_app_apply, homEquiv_extendScalarsId
instModuleCarrierObjRestrictScalars 📖	CompOp	6 math math: ExtendRestrictScalarsAdj.Counit.map_hom_apply, PresheafOfModules.map_smul, PresheafOfModules.Monoidal.tensorObj_map_tmul, ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply, ExtendScalars.smul_tmul, ExtendRestrictScalarsAdj.HomEquiv.evalAt_apply
restrictCoextendScalarsAdj 📖	CompOp	—
restrictScalars 📖	CompOp	103 math math: instPreservesMonomorphismsRestrictScalars, CommRingCat.KaehlerDifferential.map_d, restrictScalars.map_apply, restrictScalarsCongr_symm, restrictScalarsId'App_inv_naturality_assoc, extendScalarsId_hom_app_one_tmul, PresheafOfModules.restrictScalars_map_app, restrictScalarsComp'App_hom_apply, CoextendScalars.smul_apply', PresheafOfModules.limitPresheafOfModules_map, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, PresheafOfModules.sections_property, PresheafOfModules.toSheafify_app_apply', PresheafOfModules.Derivation.d_map, RestrictionCoextensionAdj.HomEquiv.toRestriction_hom_apply, extendRestrictScalarsAdj_homEquiv_apply, restrictScalarsComp'_inv_app, PresheafOfModules.congr_map_apply, PresheafOfModules.restrictScalarsObj_map, restrictScalarsId'App_hom_naturality, ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_hom_apply, restrictScalars_isEquivalence_of_ringEquiv, restrictScalarsComp'_hom_app, PresheafOfModules.restrictScalarsObj_obj, ExtendRestrictScalarsAdj.Counit.map_hom_apply, PresheafOfModules.map_comp_apply, RestrictionCoextensionAdj.counit'_app, PresheafOfModules.pushforward_map_app_apply', CoextendScalars.smul_apply, PresheafOfModules.unit_map_one, CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId, restrictScalarsId'App_inv_naturality, PresheafOfModules.map_smul, restrictScalarsId'_inv_app, PresheafOfModules.Monoidal.tensorObj_map_tmul, restrictScalarsId'App_hom_apply, restrictScalarsId'App_hom_naturality_assoc, PresheafOfModules.freeObj_map, CommRingCat.moduleCatRestrictScalarsPseudofunctor_map, PresheafOfModules.presheaf_map_apply_coe, restrictScalarsComp'App_hom_naturality_assoc, PresheafOfModules.forgetToPresheafModuleCatObjMap_apply, restrictScalarsCongr_hom_app, ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply, instIsRightAdjointRestrictScalars, instIsLeftAdjointRestrictScalars, PresheafOfModules.pushforward_obj_map_apply, ExtendRestrictScalarsAdj.homEquiv_symm_apply, RestrictionCoextensionAdj.unit'_app, RingCat.moduleCatRestrictScalarsPseudofunctor_mapId, Algebra.instLinearRestrictScalars, instReflectsIsomorphismsRestrictScalars, SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app, ExtendScalars.smul_tmul, restrictScalarsComp'App_hom_naturality, homEquiv_extendScalarsComp, ExtendScalars.map_tmul, PresheafOfModules.map_comp, RingCat.moduleCatRestrictScalarsPseudofunctor_map, restrictScalarsComp'App_inv_naturality, restrictScalarsComp'App_inv_naturality_assoc, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d, PresheafOfModules.pushforward_obj_obj, instAdditiveRestrictScalars, PresheafOfModules.Hom.naturality_assoc, PresheafOfModules.restriction_app, restrictScalars.smul_def, restrictScalarsId'_hom_app, ExtendRestrictScalarsAdj.HomEquiv.evalAt_apply, RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, PresheafOfModules.instHasLimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap, ExtendRestrictScalarsAdj.counit_app, SheafOfModules.pushforwardNatTrans_app_val_app, instFaithfulRestrictScalars, PresheafOfModules.map_id, extendScalarsComp_hom_app_one_tmul, preservesFiniteLimits_tensorLeft_of_ringHomFlat, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, restrictScalars.smul_def', PresheafOfModules.pushforward_obj_map_apply', PresheafOfModules.Hom.naturality, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_aux, extendRestrictScalarsAdj_unit_app_apply, SheafOfModules.pushforwardNatTrans_app_val_app_apply, PresheafOfModules.ofPresheaf_map, PresheafOfModules.naturality_apply, extendScalarsId_inv_app_apply, semilinearMapAddEquiv_symm_apply_apply, preservesLimit_restrictScalars, restrictScalarsCongr_inv_app, semilinearMapAddEquiv_apply, CoextendScalars.map'_hom_apply_apply, RestrictionCoextensionAdj.HomEquiv.fromRestriction_hom_apply_apply, SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app, homEquiv_extendScalarsId, ExtendScalars.hom_ext_iff, PresheafOfModules.map_comp_assoc, restrictScalarsId'App_inv_apply, restrictScalarsComp'App_inv_apply, preservesColimit_restrictScalars, ExtendRestrictScalarsAdj.unit_app, CoextendScalars.map_apply
restrictScalarsComp 📖	CompOp	3 math math: CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp, homEquiv_extendScalarsComp, RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp
restrictScalarsComp' 📖	CompOp	4 math math: restrictScalarsComp'_inv_app, restrictScalarsComp'_hom_app, PresheafOfModules.map_comp, PresheafOfModules.map_comp_assoc
restrictScalarsComp'App 📖	CompOp	8 math math: restrictScalarsComp'App_hom_apply, restrictScalarsComp'_inv_app, restrictScalarsComp'_hom_app, restrictScalarsComp'App_hom_naturality_assoc, restrictScalarsComp'App_hom_naturality, restrictScalarsComp'App_inv_naturality, restrictScalarsComp'App_inv_naturality_assoc, restrictScalarsComp'App_inv_apply
restrictScalarsCongr 📖	CompOp	3 math math: restrictScalarsCongr_symm, restrictScalarsCongr_hom_app, restrictScalarsCongr_inv_app
restrictScalarsEquivalenceOfRingEquiv 📖	CompOp	2 math math: restrictScalarsEquivalenceOfRingEquiv_additive, Algebra.restrictScalarsEquivalenceOfRingEquiv_linear
restrictScalarsId 📖	CompOp	3 math math: CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId, RingCat.moduleCatRestrictScalarsPseudofunctor_mapId, homEquiv_extendScalarsId
restrictScalarsId' 📖	CompOp	3 math math: restrictScalarsId'_inv_app, restrictScalarsId'_hom_app, PresheafOfModules.map_id
restrictScalarsId'App 📖	CompOp	8 math math: restrictScalarsId'App_inv_naturality_assoc, restrictScalarsId'App_hom_naturality, restrictScalarsId'App_inv_naturality, restrictScalarsId'_inv_app, restrictScalarsId'App_hom_apply, restrictScalarsId'App_hom_naturality_assoc, restrictScalarsId'_hom_app, restrictScalarsId'App_inv_apply
semilinearMapAddEquiv 📖	CompOp	2 math math: semilinearMapAddEquiv_symm_apply_apply, semilinearMapAddEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendRestrictScalarsAdj_homEquiv_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat CommRing.toRing moduleCategory restrictScalars carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct extendScalars EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv extendRestrictScalarsAdj TensorProduct.tmul CommRing.toCommSemiring of Ring.toAddCommGroup Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
extendRestrictScalarsAdj_unit_app_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat CommRing.toRing moduleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp extendScalars restrictScalars carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit extendRestrictScalarsAdj TensorProduct.tmul CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.compHom CommSemiring.toSemiring Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
extendScalarsComp_hom_app_one_tmul 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat CommRing.toRing moduleCategory extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.comp carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category extendScalarsComp TensorProduct.tmul restrictScalars of Ring.toAddCommGroup Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.compHom TensorProduct.addCommMonoid TensorProduct.leftModule NonUnitalNonAssocRing.toAddCommGroup NonAssocSemiring.toNonUnitalNonAssocSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid MulActionWithZero.toMulAction MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MonoidWithZero.toMulActionWithZero	—	extendRestrictScalarsAdj_homEquiv_apply homEquiv_extendScalarsComp
extendScalarsId_hom_app_one_tmul 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat CommRing.toRing moduleCategory extendScalars RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.id carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category extendScalarsId TensorProduct.tmul restrictScalars of Ring.toAddCommGroup Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	extendRestrictScalarsAdj_homEquiv_apply homEquiv_extendScalarsId
extendScalarsId_inv_app_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat CommRing.toRing moduleCategory CategoryTheory.Functor.id extendScalars RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category extendScalarsId TensorProduct.tmul NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing restrictScalars of Ring.toAddCommGroup Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
extendScalars_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor ModuleCat CommRing.toRing moduleCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.comp CategoryTheory.Iso.hom extendScalarsComp CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.Functor.associator	—	CategoryTheory.NatTrans.ext' ExtendScalars.hom_ext extendScalarsComp_hom_app_one_tmul ExtendScalars.map_tmul
extendScalars_assoc' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor ModuleCat CommRing.toRing moduleCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.comp CategoryTheory.Iso.hom extendScalarsComp CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.associator CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.CategoryStruct.id	—	extendScalars_assoc_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp
extendScalars_assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor ModuleCat CommRing.toRing moduleCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.comp CategoryTheory.Iso.hom extendScalarsComp CategoryTheory.Functor.whiskerRight CategoryTheory.Functor.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.Functor.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' extendScalars_assoc
extendScalars_comp_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor ModuleCat CommRing.toRing moduleCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom extendScalarsComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft extendScalarsId CategoryTheory.Functor.rightUnitor CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.ext' ExtendScalars.hom_ext extendScalarsComp_hom_app_one_tmul extendScalarsId_hom_app_one_tmul
extendScalars_comp_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor ModuleCat CommRing.toRing moduleCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom extendScalarsComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerLeft extendScalarsId CategoryTheory.Functor.rightUnitor	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' extendScalars_comp_id
extendScalars_id_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor ModuleCat CommRing.toRing moduleCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom extendScalarsComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight extendScalarsId CategoryTheory.Functor.leftUnitor CategoryTheory.CategoryStruct.id	—	CategoryTheory.NatTrans.ext' ExtendScalars.hom_ext extendScalarsComp_hom_app_one_tmul ExtendScalars.map_tmul extendScalarsId_hom_app_one_tmul
extendScalars_id_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor ModuleCat CommRing.toRing moduleCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id CategoryTheory.Functor.comp CategoryTheory.Iso.hom extendScalarsComp CategoryTheory.Functor.id CategoryTheory.Functor.whiskerRight extendScalarsId CategoryTheory.Functor.leftUnitor	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' extendScalars_id_comp
homEquiv_extendScalarsComp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom ModuleCat CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj extendScalars RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.comp restrictScalars EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv extendRestrictScalarsAdj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category extendScalarsComp CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.id Ring.toSemiring ExtendScalars.obj' CategoryTheory.Adjunction.unit CategoryTheory.Functor.map CategoryTheory.Iso.inv restrictScalarsComp	—	CategoryTheory.Adjunction.comp_unit_app CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Adjunction.homEquiv_unit CategoryTheory.Adjunction.unit_naturality_assoc CategoryTheory.Adjunction.right_triangle_components
homEquiv_extendScalarsId 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom ModuleCat CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj extendScalars RingHom.id Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CategoryTheory.Functor.id restrictScalars EquivLike.toFunLike Equiv.instEquivLike CategoryTheory.Adjunction.homEquiv extendRestrictScalarsAdj CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category extendScalarsId Ring.toSemiring CategoryTheory.Iso.inv restrictScalarsId	—	hom_ext LinearMap.ext extendRestrictScalarsAdj_homEquiv_apply extendScalarsId_inv_app_apply comp_apply CategoryTheory.Iso.inv_hom_id_app
instAdditiveRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.Additive ModuleCat moduleCategory instPreadditive restrictScalars	—	—
instFaithfulRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.Faithful ModuleCat moduleCategory restrictScalars	—	hom_ext LinearMap.ext DFunLike.congr_fun hom_ext_iff
instIsLeftAdjointExtendScalars 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint ModuleCat CommRing.toRing moduleCategory extendScalars	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsLeftAdjointRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint ModuleCat moduleCategory restrictScalars	—	CategoryTheory.Adjunction.isLeftAdjoint
instIsRightAdjointCoextendScalars 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint ModuleCat moduleCategory coextendScalars	—	CategoryTheory.Adjunction.isRightAdjoint
instIsRightAdjointRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint ModuleCat CommRing.toRing moduleCategory restrictScalars	—	CategoryTheory.Adjunction.isRightAdjoint
instPreservesMonomorphismsRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.PreservesMonomorphisms ModuleCat moduleCategory restrictScalars	—	mono_iff_injective
instReflectsIsomorphismsRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms ModuleCat moduleCategory restrictScalars	—	instReflectsIsomorphismsForgetLinearMapIdCarrier CategoryTheory.reflectsIsomorphisms_of_comp
preservesColimit_restrictScalars 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit ModuleCat moduleCategory restrictScalars	—	CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone HasColimit.instPreservesColimitAddCommGrpCatForget₂LinearMapIdCarrierAddMonoidHomCarrier HasColimit.reflectsColimit
preservesLimit_restrictScalars 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit ModuleCat moduleCategory restrictScalars	—	forget₂AddCommGroup_preservesLimit forget₂AddCommGroup_reflectsLimit
restrictScalarsComp'App_hom_apply 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	DFunLike.coe CategoryTheory.Functor.obj ModuleCat moduleCategory restrictScalars carrier CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom restrictScalarsComp'App	—	—
restrictScalarsComp'App_hom_naturality 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars CategoryTheory.Functor.map CategoryTheory.Iso.hom restrictScalarsComp'App	—	CategoryTheory.NatTrans.naturality
restrictScalarsComp'App_hom_naturality_assoc 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars CategoryTheory.Functor.map CategoryTheory.Iso.hom restrictScalarsComp'App	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictScalarsComp'App_hom_naturality
restrictScalarsComp'App_inv_apply 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	DFunLike.coe CategoryTheory.Functor.obj ModuleCat moduleCategory restrictScalars carrier CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv restrictScalarsComp'App	—	—
restrictScalarsComp'App_inv_naturality 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars CategoryTheory.Functor.map CategoryTheory.Iso.inv restrictScalarsComp'App	—	CategoryTheory.NatTrans.naturality
restrictScalarsComp'App_inv_naturality_assoc 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars CategoryTheory.Functor.map CategoryTheory.Iso.inv restrictScalarsComp'App	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictScalarsComp'App_inv_naturality
restrictScalarsComp'_hom_app 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.NatTrans.app ModuleCat moduleCategory restrictScalars CategoryTheory.Functor.comp CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category restrictScalarsComp' CategoryTheory.Functor.obj restrictScalarsComp'App	—	—
restrictScalarsComp'_inv_app 📖	mathematical	RingHom.comp Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.NatTrans.app ModuleCat moduleCategory CategoryTheory.Functor.comp restrictScalars CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category restrictScalarsComp' CategoryTheory.Functor.obj restrictScalarsComp'App	—	—
restrictScalarsCongr_hom_app 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat moduleCategory restrictScalars carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category restrictScalarsCongr	—	—
restrictScalarsCongr_inv_app 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat moduleCategory restrictScalars carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category restrictScalarsCongr	—	—
restrictScalarsCongr_symm 📖	mathematical	—	CategoryTheory.Iso.symm CategoryTheory.Functor ModuleCat moduleCategory CategoryTheory.Functor.category restrictScalars restrictScalarsCongr RingHom Semiring.toNonAssocSemiring Ring.toSemiring	—	—
restrictScalarsEquivalenceOfRingEquiv_additive 📖	mathematical	—	CategoryTheory.Functor.Additive ModuleCat moduleCategory instPreadditive CategoryTheory.Equivalence.functor restrictScalarsEquivalenceOfRingEquiv	—	—
restrictScalarsId'App_hom_apply 📖	mathematical	RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	DFunLike.coe CategoryTheory.Functor.obj ModuleCat moduleCategory restrictScalars carrier CategoryTheory.ConcreteCategory.hom LinearMap AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom restrictScalarsId'App	—	—
restrictScalarsId'App_hom_naturality 📖	mathematical	RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars CategoryTheory.Functor.map CategoryTheory.Iso.hom restrictScalarsId'App	—	CategoryTheory.NatTrans.naturality
restrictScalarsId'App_hom_naturality_assoc 📖	mathematical	RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars CategoryTheory.Functor.map CategoryTheory.Iso.hom restrictScalarsId'App	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictScalarsId'App_hom_naturality
restrictScalarsId'App_inv_apply 📖	mathematical	RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	DFunLike.coe CategoryTheory.Functor.obj ModuleCat moduleCategory restrictScalars carrier CategoryTheory.ConcreteCategory.hom LinearMap AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv restrictScalarsId'App	—	—
restrictScalarsId'App_inv_naturality 📖	mathematical	RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars CategoryTheory.Iso.inv restrictScalarsId'App CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality
restrictScalarsId'App_inv_naturality_assoc 📖	mathematical	RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars CategoryTheory.Iso.inv restrictScalarsId'App CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' restrictScalarsId'App_inv_naturality
restrictScalarsId'_hom_app 📖	mathematical	RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.NatTrans.app ModuleCat moduleCategory restrictScalars CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category restrictScalarsId' CategoryTheory.Functor.obj restrictScalarsId'App	—	—
restrictScalarsId'_inv_app 📖	mathematical	RingHom.id Semiring.toNonAssocSemiring Ring.toSemiring	CategoryTheory.NatTrans.app ModuleCat moduleCategory CategoryTheory.Functor.id restrictScalars CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category restrictScalarsId' CategoryTheory.Functor.obj restrictScalarsId'App	—	—
restrictScalars_isEquivalence_of_ringEquiv 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence ModuleCat moduleCategory restrictScalars RingEquiv.toRingHom Semiring.toNonAssocSemiring Ring.toSemiring	—	CategoryTheory.Equivalence.isEquivalence_functor
sMulCommClass_mk 📖	mathematical	—	SMulCommClass SemigroupAction.toSMul carrier RestrictScalars.obj' CommRing.toRing of Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid isAddCommGroup Module.toDistribMulAction isModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul CommSemiring.toSemiring CommRing.toCommSemiring	—	mul_comm
semilinearMapAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv LinearMap Ring.toSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule Quiver.Hom ModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars LinearMap.instAdd instAddHom EquivLike.toFunLike AddEquiv.instEquivLike semilinearMapAddEquiv ofHom Module.compHom RingHom.id Semiring.toNonAssocSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap.instFunLike	—	—
semilinearMapAddEquiv_symm_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike AddEquiv Quiver.Hom ModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Functor.obj restrictScalars instAddHom LinearMap.instAdd EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm semilinearMapAddEquiv CategoryTheory.ConcreteCategory.hom RingHom.id Semiring.toNonAssocSemiring instConcreteCategoryLinearMapIdCarrier	—	—

ModuleCat.Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLinearRestrictScalars 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring ModuleCat ModuleCat.moduleCategory ModuleCat.instPreadditive instLinear ModuleCat.restrictScalars AlgHom.toRingHom Ring.toSemiring	—	ModuleCat.hom_ext LinearMap.ext AlgHom.commutes
restrictScalarsEquivalenceOfRingEquiv_linear 📖	mathematical	—	CategoryTheory.Functor.Linear CommSemiring.toSemiring ModuleCat ModuleCat.moduleCategory ModuleCat.instPreadditive instLinear CategoryTheory.Equivalence.functor ModuleCat.restrictScalarsEquivalenceOfRingEquiv AlgEquiv.toRingEquiv Ring.toSemiring	—	instLinearRestrictScalars

ModuleCat.CoextendScalars

Definitions

Name	Category	Theorems
distribMulAction 📖	CompOp	—
hasSMul 📖	CompOp	1 math math: smul_apply'
instCoeFunCarrierObj'Forall 📖	CompOp	—
instCoeFunCarrierObjCoextendScalarsForall 📖	CompOp	—
isModule 📖	CompOp	2 math math: ModuleCat.RestrictionCoextensionAdj.unit'_app, map'_hom_apply_apply
map' 📖	CompOp	1 math math: map'_hom_apply_apply
mulAction 📖	CompOp	—
obj' 📖	CompOp	1 math math: map'_hom_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map'_hom_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike LinearMap.addCommGroup isModule ModuleCat.Hom.hom obj' map'	—	—
map_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.coextendScalars CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Functor.map	—	—
smul_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.coextendScalars SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
smul_apply' 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike hasSMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—

ModuleCat.ExtendRestrictScalarsAdj

Definitions

Name	Category	Theorems
counit 📖	CompOp	1 math math: counit_app
homEquiv 📖	CompOp	1 math math: homEquiv_symm_apply
unit 📖	CompOp	1 math math: unit_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counit_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.comp ModuleCat.restrictScalars ModuleCat.extendScalars CategoryTheory.Functor.id counit Counit.map	—	—
homEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom ModuleCat CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory CategoryTheory.Functor.obj ModuleCat.restrictScalars ModuleCat.extendScalars EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquiv HomEquiv.fromExtendScalars	—	—
unit_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp ModuleCat.extendScalars ModuleCat.restrictScalars unit Unit.map CategoryTheory.Functor.obj	—	—

ModuleCat.ExtendRestrictScalarsAdj.Counit

Definitions

Name	Category	Theorems
map 📖	CompOp	2 math math: map_hom_apply, ModuleCat.ExtendRestrictScalarsAdj.counit_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring TensorProduct CommRing.toCommSemiring ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule TensorProduct.addCommGroup TensorProduct.leftModule ModuleCat.instModuleCarrierObjRestrictScalars LinearMap.instFunLike ModuleCat.Hom.hom CategoryTheory.Functor.comp ModuleCat.extendScalars map CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TensorProduct.addCommMonoid TensorProduct.instModule TensorProduct.lift LinearMap.addCommMonoid LinearMap.module AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—

ModuleCat.ExtendRestrictScalarsAdj.HomEquiv

Definitions

Name	Category	Theorems
evalAt 📖	CompOp	2 math math: fromExtendScalars_hom_apply, evalAt_apply
fromExtendScalars 📖	CompOp	2 math math: fromExtendScalars_hom_apply, ModuleCat.ExtendRestrictScalarsAdj.homEquiv_symm_apply
toRestrictScalars 📖	CompOp	1 math math: toRestrictScalars_hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalAt_apply 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Module.compHom LinearMap.instFunLike evalAt CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ModuleCat.instModuleCarrierObjRestrictScalars CategoryTheory.ConcreteCategory.hom Ring.toSemiring ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—
fromExtendScalars_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring TensorProduct CommRing.toCommSemiring ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule TensorProduct.addCommGroup TensorProduct.leftModule ModuleCat.instModuleCarrierObjRestrictScalars LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.extendScalars fromExtendScalars CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule Module.compHom TensorProduct.lift LinearMap.addCommMonoid LinearMap.module AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup evalAt	—	—
toRestrictScalars_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule Module.compHom LinearMap.instFunLike ModuleCat.Hom.hom toRestrictScalars ModuleCat.extendScalars CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier TensorProduct.tmul CommRing.toCommSemiring ModuleCat.of Ring.toAddCommGroup Semiring.toModule CommSemiring.toSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—

ModuleCat.ExtendRestrictScalarsAdj.Unit

Definitions

Name	Category	Theorems
map 📖	CompOp	1 math math: ModuleCat.ExtendRestrictScalarsAdj.unit_app

ModuleCat.ExtendScalars

Definitions

Name	Category	Theorems
map' 📖	CompOp	2 math math: map'_id, map'_comp
obj' 📖	CompOp	3 math math: map'_id, map'_comp, ModuleCat.homEquiv_extendScalarsComp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_ext 📖	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.extendScalars ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier TensorProduct.tmul CommRing.toCommSemiring ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	CategoryTheory.Functor.map_injective ModuleCat.instFaithfulRestrictScalars ModuleCat.hom_ext TensorProduct.ext' Algebra.to_smulCommClass smul_tmul mul_one map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass
hom_ext_iff 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.extendScalars ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier TensorProduct.tmul CommRing.toCommSemiring ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	hom_ext
map'_comp 📖	mathematical	—	map' CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory obj'	—	ModuleCat.hom_ext LinearMap.ext TensorProduct.induction_on
map'_id 📖	mathematical	—	map' CategoryTheory.CategoryStruct.id ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory obj'	—	Algebra.to_smulCommClass LinearMap.baseChange_id
map_tmul 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.extendScalars ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Functor.map TensorProduct.tmul CommRing.toCommSemiring ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule Module.compHom CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—
smul_tmul 📖	mathematical	—	TensorProduct CommRing.toCommSemiring ModuleCat.carrier CommRing.toRing CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Module.compHom CommSemiring.toSemiring ModuleCat.isModule TensorProduct.leftHasSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ModuleCat.instModuleCarrierObjRestrictScalars TensorProduct.tmul NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—

ModuleCat.RestrictScalars

Definitions

Name	Category	Theorems
map' 📖	CompOp	—
obj' 📖	CompOp	1 math math: ModuleCat.sMulCommClass_mk

ModuleCat.RestrictionCoextensionAdj

Definitions

Name	Category	Theorems
app' 📖	CompOp	1 math math: unit'_app
counit' 📖	CompOp	1 math math: counit'_app
unit' 📖	CompOp	1 math math: unit'_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counit'_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.comp ModuleCat.coextendScalars ModuleCat.restrictScalars CategoryTheory.Functor.id counit' ModuleCat.ofHom ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat.isAddCommGroup Module.compHom Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule RingHom.id Semiring.toNonAssocSemiring AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddHom.toFun ModuleCat.of Ring.toAddCommGroup Semiring.toModule LinearMap.toAddHom AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
unit'_app 📖	mathematical	—	CategoryTheory.NatTrans.app ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp ModuleCat.restrictScalars ModuleCat.coextendScalars unit' ModuleCat.ofHom ModuleCat.carrier LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring CategoryTheory.Functor.obj ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.addCommGroup ModuleCat.CoextendScalars.isModule app'	—	—

ModuleCat.RestrictionCoextensionAdj.HomEquiv

Definitions

Name	Category	Theorems
fromRestriction 📖	CompOp	1 math math: fromRestriction_hom_apply_apply
toRestriction 📖	CompOp	1 math math: toRestriction_hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromRestriction_hom_apply_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars ModuleCat.of Ring.toAddCommGroup Semiring.toModule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.coextendScalars ModuleCat.Hom.hom fromRestriction CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
toRestriction_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom toRestriction ModuleCat.of Ring.toAddCommGroup Semiring.toModule ModuleCat.coextendScalars AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—

ModuleCat.restrictScalars

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Functor.map	—	—
smul_def 📖	mathematical	—	ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid ModuleCat.isModule DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	—
smul_def' 📖	mathematical	—	ModuleCat.carrier CategoryTheory.Functor.obj ModuleCat ModuleCat.moduleCategory ModuleCat.restrictScalars SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid ModuleCat.isModule DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	—

---

← Back to Index