ZModuleEquivalence

📁 Source: Mathlib/Algebra/Category/Grp/ZModuleEquivalence.lean

Statistics

Metric	Count
Definitions	0
Theorems forget₂AddCommGroupIsEquivalence, forget₂_addCommGroup_full, forget₂_addCommGrp_essSurj	3
Total	3

ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget₂AddCommGroupIsEquivalence 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence ModuleCat Int.instRing moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	CategoryTheory.forget₂_faithful forget₂_addCommGroup_full forget₂_addCommGrp_essSurj
forget₂_addCommGroup_full 📖	mathematical	—	CategoryTheory.Functor.Full ModuleCat Int.instRing moduleCategory AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass SMul.ext int_smul_eq_zsmul AddMonoidHom.map_zsmul
forget₂_addCommGrp_essSurj 📖	mathematical	—	CategoryTheory.Functor.EssSurj ModuleCat Int.instRing AddCommGrpCat moduleCategory AddCommGrpCat.instCategory CategoryTheory.forget₂ LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier AddMonoidHom AddCommGrpCat.carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommGrpCat.str AddMonoidHom.instFunLike AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier hasForgetToAddCommGroup	—	—

---

← Back to Index