Images

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

Statistics

Metric	Count
Definitions factorThruImage, image, ι, imageIsoRange, isImage, monoFactorisation	6
Theorems fac, lift_fac, instMonoι	3
Total	9

AddCommGrpCat

Definitions

Name	Category	Theorems
factorThruImage 📖	CompOp	1 math math: image.fac
image 📖	CompOp	3 math math: image.lift_fac, instMonoι, image.fac
imageIsoRange 📖	CompOp	—
isImage 📖	CompOp	—
monoFactorisation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMonoι 📖	mathematical	—	CategoryTheory.Mono AddCommGrpCat instCategory image image.ι	—	CategoryTheory.ConcreteCategory.mono_of_injective Subtype.val_injective

AddCommGrpCat.image

Definitions

Name	Category	Theorems
ι 📖	CompOp	3 math math: lift_fac, AddCommGrpCat.instMonoι, fac

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AddCommGrpCat CategoryTheory.Category.toCategoryStruct AddCommGrpCat.instCategory AddCommGrpCat.image AddCommGrpCat.factorThruImage ι	—	AddCommGrpCat.hom_ext AddMonoidHom.ext
lift_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AddCommGrpCat CategoryTheory.Category.toCategoryStruct AddCommGrpCat.instCategory AddCommGrpCat.image CategoryTheory.Limits.MonoFactorisation.I lift CategoryTheory.Limits.MonoFactorisation.m ι	—	AddCommGrpCat.hom_ext AddMonoidHom.ext CategoryTheory.Limits.MonoFactorisation.fac

---

← Back to Index