category theory: isomorphisms between images

Stream: Is there code for X?

[Kevin Buzzard]

I'm having trouble making eq_to_hom : image f = image g cancel when f = g. This is in contrast to my usual experience with eq_to_hom which is that when you make the stars align, simp makes it vanish. I think that the three claims below are all basically equivalent and I can't prove any of them. If someone could help me to prove one of them that would be great; any hints about which if any of them should be in mathlib / be @[simp] / @[simps] / @[reassoc] / whatever (I don't understand any of these properly within the context of category theory yet) would also be welcomed :-)

import category_theory.abelian.basic

open category_theory category_theory.limits

variables (𝓐 : Type*) [category 𝓐] [abelian 𝓐]

example (A B : 𝓐) (f g : A ⟶ B) (h : f = g) :
  (eq_to_hom (by rw h) : image f ⟶ image g) ≫ image.ι g = image.ι f :=
begin
  sorry
end

example (A B : 𝓐) (f g : A ⟶ B) (h : f = g) :
  factor_thru_image f ≫ (eq_to_hom (by rw h) : image f ⟶ image g) = factor_thru_image g :=
begin
  sorry
end

example (A B : 𝓐) (f g : A ⟶ B) (h : f = g) :
  factor_thru_image f ≫ (eq_to_hom (by rw h) : image f ⟶ image g) ≫ image.ι g = f :=
begin
  sorry,
end

[Kevin Buzzard]

PS I'm a little surprised that ext doesn't append image.ι g to both morphisms in the middle example. Should it? If it did then simp then reduces it to the third example.

[Kevin Buzzard]

Aah, docs#category_theory.limits.image.eq_fac should help.

[Kevin Buzzard]

example (A B : 𝓐) (f g : A ⟶ B) (h : f = g) :
  (eq_to_hom (by rw h) : image f ⟶ image g) = (image.eq_to_iso h).hom :=
begin
  sorry -- :-(
end

:sad:

[Adam Topaz]

Are you using docs#category_theory.limits.image.eq_to_hom ?

[Adam Topaz]

I suppose (read: hope) that would behave better with the image api

[Kevin Buzzard]

OK so you're telling me that in the specific case when I want image f -> image g from f = g I should not use docs#category_theory.eq_to_hom but I should instead use docs#category_theory.limits.image.eq_to_hom ? My last example is me failing to prove that these coincide, basically.

[Adam Topaz]

It looks like the API is rather built up around docs#category_theory.limits.image.eq_to_iso

[Kevin Buzzard]

Are there any more eq_to_homs I need to know about??

[Adam Topaz]

I don't know. It seems that we're missing some lemmas around the image api

[Adam Topaz]

example (A B : 𝓐) (f g : A ⟶ B) (h : f = g) :
  (eq_to_hom (by rw h) : image f ⟶ image g) = (image.eq_to_iso h).hom :=
begin
  cases h,
  rw [← cancel_mono (image.ι f), ← image.eq_fac h],
  simp,
end

In case it helps :slight_frown:

[Adam Topaz]

I don't know why docs#category_theory.limits.image.eq_fac is not reversed and tagged with simp.
I don't know why we don't have an ext lemma about image.ι.
Were these intentional design decisions @Scott Morrison @Markus Himmel ?

[Kevin Buzzard]

Let me say right now that I'm loving the abelian category API. I've found it very intuitive to use and I've written 1000 lines of code in the last week or so using it without any problems until now; furthermore it seems like the solutions to all my current problems are in this thread. But I have the same questions as Adam.

[Adam Topaz]

For abelian categories, I suspect that docs#category_theory.abelian.image is much better behaved.

[Kevin Buzzard]

I can do everything with eq_to_hom if the following were simp lemmas:

@[simp, reassoc] lemma _root_.category_theory.limits.eq_to_hom_comp_image.ι {C : Type*} [category C] {X Y : C} {f f' : X ⟶ Y}
  [has_image f] [has_image f'] [has_equalizers C] (h : f = f') :
(eq_to_hom (by simp_rw h)) ≫ image.ι f' = image.ι f :=
begin
  unfreezingI {subst h},
  simp,
end

--- move
@[simp, reassoc] lemma _root_.category_theory.limits.eq_to_hom_comp_kernel.ι {C : Type*}
  [category C] [abelian C] {X Y : C} {f f' : X ⟶ Y} (h : f = f') :
(eq_to_hom (by simp_rw h)) ≫ kernel.ι f' = kernel.ι f :=
begin
  unfreezingI {subst h},
  simp,
end

I only care about abelian categories right now so the second one has too many assumptions. The first one is the other way around from a lemma we have already, modulo the fact that I am wedded to eq_to_hom rather than the image-specific versions.

[Kevin Buzzard]

Thanks to Adam for reminding me that just because I can't subst or cases on the equality of functions in my use case (d_from = d i j >> some_iso_or_other) I can do it in the general lemmas.