Images

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Shapes/Images.lean

Statistics

Metric	Count
Definitions iso	1
Theorems factorThruImage_comp_hom, factorThruImage_comp_hom_assoc, hom_comp_map_image_ι, hom_comp_map_image_ι_assoc, inv_comp_image_ι_map, inv_comp_image_ι_map_assoc, iso_hom, iso_inv	8
Total	9

CategoryTheory.PreservesImage

Definitions

Name	Category	Theorems
iso 📖	CompOp	8 math math: factorThruImage_comp_hom, factorThruImage_comp_hom_assoc, iso_hom, hom_comp_map_image_ι, inv_comp_image_ι_map, hom_comp_map_image_ι_assoc, iso_inv, inv_comp_image_ι_map_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorThruImage_comp_hom 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.image CategoryTheory.Functor.map CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.factorThruImage CategoryTheory.Iso.hom iso	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.image.fac_lift
factorThruImage_comp_hom_assoc 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.image CategoryTheory.Functor.map CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.factorThruImage CategoryTheory.Iso.hom iso	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' factorThruImage_comp_hom
hom_comp_map_image_ι 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Limits.HasImages.has_image CategoryTheory.Iso.hom iso CategoryTheory.Limits.image.ι	—	CategoryTheory.Limits.HasImages.has_image iso_hom CategoryTheory.Limits.image.lift_fac
hom_comp_map_image_ι_assoc 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Limits.HasImages.has_image CategoryTheory.Iso.hom iso CategoryTheory.Limits.image.ι	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_comp_map_image_ι
inv_comp_image_ι_map 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Functor.map CategoryTheory.Iso.inv iso CategoryTheory.Limits.image.ι	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.IsImage.lift_ι
inv_comp_image_ι_map_assoc 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Functor.map CategoryTheory.Iso.inv iso CategoryTheory.Limits.image.ι	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inv_comp_image_ι_map
iso_hom 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	CategoryTheory.Iso.hom CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Limits.HasImages.has_image iso CategoryTheory.Limits.image.lift CategoryTheory.Limits.image.ι CategoryTheory.Limits.factorThruImage	—	CategoryTheory.Limits.HasImages.has_image
iso_inv 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PreservesColimit CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.span	CategoryTheory.Iso.inv CategoryTheory.Limits.image CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Limits.HasImages.has_image iso CategoryTheory.Limits.IsImage.lift CategoryTheory.Limits.image.ι CategoryTheory.Limits.factorThruImage CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage CategoryTheory.Limits.Image.monoFactorisation	—	CategoryTheory.Limits.HasImages.has_image

---

← Back to Index