Theorems · Inductive type · category theory

CategoryTheory.Limits.ImageMap

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [CategoryTheory.Limits.HasImage f.hom] → [CategoryTheory.Limits.HasImage g.hom] → (f ⟶ g) → Type v

An image map is a morphism image f → image g fitting into a commutative square and satisfying the obvious commutativity conditions.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Images

Cited by

17 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasImageCategoryTheory.Limits.HasImage