Documentation

Mathlib.CategoryTheory.Limits.Shapes.Images

Categorical images #

We define the categorical image of f as a factorisation f = em through a monomorphism m, so that m factors through the m' in any other such factorisation.

Main definitions #

Main statements #

Future work #

structure CategoryTheory.Limits.MonoFactorisation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :
Type (max u v)

A factorisation of a morphism f = em, with m monic.

  • I : C

    A factorisation of a morphism f = em, with m monic.

  • m : self.I Y

    A factorisation of a morphism f = em, with m monic.

  • m_mono : CategoryTheory.Mono self.m

    A factorisation of a morphism f = em, with m monic.

  • e : X self.I

    A factorisation of a morphism f = em, with m monic.

  • A factorisation of a morphism f = em, with m monic.

Instances For

A factorisation of a morphism f = em, with m monic.

@[simp]

A factorisation of a morphism f = em, with m monic.

The morphism m in a factorisation f = em through a monomorphism is uniquely determined.

@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.compMono_e {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (F : CategoryTheory.Limits.MonoFactorisation f) {Y' : C} (g : Y Y') [CategoryTheory.Mono g] :
(F.compMono g).e = F.e
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.compMono_I {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (F : CategoryTheory.Limits.MonoFactorisation f) {Y' : C} (g : Y Y') [CategoryTheory.Mono g] :
(F.compMono g).I = F.I

Any mono factorisation of f gives a mono factorisation of f ≫ g when g is a mono.

Equations

A mono factorisation of f ≫ g, where g is an isomorphism, gives a mono factorisation of f.

Equations
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.isoComp_I {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (F : CategoryTheory.Limits.MonoFactorisation f) {X' : C} (g : X' X) :
(F.isoComp g).I = F.I
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.isoComp_m {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {f : X Y} (F : CategoryTheory.Limits.MonoFactorisation f) {X' : C} (g : X' X) :
(F.isoComp g).m = F.m

Any mono factorisation of f gives a mono factorisation of g ≫ f.

Equations

Data exhibiting that a given factorisation through a mono is initial.

Instances For
@[simp]

Data exhibiting that a given factorisation through a mono is initial.

The trivial factorisation of a monomorphism satisfies the universal property.

Equations

Two factorisations through monomorphisms satisfying the universal property must factor through isomorphic objects.

Equations
  • hF.isoExt hF' = { hom := hF.lift F', inv := hF'.lift F, hom_inv_id := , inv_hom_id := }

If f and g are isomorphic arrows, then a mono factorisation of f that is an image gives a mono factorisation of g that is an image

Equations
structure CategoryTheory.Limits.ImageFactorisation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :
Type (max u v)

Data exhibiting that a morphism f has an image.

Instances For

If f and g are isomorphic arrows, then an image factorisation of f gives an image factorisation of g

Equations
  • F.ofArrowIso sq = { F := F.F.ofArrowIso sq, isImage := F.isImage.ofArrowIso sq }

has_image f means that there exists an image factorisation of f.

@[instance 100]
Equations
  • =

The witness of the universal property for the chosen factorisation of f through a monomorphism.

Equations

Any other factorisation of the morphism f through a monomorphism receives a map from the image.

Equations
Instances For

If has_image g, then has_image (f ≫ g) when f is an isomorphism.

Equations
  • =

HasImages asserts that every morphism has an image.

An equation between morphisms gives a comparison map between the images (which momentarily we prove is an iso).

Equations
  • One or more equations did not get rendered due to their size.
Instances For

image.preComp f g is an epimorphism when f is an epimorphism (we need C to have equalizers to prove this).

Equations
  • =

image.preComp f g is an isomorphism when f is an isomorphism (we need C to have equalizers to prove this).

Equations
  • =

Postcomposing by an isomorphism induces an isomorphism on the image.

Equations
  • One or more equations did not get rendered due to their size.

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

Instances For
@[simp]

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

To give an image map for a commutative square with f at the top and g at the bottom, it suffices to give a map between any mono factorisation of f and any image factorisation of g.

Equations
  • One or more equations did not get rendered due to their size.
theorem CategoryTheory.Limits.ImageMap.ext {C : Type u} :
∀ {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C} {inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f g} {x y : CategoryTheory.Limits.ImageMap sq}, x.map = y.mapx = y

The identity image f ⟶ image f fits into the commutative square represented by the identity morphism 𝟙 f in the arrow category.

Equations

The functor from the arrow category of C to C itself that maps a morphism to its image and a commutative square to the induced morphism on images.

Equations
  • One or more equations did not get rendered due to their size.

A strong epi-mono factorisation is a decomposition f = em with e a strong epimorphism and m a monomorphism.

Instances For

A strong epi-mono factorisation is a decomposition f = em with e a strong epimorphism and m a monomorphism.

Satisfying the inhabited linter

Equations
  • One or more equations did not get rendered due to their size.

A mono factorisation coming from a strong epi-mono factorisation always has the universal property of the image.

Equations

A category has strong epi-mono factorisations if every morphism admits a strong epi-mono factorisation.

Instances

A category has strong epi-mono factorisations if every morphism admits a strong epi-mono factorisation.

If there is a single strong epi-mono factorisation of f, then every image factorisation is a strong epi-mono factorisation.

@[instance 100]

If we constructed our images from strong epi-mono factorisations, then these images are strong epi images.

Equations
  • =
@[instance 100]

If a category has images, equalizers and pullbacks, then images are automatically strong epi images.

Equations
  • =

If C has strong epi mono factorisations, then the image is unique up to isomorphism, in that if f factors as a strong epi followed by a mono, this factorisation is essentially the image factorisation.

Equations
  • One or more equations did not get rendered due to their size.

A category with strong epi mono factorisations admits functorial epi/mono factorizations.

Equations
  • One or more equations did not get rendered due to their size.