category_theory.limits.shapes.images

source

structure category_theory.limits.mono_factorisation {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :

Type (max u v)

I : C
m : self.I ⟶ Y
m_mono : category_theory.mono self.m
e : X ⟶ self.I
fac' : self.e ≫ self.m = f . "obviously"

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

Instances for category_theory.limits.mono_factorisation

category_theory.limits.mono_factorisation.has_sizeof_inst
category_theory.limits.mono_factorisation.inhabited

source

@[simp]

theorem category_theory.limits.mono_factorisation.fac {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (self : category_theory.limits.mono_factorisation f) :

self.e ≫ self.m = f

source

@[simp]

theorem category_theory.limits.mono_factorisation.fac_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (self : category_theory.limits.mono_factorisation f) {X' : C} (f' : Y ⟶ X') :

self.e ≫ self.m ≫ f' = f ≫ f'

source

def category_theory.limits.mono_factorisation.self {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

category_theory.limits.mono_factorisation f

The obvious factorisation of a monomorphism through itself.

Equations

category_theory.limits.mono_factorisation.self f = {I := X, m := f, m_mono := _inst_2, e := 𝟙 X, fac' := _}

source

@[protected, instance]

def category_theory.limits.mono_factorisation.inhabited {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

inhabited (category_theory.limits.mono_factorisation f)

Equations

category_theory.limits.mono_factorisation.inhabited f = {default := category_theory.limits.mono_factorisation.self f _inst_2}

source

@[ext]

theorem category_theory.limits.mono_factorisation.ext {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hI : F.I = F'.I) (hm : F.m = category_theory.eq_to_hom hI ≫ F'.m) :

F = F'

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

source

@[simp]

theorem category_theory.limits.mono_factorisation.comp_mono_I {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.mono_factorisation f) {Y' : C} (g : Y ⟶ Y') [category_theory.mono g] :

(F.comp_mono g).I = F.I

source

def category_theory.limits.mono_factorisation.comp_mono {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.mono_factorisation f) {Y' : C} (g : Y ⟶ Y') [category_theory.mono g] :

category_theory.limits.mono_factorisation (f ≫ g)

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

Equations

F.comp_mono g = {I := F.I, m := F.m ≫ g, m_mono := _, e := F.e, fac' := _}

source

@[simp]

theorem category_theory.limits.mono_factorisation.comp_mono_e {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.mono_factorisation f) {Y' : C} (g : Y ⟶ Y') [category_theory.mono g] :

(F.comp_mono g).e = F.e

source

@[simp]

theorem category_theory.limits.mono_factorisation.comp_mono_m {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.mono_factorisation f) {Y' : C} (g : Y ⟶ Y') [category_theory.mono g] :

(F.comp_mono g).m = F.m ≫ g

source

@[simp]

theorem category_theory.limits.mono_factorisation.of_comp_iso_e {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [category_theory.is_iso g] (F : category_theory.limits.mono_factorisation (f ≫ g)) :

F.of_comp_iso.e = F.e

source

noncomputable def category_theory.limits.mono_factorisation.of_comp_iso {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [category_theory.is_iso g] (F : category_theory.limits.mono_factorisation (f ≫ g)) :

category_theory.limits.mono_factorisation f

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

Equations

F.of_comp_iso = {I := F.I, m := F.m ≫ category_theory.inv g, m_mono := _, e := F.e, fac' := _}

source

@[simp]

theorem category_theory.limits.mono_factorisation.of_comp_iso_m {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [category_theory.is_iso g] (F : category_theory.limits.mono_factorisation (f ≫ g)) :

F.of_comp_iso.m = F.m ≫ category_theory.inv g

source

@[simp]

theorem category_theory.limits.mono_factorisation.of_comp_iso_I {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'} [category_theory.is_iso g] (F : category_theory.limits.mono_factorisation (f ≫ g)) :

F.of_comp_iso.I = F.I

source

@[simp]

theorem category_theory.limits.mono_factorisation.iso_comp_I {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.mono_factorisation f) {X' : C} (g : X' ⟶ X) :

(F.iso_comp g).I = F.I

source

@[simp]

theorem category_theory.limits.mono_factorisation.iso_comp_m {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.mono_factorisation f) {X' : C} (g : X' ⟶ X) :

(F.iso_comp g).m = F.m

source

def category_theory.limits.mono_factorisation.iso_comp {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.mono_factorisation f) {X' : C} (g : X' ⟶ X) :

category_theory.limits.mono_factorisation (g ≫ f)

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

Equations

F.iso_comp g = {I := F.I, m := F.m, m_mono := _, e := g ≫ F.e, fac' := _}

source

@[simp]

theorem category_theory.limits.mono_factorisation.iso_comp_e {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.mono_factorisation f) {X' : C} (g : X' ⟶ X) :

(F.iso_comp g).e = g ≫ F.e

source

@[simp]

theorem category_theory.limits.mono_factorisation.of_iso_comp_m {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [category_theory.is_iso g] (F : category_theory.limits.mono_factorisation (g ≫ f)) :

(category_theory.limits.mono_factorisation.of_iso_comp g F).m = F.m

source

noncomputable def category_theory.limits.mono_factorisation.of_iso_comp {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [category_theory.is_iso g] (F : category_theory.limits.mono_factorisation (g ≫ f)) :

category_theory.limits.mono_factorisation f

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

Equations

category_theory.limits.mono_factorisation.of_iso_comp g F = {I := F.I, m := F.m, m_mono := _, e := category_theory.inv g ≫ F.e, fac' := _}

source

@[simp]

theorem category_theory.limits.mono_factorisation.of_iso_comp_I {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [category_theory.is_iso g] (F : category_theory.limits.mono_factorisation (g ≫ f)) :

(category_theory.limits.mono_factorisation.of_iso_comp g F).I = F.I

source

@[simp]

theorem category_theory.limits.mono_factorisation.of_iso_comp_e {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X) [category_theory.is_iso g] (F : category_theory.limits.mono_factorisation (g ≫ f)) :

(category_theory.limits.mono_factorisation.of_iso_comp g F).e = category_theory.inv g ≫ F.e

source

@[simp]

theorem category_theory.limits.mono_factorisation.of_arrow_iso_e {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} (F : category_theory.limits.mono_factorisation f.hom) (sq : f ⟶ g) [category_theory.is_iso sq] :

(F.of_arrow_iso sq).e = category_theory.inv sq.left ≫ F.e

source

noncomputable def category_theory.limits.mono_factorisation.of_arrow_iso {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} (F : category_theory.limits.mono_factorisation f.hom) (sq : f ⟶ g) [category_theory.is_iso sq] :

category_theory.limits.mono_factorisation g.hom

If f and g are isomorphic arrows, then a mono factorisation of f gives a mono factorisation of g

Equations

F.of_arrow_iso sq = {I := F.I, m := F.m ≫ sq.right, m_mono := _, e := category_theory.inv sq.left ≫ F.e, fac' := _}

source

@[simp]

theorem category_theory.limits.mono_factorisation.of_arrow_iso_I {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} (F : category_theory.limits.mono_factorisation f.hom) (sq : f ⟶ g) [category_theory.is_iso sq] :

(F.of_arrow_iso sq).I = F.I

source

@[simp]

theorem category_theory.limits.mono_factorisation.of_arrow_iso_m {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} (F : category_theory.limits.mono_factorisation f.hom) (sq : f ⟶ g) [category_theory.is_iso sq] :

(F.of_arrow_iso sq).m = F.m ≫ sq.right

source

structure category_theory.limits.is_image {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.mono_factorisation f) :

Type (max u v)

lift : Π (F' : category_theory.limits.mono_factorisation f), F.I ⟶ F'.I
lift_fac' : (∀ (F' : category_theory.limits.mono_factorisation f), self.lift F' ≫ F'.m = F.m) . "obviously"

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

Instances for category_theory.limits.is_image

category_theory.limits.is_image.has_sizeof_inst
category_theory.limits.is_image.inhabited

source

@[simp]

theorem category_theory.limits.is_image.lift_fac {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F : category_theory.limits.mono_factorisation f} (self : category_theory.limits.is_image F) (F' : category_theory.limits.mono_factorisation f) :

self.lift F' ≫ F'.m = F.m

source

@[simp]

theorem category_theory.limits.is_image.lift_fac_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F : category_theory.limits.mono_factorisation f} (self : category_theory.limits.is_image F) (F' : category_theory.limits.mono_factorisation f) {X' : C} (f' : Y ⟶ X') :

self.lift F' ≫ F'.m ≫ f' = F.m ≫ f'

source

@[simp]

theorem category_theory.limits.is_image.fac_lift {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (F' : category_theory.limits.mono_factorisation f) :

F.e ≫ hF.lift F' = F'.e

source

@[simp]

theorem category_theory.limits.is_image.fac_lift_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (F' : category_theory.limits.mono_factorisation f) {X' : C} (f' : F'.I ⟶ X') :

F.e ≫ hF.lift F' ≫ f' = F'.e ≫ f'

source

@[simp]

theorem category_theory.limits.is_image.self_lift {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] (F' : category_theory.limits.mono_factorisation f) :

(category_theory.limits.is_image.self f).lift F' = F'.e

source

def category_theory.limits.is_image.self {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

category_theory.limits.is_image (category_theory.limits.mono_factorisation.self f)

The trivial factorisation of a monomorphism satisfies the universal property.

Equations

category_theory.limits.is_image.self f = {lift := λ (F' : category_theory.limits.mono_factorisation f), F'.e, lift_fac' := _}

source

@[protected, instance]

def category_theory.limits.is_image.inhabited {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

inhabited (category_theory.limits.is_image (category_theory.limits.mono_factorisation.self f))

Equations

category_theory.limits.is_image.inhabited f = {default := category_theory.limits.is_image.self f _inst_2}

source

def category_theory.limits.is_image.iso_ext {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (hF' : category_theory.limits.is_image F') :

F.I ≅ F'.I

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

Equations

hF.iso_ext hF' = {hom := hF.lift F', inv := hF'.lift F, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.limits.is_image.iso_ext_hom {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (hF' : category_theory.limits.is_image F') :

(hF.iso_ext hF').hom = hF.lift F'

source

@[simp]

theorem category_theory.limits.is_image.iso_ext_inv {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (hF' : category_theory.limits.is_image F') :

(hF.iso_ext hF').inv = hF'.lift F

source

theorem category_theory.limits.is_image.iso_ext_hom_m {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (hF' : category_theory.limits.is_image F') :

(hF.iso_ext hF').hom ≫ F'.m = F.m

source

theorem category_theory.limits.is_image.iso_ext_inv_m {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (hF' : category_theory.limits.is_image F') :

(hF.iso_ext hF').inv ≫ F.m = F'.m

source

theorem category_theory.limits.is_image.e_iso_ext_hom {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (hF' : category_theory.limits.is_image F') :

F.e ≫ (hF.iso_ext hF').hom = F'.e

source

theorem category_theory.limits.is_image.e_iso_ext_inv {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} {F F' : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) (hF' : category_theory.limits.is_image F') :

F'.e ≫ (hF.iso_ext hF').inv = F.e

source

@[simp]

theorem category_theory.limits.is_image.of_arrow_iso_lift {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} {F : category_theory.limits.mono_factorisation f.hom} (hF : category_theory.limits.is_image F) (sq : f ⟶ g) [category_theory.is_iso sq] (F' : category_theory.limits.mono_factorisation g.hom) :

(hF.of_arrow_iso sq).lift F' = hF.lift (F'.of_arrow_iso (category_theory.inv sq))

source

noncomputable def category_theory.limits.is_image.of_arrow_iso {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} {F : category_theory.limits.mono_factorisation f.hom} (hF : category_theory.limits.is_image F) (sq : f ⟶ g) [category_theory.is_iso sq] :

category_theory.limits.is_image (F.of_arrow_iso sq)

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

hF.of_arrow_iso sq = {lift := λ (F' : category_theory.limits.mono_factorisation g.hom), hF.lift (F'.of_arrow_iso (category_theory.inv sq)), lift_fac' := _}

source

structure category_theory.limits.image_factorisation {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :

Type (max u v)

F : category_theory.limits.mono_factorisation f
is_image : category_theory.limits.is_image self.F

Data exhibiting that a morphism f has an image.

Instances for category_theory.limits.image_factorisation

category_theory.limits.image_factorisation.has_sizeof_inst
category_theory.limits.image_factorisation.inhabited

source

@[protected, instance]

def category_theory.limits.image_factorisation.inhabited {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

inhabited (category_theory.limits.image_factorisation f)

Equations

category_theory.limits.image_factorisation.inhabited f = {default := {F := category_theory.limits.mono_factorisation.self f _inst_2, is_image := category_theory.limits.is_image.self f _inst_2}}

source

@[simp]

theorem category_theory.limits.image_factorisation.of_arrow_iso_is_image {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} (F : category_theory.limits.image_factorisation f.hom) (sq : f ⟶ g) [category_theory.is_iso sq] :

(F.of_arrow_iso sq).is_image = F.is_image.of_arrow_iso sq

source

noncomputable def category_theory.limits.image_factorisation.of_arrow_iso {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} (F : category_theory.limits.image_factorisation f.hom) (sq : f ⟶ g) [category_theory.is_iso sq] :

category_theory.limits.image_factorisation g.hom

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

Equations

F.of_arrow_iso sq = {F := F.F.of_arrow_iso sq _inst_2, is_image := F.is_image.of_arrow_iso sq _inst_2}

source

@[simp]

theorem category_theory.limits.image_factorisation.of_arrow_iso_F {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} (F : category_theory.limits.image_factorisation f.hom) (sq : f ⟶ g) [category_theory.is_iso sq] :

(F.of_arrow_iso sq).F = F.F.of_arrow_iso sq

source

@[class]

structure category_theory.limits.has_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :

Prop

exists_image : nonempty (category_theory.limits.image_factorisation f)

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

Instances of this typeclass

source

theorem category_theory.limits.has_image.mk {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.image_factorisation f) :

category_theory.limits.has_image f

source

theorem category_theory.limits.has_image.of_arrow_iso {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [h : category_theory.limits.has_image f.hom] (sq : f ⟶ g) [category_theory.is_iso sq] :

category_theory.limits.has_image g.hom

source

@[protected, instance]

def category_theory.limits.mono_has_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

category_theory.limits.has_image f

source

noncomputable def category_theory.limits.image.mono_factorisation {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.mono_factorisation f

Some factorisation of f through a monomorphism (selected with choice).

Equations

category_theory.limits.image.mono_factorisation f = (classical.choice category_theory.limits.has_image.exists_image).F

source

noncomputable def category_theory.limits.image.is_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.is_image (category_theory.limits.image.mono_factorisation f)

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

Equations

category_theory.limits.image.is_image f = (classical.choice category_theory.limits.has_image.exists_image).is_image

source

noncomputable def category_theory.limits.image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

C

The categorical image of a morphism.

Equations

category_theory.limits.image f = (category_theory.limits.image.mono_factorisation f).I

source

noncomputable def category_theory.limits.image.ι {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.image f ⟶ Y

The inclusion of the image of a morphism into the target.

Equations

category_theory.limits.image.ι f = (category_theory.limits.image.mono_factorisation f).m

Instances for category_theory.limits.image.ι

category_theory.limits.image.ι.category_theory.mono

source

@[simp]

theorem category_theory.limits.image.as_ι {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

(category_theory.limits.image.mono_factorisation f).m = category_theory.limits.image.ι f

source

@[protected, instance]

def category_theory.limits.image.ι.category_theory.mono {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.mono (category_theory.limits.image.ι f)

source

noncomputable def category_theory.limits.factor_thru_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

X ⟶ category_theory.limits.image f

The map from the source to the image of a morphism.

Equations

category_theory.limits.factor_thru_image f = (category_theory.limits.image.mono_factorisation f).e

Instances for category_theory.limits.factor_thru_image

source

@[simp]

theorem category_theory.limits.as_factor_thru_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

(category_theory.limits.image.mono_factorisation f).e = category_theory.limits.factor_thru_image f

Rewrite in terms of the factor_thru_image interface.

source

@[simp]

theorem category_theory.limits.image.fac {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.factor_thru_image f ≫ category_theory.limits.image.ι f = f

source

@[simp]

theorem category_theory.limits.image.fac_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] {X' : C} (f' : Y ⟶ X') :

category_theory.limits.factor_thru_image f ≫ category_theory.limits.image.ι f ≫ f' = f ≫ f'

source

noncomputable def category_theory.limits.image.lift {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) :

category_theory.limits.image f ⟶ F'.I

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

Equations

category_theory.limits.image.lift F' = (category_theory.limits.image.is_image f).lift F'

Instances for category_theory.limits.image.lift

category_theory.limits.image.lift_mono

source

@[simp]

theorem category_theory.limits.image.lift_fac_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) {X' : C} (f' : Y ⟶ X') :

category_theory.limits.image.lift F' ≫ F'.m ≫ f' = category_theory.limits.image.ι f ≫ f'

source

@[simp]

theorem category_theory.limits.image.lift_fac {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) :

category_theory.limits.image.lift F' ≫ F'.m = category_theory.limits.image.ι f

source

@[simp]

theorem category_theory.limits.image.fac_lift_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) {X' : C} (f' : F'.I ⟶ X') :

category_theory.limits.factor_thru_image f ≫ category_theory.limits.image.lift F' ≫ f' = F'.e ≫ f'

source

@[simp]

theorem category_theory.limits.image.fac_lift {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) :

category_theory.limits.factor_thru_image f ≫ category_theory.limits.image.lift F' = F'.e

source

@[simp]

theorem category_theory.limits.image.is_image_lift {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F : category_theory.limits.mono_factorisation f) :

(category_theory.limits.image.is_image f).lift F = category_theory.limits.image.lift F

source

@[simp]

theorem category_theory.limits.is_image.lift_ι {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] {F : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) :

hF.lift (category_theory.limits.image.mono_factorisation f) ≫ category_theory.limits.image.ι f = F.m

source

@[simp]

theorem category_theory.limits.is_image.lift_ι_assoc {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] {F : category_theory.limits.mono_factorisation f} (hF : category_theory.limits.is_image F) {X' : C} (f' : Y ⟶ X') :

hF.lift (category_theory.limits.image.mono_factorisation f) ≫ category_theory.limits.image.ι f ≫ f' = F.m ≫ f'

source

@[protected, instance]

def category_theory.limits.image.lift_mono {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) :

category_theory.mono (category_theory.limits.image.lift F')

source

theorem category_theory.limits.has_image.uniq {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F' : category_theory.limits.mono_factorisation f) (l : category_theory.limits.image f ⟶ F'.I) (w : l ≫ F'.m = category_theory.limits.image.ι f) :

l = category_theory.limits.image.lift F'

source

@[protected, instance]

def category_theory.limits.category_theory.category_struct.comp.has_image {C : Type u} [category_theory.category C] {X Y Z : C} (f : X ⟶ Y) [category_theory.is_iso f] (g : Y ⟶ Z) [category_theory.limits.has_image g] :

category_theory.limits.has_image (f ≫ g)

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

source

@[class]

structure category_theory.limits.has_images (C : Type u) [category_theory.category C] :

Prop

has_image : ∀ {X Y : C} (f : X ⟶ Y), category_theory.limits.has_image f

has_images asserts that every morphism has an image.

Instances of this typeclass

category_theory.limits.has_images_of_has_strong_epi_mono_factorisations

source

noncomputable def category_theory.limits.image_mono_iso_source {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

category_theory.limits.image f ≅ X

The image of a monomorphism is isomorphic to the source.

Equations

category_theory.limits.image_mono_iso_source f = (category_theory.limits.image.is_image f).iso_ext (category_theory.limits.is_image.self f)

source

@[simp]

theorem category_theory.limits.image_mono_iso_source_inv_ι_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] {X' : C} (f' : Y ⟶ X') :

(category_theory.limits.image_mono_iso_source f).inv ≫ category_theory.limits.image.ι f ≫ f' = f ≫ f'

source

@[simp]

theorem category_theory.limits.image_mono_iso_source_inv_ι {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

(category_theory.limits.image_mono_iso_source f).inv ≫ category_theory.limits.image.ι f = f

source

@[simp]

theorem category_theory.limits.image_mono_iso_source_hom_self {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] :

(category_theory.limits.image_mono_iso_source f).hom ≫ f = category_theory.limits.image.ι f

source

@[simp]

theorem category_theory.limits.image_mono_iso_source_hom_self_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.mono f] {X' : C} (f' : Y ⟶ X') :

(category_theory.limits.image_mono_iso_source f).hom ≫ f ≫ f' = category_theory.limits.image.ι f ≫ f'

source

@[ext]

theorem category_theory.limits.image.ext {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] {W : C} {g h : category_theory.limits.image f ⟶ W} [category_theory.limits.has_limit (category_theory.limits.parallel_pair g h)] (w : category_theory.limits.factor_thru_image f ≫ g = category_theory.limits.factor_thru_image f ≫ h) :

g = h

source

@[protected, instance]

def category_theory.limits.factor_thru_image.category_theory.epi {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [∀ {Z : C} (g h : category_theory.limits.image f ⟶ Z), category_theory.limits.has_limit (category_theory.limits.parallel_pair g h)] :

category_theory.epi (category_theory.limits.factor_thru_image f)

source

theorem category_theory.limits.epi_image_of_epi {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [E : category_theory.epi f] :

category_theory.epi (category_theory.limits.image.ι f)

source

theorem category_theory.limits.epi_of_epi_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] [category_theory.epi (category_theory.limits.image.ι f)] [category_theory.epi (category_theory.limits.factor_thru_image f)] :

category_theory.epi f

source

noncomputable def category_theory.limits.image.eq_to_hom {C : Type u} [category_theory.category C] {X Y : C} {f f' : X ⟶ Y} [category_theory.limits.has_image f] [category_theory.limits.has_image f'] (h : f = f') :

category_theory.limits.image f ⟶ category_theory.limits.image f'

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

Equations

category_theory.limits.image.eq_to_hom h = category_theory.limits.image.lift {I := category_theory.limits.image f' _inst_3, m := category_theory.limits.image.ι f' _inst_3, m_mono := _, e := category_theory.limits.factor_thru_image f' _inst_3, fac' := _}

Instances for category_theory.limits.image.eq_to_hom

category_theory.limits.image.eq_to_hom.category_theory.is_iso

source

@[protected, instance]

def category_theory.limits.image.eq_to_hom.category_theory.is_iso {C : Type u} [category_theory.category C] {X Y : C} {f f' : X ⟶ Y} [category_theory.limits.has_image f] [category_theory.limits.has_image f'] (h : f = f') :

category_theory.is_iso (category_theory.limits.image.eq_to_hom h)

source

noncomputable def category_theory.limits.image.eq_to_iso {C : Type u} [category_theory.category C] {X Y : C} {f f' : X ⟶ Y} [category_theory.limits.has_image f] [category_theory.limits.has_image f'] (h : f = f') :

category_theory.limits.image f ≅ category_theory.limits.image f'

An equation between morphisms gives an isomorphism between the images.

Equations

category_theory.limits.image.eq_to_iso h = category_theory.as_iso (category_theory.limits.image.eq_to_hom h)

source

theorem category_theory.limits.image.eq_fac {C : Type u} [category_theory.category C] {X Y : C} {f f' : X ⟶ Y} [category_theory.limits.has_image f] [category_theory.limits.has_image f'] [category_theory.limits.has_equalizers C] (h : f = f') :

category_theory.limits.image.ι f = (category_theory.limits.image.eq_to_iso h).hom ≫ category_theory.limits.image.ι f'

As long as the category has equalizers, the image inclusion maps commute with image.eq_to_iso.

source

noncomputable def category_theory.limits.image.pre_comp {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_image g] [category_theory.limits.has_image (f ≫ g)] :

category_theory.limits.image (f ≫ g) ⟶ category_theory.limits.image g

The comparison map image (f ≫ g) ⟶ image g.

Equations

category_theory.limits.image.pre_comp f g = category_theory.limits.image.lift {I := category_theory.limits.image g _inst_2, m := category_theory.limits.image.ι g _inst_2, m_mono := _, e := f ≫ category_theory.limits.factor_thru_image g, fac' := _}

Instances for category_theory.limits.image.pre_comp

source

@[simp]

theorem category_theory.limits.image.pre_comp_ι {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_image g] [category_theory.limits.has_image (f ≫ g)] :

category_theory.limits.image.pre_comp f g ≫ category_theory.limits.image.ι g = category_theory.limits.image.ι (f ≫ g)

source

@[simp]

theorem category_theory.limits.image.pre_comp_ι_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_image g] [category_theory.limits.has_image (f ≫ g)] {X' : C} (f' : Z ⟶ X') :

category_theory.limits.image.pre_comp f g ≫ category_theory.limits.image.ι g ≫ f' = category_theory.limits.image.ι (f ≫ g) ≫ f'

source

@[simp]

theorem category_theory.limits.image.factor_thru_image_pre_comp_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_image g] [category_theory.limits.has_image (f ≫ g)] {X' : C} (f' : category_theory.limits.image g ⟶ X') :

category_theory.limits.factor_thru_image (f ≫ g) ≫ category_theory.limits.image.pre_comp f g ≫ f' = f ≫ category_theory.limits.factor_thru_image g ≫ f'

source

@[simp]

theorem category_theory.limits.image.factor_thru_image_pre_comp {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_image g] [category_theory.limits.has_image (f ≫ g)] :

category_theory.limits.factor_thru_image (f ≫ g) ≫ category_theory.limits.image.pre_comp f g = f ≫ category_theory.limits.factor_thru_image g

source

@[protected, instance]

def category_theory.limits.image.pre_comp_mono {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_image g] [category_theory.limits.has_image (f ≫ g)] :

category_theory.mono (category_theory.limits.image.pre_comp f g)

image.pre_comp f g is a monomorphism.

source

theorem category_theory.limits.image.pre_comp_comp {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) {W : C} (h : Z ⟶ W) [category_theory.limits.has_image (g ≫ h)] [category_theory.limits.has_image (f ≫ g ≫ h)] [category_theory.limits.has_image h] [category_theory.limits.has_image ((f ≫ g) ≫ h)] :

category_theory.limits.image.pre_comp f (g ≫ h) ≫ category_theory.limits.image.pre_comp g h = category_theory.limits.image.eq_to_hom _ ≫ category_theory.limits.image.pre_comp (f ≫ g) h

The two step comparison map image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h agrees with the one step comparison map image (f ≫ (g ≫ h)) ≅ image ((f ≫ g) ≫ h) ⟶ image h.

source

@[protected, instance]

def category_theory.limits.image.pre_comp_epi_of_epi {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_equalizers C] [category_theory.limits.has_image g] [category_theory.limits.has_image (f ≫ g)] [category_theory.epi f] :

category_theory.epi (category_theory.limits.image.pre_comp f g)

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

source

@[protected, instance]

def category_theory.limits.has_image_iso_comp {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_equalizers C] [category_theory.is_iso f] [category_theory.limits.has_image g] :

category_theory.limits.has_image (f ≫ g)

source

@[protected, instance]

def category_theory.limits.image.is_iso_precomp_iso {C : Type u} [category_theory.category C] {X Y Z : C} (g : Y ⟶ Z) [category_theory.limits.has_equalizers C] (f : X ⟶ Y) [category_theory.is_iso f] [category_theory.limits.has_image g] :

category_theory.is_iso (category_theory.limits.image.pre_comp f g)

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

source

@[protected, instance]

def category_theory.limits.has_image_comp_iso {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_equalizers C] [category_theory.limits.has_image f] [category_theory.is_iso g] :

category_theory.limits.has_image (f ≫ g)

source

noncomputable def category_theory.limits.image.comp_iso {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_equalizers C] [category_theory.limits.has_image f] [category_theory.is_iso g] :

category_theory.limits.image f ≅ category_theory.limits.image (f ≫ g)

Postcomposing by an isomorphism induces an isomorphism on the image.

Equations

category_theory.limits.image.comp_iso f g = {hom := category_theory.limits.image.lift (category_theory.limits.image.mono_factorisation (f ≫ g)).of_comp_iso, inv := category_theory.limits.image.lift ((category_theory.limits.image.mono_factorisation f).comp_mono g), hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.limits.image.comp_iso_hom_comp_image_ι {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_equalizers C] [category_theory.limits.has_image f] [category_theory.is_iso g] :

(category_theory.limits.image.comp_iso f g).hom ≫ category_theory.limits.image.ι (f ≫ g) = category_theory.limits.image.ι f ≫ g

source

@[simp]

theorem category_theory.limits.image.comp_iso_hom_comp_image_ι_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_equalizers C] [category_theory.limits.has_image f] [category_theory.is_iso g] {X' : C} (f' : Z ⟶ X') :

(category_theory.limits.image.comp_iso f g).hom ≫ category_theory.limits.image.ι (f ≫ g) ≫ f' = category_theory.limits.image.ι f ≫ g ≫ f'

source

@[simp]

theorem category_theory.limits.image.comp_iso_inv_comp_image_ι_assoc {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_equalizers C] [category_theory.limits.has_image f] [category_theory.is_iso g] {X' : C} (f' : Y ⟶ X') :

(category_theory.limits.image.comp_iso f g).inv ≫ category_theory.limits.image.ι f ≫ f' = category_theory.limits.image.ι (f ≫ g) ≫ category_theory.inv g ≫ f'

source

@[simp]

theorem category_theory.limits.image.comp_iso_inv_comp_image_ι {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z) [category_theory.limits.has_equalizers C] [category_theory.limits.has_image f] [category_theory.is_iso g] :

(category_theory.limits.image.comp_iso f g).inv ≫ category_theory.limits.image.ι f = category_theory.limits.image.ι (f ≫ g) ≫ category_theory.inv g

source

@[protected, instance]

def category_theory.limits.hom.has_image {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_image f] :

category_theory.limits.has_image (category_theory.arrow.mk f).hom

source

structure category_theory.limits.image_map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) :

Type v

map : category_theory.limits.image f.hom ⟶ category_theory.limits.image g.hom
map_ι' : self.map ≫ category_theory.limits.image.ι g.hom = category_theory.limits.image.ι f.hom ≫ sq.right . "obviously"

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

Instances for category_theory.limits.image_map

category_theory.limits.image_map.has_sizeof_inst
category_theory.limits.inhabited_image_map
category_theory.limits.image_map.subsingleton

source

@[protected, instance]

noncomputable def category_theory.limits.inhabited_image_map {C : Type u} [category_theory.category C] {f : category_theory.arrow C} [category_theory.limits.has_image f.hom] :

inhabited (category_theory.limits.image_map (𝟙 f))

Equations

category_theory.limits.inhabited_image_map = {default := {map := 𝟙 (category_theory.limits.image f.hom), map_ι' := _}}

source

@[simp]

theorem category_theory.limits.image_map.map_ι {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] {sq : f ⟶ g} (self : category_theory.limits.image_map sq) :

self.map ≫ category_theory.limits.image.ι g.hom = category_theory.limits.image.ι f.hom ≫ sq.right

source

@[simp]

theorem category_theory.limits.image_map.map_ι_assoc {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] {sq : f ⟶ g} (self : category_theory.limits.image_map sq) {X' : C} (f' : g.right ⟶ X') :

self.map ≫ category_theory.limits.image.ι g.hom ≫ f' = category_theory.limits.image.ι f.hom ≫ sq.right ≫ f'

source

@[simp]

theorem category_theory.limits.image_map.factor_map_assoc {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) (m : category_theory.limits.image_map sq) {X' : C} (f' : category_theory.limits.image g.hom ⟶ X') :

category_theory.limits.factor_thru_image f.hom ≫ m.map ≫ f' = sq.left ≫ category_theory.limits.factor_thru_image g.hom ≫ f'

source

@[simp]

theorem category_theory.limits.image_map.factor_map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) (m : category_theory.limits.image_map sq) :

category_theory.limits.factor_thru_image f.hom ≫ m.map = sq.left ≫ category_theory.limits.factor_thru_image g.hom

source

noncomputable def category_theory.limits.image_map.transport {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) (F : category_theory.limits.mono_factorisation f.hom) {F' : category_theory.limits.mono_factorisation g.hom} (hF' : category_theory.limits.is_image F') {map : F.I ⟶ F'.I} (map_ι : map ≫ F'.m = F.m ≫ sq.right) :

category_theory.limits.image_map sq

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

category_theory.limits.image_map.transport sq F hF' map_ι = {map := category_theory.limits.image.lift F ≫ map ≫ hF'.lift (category_theory.limits.image.mono_factorisation g.hom), map_ι' := _}

source

@[class]

structure category_theory.limits.has_image_map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) :

Prop

has_image_map : nonempty (category_theory.limits.image_map sq)

has_image_map sq means that there is an image_map for the square sq.

Instances of this typeclass

source

theorem category_theory.limits.has_image_map.mk {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] {sq : f ⟶ g} (m : category_theory.limits.image_map sq) :

category_theory.limits.has_image_map sq

source

theorem category_theory.limits.has_image_map.transport {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) (F : category_theory.limits.mono_factorisation f.hom) {F' : category_theory.limits.mono_factorisation g.hom} (hF' : category_theory.limits.is_image F') (map : F.I ⟶ F'.I) (map_ι : map ≫ F'.m = F.m ≫ sq.right) :

category_theory.limits.has_image_map sq

source

noncomputable def category_theory.limits.has_image_map.image_map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] :

category_theory.limits.image_map sq

Obtain an image_map from a has_image_map instance.

Equations

category_theory.limits.has_image_map.image_map sq = classical.choice category_theory.limits.has_image_map.has_image_map

source

@[protected, instance]

def category_theory.limits.has_image_map_of_is_iso {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.is_iso sq] :

category_theory.limits.has_image_map sq

source

@[protected, instance]

def category_theory.limits.has_image_map.comp {C : Type u} [category_theory.category C] {f g h : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] [category_theory.limits.has_image h.hom] (sq1 : f ⟶ g) (sq2 : g ⟶ h) [category_theory.limits.has_image_map sq1] [category_theory.limits.has_image_map sq2] :

category_theory.limits.has_image_map (sq1 ≫ sq2)

source

theorem category_theory.limits.image_map.ext {C : Type u} {_inst_1 : category_theory.category C} {f g : category_theory.arrow C} {_inst_2 : category_theory.limits.has_image f.hom} {_inst_3 : category_theory.limits.has_image g.hom} {sq : f ⟶ g} (x y : category_theory.limits.image_map sq) (h : x.map = y.map) :

x = y

source

theorem category_theory.limits.image_map.ext_iff {C : Type u} {_inst_1 : category_theory.category C} {f g : category_theory.arrow C} {_inst_2 : category_theory.limits.has_image f.hom} {_inst_3 : category_theory.limits.has_image g.hom} {sq : f ⟶ g} (x y : category_theory.limits.image_map sq) :

x = y ↔ x.map = y.map

source

@[protected, instance]

def category_theory.limits.image_map.subsingleton {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) :

subsingleton (category_theory.limits.image_map sq)

source

@[reducible]

noncomputable def category_theory.limits.image.map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] :

category_theory.limits.image f.hom ⟶ category_theory.limits.image g.hom

The map on images induced by a commutative square.

source

theorem category_theory.limits.image.factor_map {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] :

category_theory.limits.factor_thru_image f.hom ≫ category_theory.limits.image.map sq = sq.left ≫ category_theory.limits.factor_thru_image g.hom

source

theorem category_theory.limits.image.map_ι {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] :

category_theory.limits.image.map sq ≫ category_theory.limits.image.ι g.hom = category_theory.limits.image.ι f.hom ≫ sq.right

source

theorem category_theory.limits.image.map_hom_mk'_ι {C : Type u} [category_theory.category C] {X Y P Q : C} {k : X ⟶ Y} [category_theory.limits.has_image k] {l : P ⟶ Q} [category_theory.limits.has_image l] {m : X ⟶ P} {n : Y ⟶ Q} (w : m ≫ l = k ≫ n) [category_theory.limits.has_image_map (category_theory.arrow.hom_mk' w)] :

category_theory.limits.image.map (category_theory.arrow.hom_mk' w) ≫ category_theory.limits.image.ι l = category_theory.limits.image.ι k ≫ n

source

noncomputable def category_theory.limits.image_map_comp {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] {h : category_theory.arrow C} [category_theory.limits.has_image h.hom] (sq' : g ⟶ h) [category_theory.limits.has_image_map sq'] :

category_theory.limits.image_map (sq ≫ sq')

Image maps for composable commutative squares induce an image map in the composite square.

Equations

category_theory.limits.image_map_comp sq sq' = {map := category_theory.limits.image.map sq ≫ category_theory.limits.image.map sq', map_ι' := _}

source

@[simp]

theorem category_theory.limits.image.map_comp {C : Type u} [category_theory.category C] {f g : category_theory.arrow C} [category_theory.limits.has_image f.hom] [category_theory.limits.has_image g.hom] (sq : f ⟶ g) [category_theory.limits.has_image_map sq] {h : category_theory.arrow C} [category_theory.limits.has_image h.hom] (sq' : g ⟶ h) [category_theory.limits.has_image_map sq'] [category_theory.limits.has_image_map (sq ≫ sq')] :

category_theory.limits.image.map (sq ≫ sq') = category_theory.limits.image.map sq ≫ category_theory.limits.image.map sq'

source

noncomputable def category_theory.limits.image_map_id {C : Type u} [category_theory.category C] (f : category_theory.arrow C) [category_theory.limits.has_image f.hom] :

category_theory.limits.image_map (𝟙 f)

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

Equations

category_theory.limits.image_map_id f = {map := 𝟙 (category_theory.limits.image f.hom), map_ι' := _}

source

@[simp]

theorem category_theory.limits.image.map_id {C : Type u} [category_theory.category C] (f : category_theory.arrow C) [category_theory.limits.has_image f.hom] [category_theory.limits.has_image_map (𝟙 f)] :

category_theory.limits.image.map (𝟙 f) = 𝟙 (category_theory.limits.image f.hom)

source

@[class]

structure category_theory.limits.has_image_maps (C : Type u) [category_theory.category C] [category_theory.limits.has_images C] :

Type

has_image_map : ∀ {f g : category_theory.arrow C} (st : f ⟶ g), category_theory.limits.has_image_map st

If a category has_image_maps, then all commutative squares induce morphisms on images.

Instances of this typeclass

category_theory.limits.has_image_maps_of_has_strong_epi_images

Instances of other typeclasses for category_theory.limits.has_image_maps

category_theory.limits.has_image_maps.has_sizeof_inst

source

noncomputable def category_theory.limits.im {C : Type u} [category_theory.category C] [category_theory.limits.has_images C] [category_theory.limits.has_image_maps C] :

category_theory.arrow C ⥤ C

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

category_theory.limits.im = {obj := λ (f : category_theory.arrow C), category_theory.limits.image f.hom, map := λ (_x _x_1 : category_theory.arrow C) (st : _x ⟶ _x_1), category_theory.limits.image.map st, map_id' := _, map_comp' := _}

source

@[simp]

theorem category_theory.limits.im_map {C : Type u} [category_theory.category C] [category_theory.limits.has_images C] [category_theory.limits.has_image_maps C] (_x _x_1 : category_theory.arrow C) (st : _x ⟶ _x_1) :

category_theory.limits.im.map st = category_theory.limits.image.map st

source

@[simp]

theorem category_theory.limits.im_obj {C : Type u} [category_theory.category C] [category_theory.limits.has_images C] [category_theory.limits.has_image_maps C] (f : category_theory.arrow C) :

category_theory.limits.im.obj f = category_theory.limits.image f.hom

source

structure category_theory.limits.strong_epi_mono_factorisation {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) :

Type (max u v)

to_mono_factorisation : category_theory.limits.mono_factorisation f
e_strong_epi : category_theory.strong_epi self.to_mono_factorisation.e

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

Instances for category_theory.limits.strong_epi_mono_factorisation

category_theory.limits.strong_epi_mono_factorisation.has_sizeof_inst
category_theory.limits.strong_epi_mono_factorisation_inhabited

source

@[protected, instance]

def category_theory.limits.strong_epi_mono_factorisation_inhabited {C : Type u} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.strong_epi f] :

inhabited (category_theory.limits.strong_epi_mono_factorisation f)

Satisfying the inhabited linter

Equations

category_theory.limits.strong_epi_mono_factorisation_inhabited f = {default := {to_mono_factorisation := {I := Y, m := 𝟙 Y, m_mono := _, e := f, fac' := _}, e_strong_epi := _inst_2}}

source

noncomputable def category_theory.limits.strong_epi_mono_factorisation.to_mono_is_image {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.strong_epi_mono_factorisation f) :

category_theory.limits.is_image F.to_mono_factorisation

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

Equations

F.to_mono_is_image = {lift := λ (G : category_theory.limits.mono_factorisation f), _.lift, lift_fac' := _}

source

@[class]

structure category_theory.limits.has_strong_epi_mono_factorisations (C : Type u) [category_theory.category C] :

Prop

has_fac : ∀ {X Y : C} (f : X ⟶ Y), nonempty (category_theory.limits.strong_epi_mono_factorisation f)

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

source

theorem category_theory.limits.has_strong_epi_mono_factorisations.mk {C : Type u} [category_theory.category C] (d : Π {X Y : C} (f : X ⟶ Y), category_theory.limits.strong_epi_mono_factorisation f) :

category_theory.limits.has_strong_epi_mono_factorisations C

source

@[protected, instance]

def category_theory.limits.has_images_of_has_strong_epi_mono_factorisations {C : Type u} [category_theory.category C] [category_theory.limits.has_strong_epi_mono_factorisations C] :

category_theory.limits.has_images C

source

@[class]

structure category_theory.limits.has_strong_epi_images (C : Type u) [category_theory.category C] [category_theory.limits.has_images C] :

Prop

strong_factor_thru_image : ∀ {X Y : C} (f : X ⟶ Y), category_theory.strong_epi (category_theory.limits.factor_thru_image f)

A category has strong epi images if it has all images and factor_thru_image f is a strong epimorphism for all f.

Instances of this typeclass

source

theorem category_theory.limits.strong_epi_of_strong_epi_mono_factorisation {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} (F : category_theory.limits.strong_epi_mono_factorisation f) {F' : category_theory.limits.mono_factorisation f} (hF' : category_theory.limits.is_image F') :

category_theory.strong_epi F'.e

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

source

theorem category_theory.limits.strong_epi_factor_thru_image_of_strong_epi_mono_factorisation {C : Type u} [category_theory.category C] {X Y : C} {f : X ⟶ Y} [category_theory.limits.has_image f] (F : category_theory.limits.strong_epi_mono_factorisation f) :

category_theory.strong_epi (category_theory.limits.factor_thru_image f)

source

@[protected, instance]

def category_theory.limits.has_strong_epi_images_of_has_strong_epi_mono_factorisations {C : Type u} [category_theory.category C] [category_theory.limits.has_strong_epi_mono_factorisations C] :

category_theory.limits.has_strong_epi_images C

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

source

@[protected, instance]

def category_theory.limits.has_image_maps_of_has_strong_epi_images {C : Type u} [category_theory.category C] [category_theory.limits.has_images C] [category_theory.limits.has_strong_epi_images C] :

category_theory.limits.has_image_maps C

A category with strong epi images has image maps.

Equations

category_theory.limits.has_image_maps_of_has_strong_epi_images = {has_image_map := _}

source

@[protected, instance]

def category_theory.limits.has_strong_epi_images_of_has_pullbacks_of_has_equalizers {C : Type u} [category_theory.category C] [category_theory.limits.has_images C] [category_theory.limits.has_pullbacks C] [category_theory.limits.has_equalizers C] :

category_theory.limits.has_strong_epi_images C

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

source

noncomputable def category_theory.limits.image.iso_strong_epi_mono {C : Type u} [category_theory.category C] [category_theory.limits.has_strong_epi_mono_factorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [category_theory.strong_epi e] [category_theory.mono m] :

I' ≅ category_theory.limits.image f

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

category_theory.limits.image.iso_strong_epi_mono e m comm = (category_theory.limits.strong_epi_mono_factorisation.mk {I := I', m := m, m_mono := _inst_4, e := e, fac' := comm}).to_mono_is_image.iso_ext (category_theory.limits.image.is_image f)

source

@[simp]

theorem category_theory.limits.image.iso_strong_epi_mono_hom_comp_ι {C : Type u} [category_theory.category C] [category_theory.limits.has_strong_epi_mono_factorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [category_theory.strong_epi e] [category_theory.mono m] :

(category_theory.limits.image.iso_strong_epi_mono e m comm).hom ≫ category_theory.limits.image.ι f = m

source

@[simp]

theorem category_theory.limits.image.iso_strong_epi_mono_inv_comp_mono {C : Type u} [category_theory.category C] [category_theory.limits.has_strong_epi_mono_factorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I') (m : I' ⟶ Y) (comm : e ≫ m = f) [category_theory.strong_epi e] [category_theory.mono m] :

(category_theory.limits.image.iso_strong_epi_mono e m comm).inv ≫ m = category_theory.limits.image.ι f

source

theorem category_theory.functor.has_strong_epi_mono_factorisations_imp_of_is_equivalence {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (F : C ⥤ D) [category_theory.is_equivalence F] [h : category_theory.limits.has_strong_epi_mono_factorisations C] :

category_theory.limits.has_strong_epi_mono_factorisations D

mathlib3 documentation

Categorical images #

Main definitions #

Main statements #

Future work #