Images

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

Statistics

Metric	Count
Definitions factorThruImage, image, ι, imageIsoRange, isImage, monoFactorisation	6
Theorems fac, lift_fac, imageIsoRange_hom_subtype, imageIsoRange_hom_subtype_apply, imageIsoRange_hom_subtype_assoc, imageIsoRange_inv_image_ι, imageIsoRange_inv_image_ι_apply, imageIsoRange_inv_image_ι_assoc, instMonoι	9
Total	15

ModuleCat

Definitions

Name	Category	Theorems
factorThruImage 📖	CompOp	1 math math: image.fac
image 📖	CompOp	3 math math: image.lift_fac, instMonoι, image.fac
imageIsoRange 📖	CompOp	6 math math: imageIsoRange_hom_subtype, imageIsoRange_inv_image_ι_apply, imageIsoRange_hom_subtype_assoc, imageIsoRange_inv_image_ι, imageIsoRange_inv_image_ι_assoc, imageIsoRange_hom_subtype_apply
isImage 📖	CompOp	—
monoFactorisation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
imageIsoRange_hom_subtype 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations abelian of carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule SetLike.instMembership Submodule.setLike LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Hom.hom Submodule.addCommGroup Submodule.module CategoryTheory.Iso.hom imageIsoRange ofHom Submodule.subtype CategoryTheory.Limits.image.ι	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations RingHomSurjective.ids imageIsoRange_inv_image_ι CategoryTheory.Iso.hom_inv_id_assoc
imageIsoRange_hom_subtype_apply 📖	mathematical	—	carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule SetLike.instMembership Submodule.setLike LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Hom.hom DFunLike.coe LinearMap CategoryTheory.Limits.image ModuleCat moduleCategory CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations abelian Submodule.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom instConcreteCategoryLinearMapIdCarrier of CategoryTheory.Iso.hom imageIsoRange CategoryTheory.Limits.image.ι	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations RingHomSurjective.ids CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise imageIsoRange_hom_subtype
imageIsoRange_hom_subtype_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations abelian of carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule SetLike.instMembership Submodule.setLike LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Hom.hom Submodule.addCommGroup Submodule.module CategoryTheory.Iso.hom imageIsoRange ofHom Submodule.subtype CategoryTheory.Limits.image.ι	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations RingHomSurjective.ids CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageIsoRange_hom_subtype
imageIsoRange_inv_image_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory of carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule SetLike.instMembership Submodule.setLike LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Hom.hom Submodule.addCommGroup Submodule.module CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations abelian CategoryTheory.Iso.inv imageIsoRange CategoryTheory.Limits.image.ι ofHom Submodule.subtype	—	CategoryTheory.Limits.IsImage.isoExt_inv_m
imageIsoRange_inv_image_ι_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier CategoryTheory.Limits.image ModuleCat moduleCategory CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations abelian AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom instConcreteCategoryLinearMapIdCarrier CategoryTheory.Limits.image.ι Submodule SetLike.instMembership Submodule.setLike LinearMap.range RingHomSurjective.ids Hom.hom Submodule.addCommGroup Submodule.module of CategoryTheory.Iso.inv imageIsoRange	—	RingHomSurjective.ids CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise imageIsoRange_inv_image_ι
imageIsoRange_inv_image_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory of carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule SetLike.instMembership Submodule.setLike LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Hom.hom Submodule.addCommGroup Submodule.module CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations abelian CategoryTheory.Iso.inv imageIsoRange CategoryTheory.Limits.image.ι ofHom Submodule.subtype	—	RingHomSurjective.ids CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageIsoRange_inv_image_ι
instMonoι 📖	mathematical	—	CategoryTheory.Mono ModuleCat moduleCategory image image.ι	—	CategoryTheory.ConcreteCategory.mono_of_injective Subtype.val_injective

ModuleCat.image

Definitions

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

Theorems

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

---

← Back to Index