Injective

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

Statistics

Metric	Count
Definitions	0
Theorems injective_iff_injective_object, injective_module_of_injective_object, injective_object_of_injective_module, ulift_injective_of_injective	4
Total	4

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_iff_injective_object 📖	mathematical	—	Injective CategoryTheory.Injective ModuleCat ModuleCat.moduleCategory ModuleCat.of	—	injective_object_of_injective_module injective_module_of_injective_object
injective_module_of_injective_object 📖	mathematical	—	Injective	—	ModuleCat.mono_iff_injective CategoryTheory.Injective.factors ModuleCat.hom_ext_iff
injective_object_of_injective_module 📖	mathematical	—	CategoryTheory.Injective ModuleCat ModuleCat.moduleCategory ModuleCat.of	—	Injective.out ModuleCat.mono_iff_injective ModuleCat.hom_ext LinearMap.ext

ModuleCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ulift_injective_of_injective 📖	mathematical	—	CategoryTheory.Injective ModuleCat moduleCategory of ULift.addCommGroup ULift.module' Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Module.injective_object_of_injective_module Module.ulift_injective_of_injective Module.injective_module_of_injective_object

---

← Back to Index