Morphisms in concrete categories

Stream: maths

[Markus Himmel]

I don't understand how to work with concrete categories. Is there some standard way of saying "take this bundled homomorphism and turn it into a morphism in the corresponding concrete category"? For example, the following does not work:

import algebra.category.Group.preadditive
import category_theory.limits.shapes.kernels

open category_theory.limits

universe u

namespace AddCommGroup

variables {G H : AddCommGroup.{u}} (f : G ⟶ H)

def kernel_fork : kernel_fork f :=
kernel_fork.of_ι f.ker.subtype sorry

end AddCommGroup

The error is

type mismatch at application
  kernel_fork.of_ι (add_monoid_hom.ker f).subtype
term
  (add_monoid_hom.ker f).subtype
has type
  ↥(add_monoid_hom.ker f) →+ ↥G
but is expected to have type
  ?m_1 ⟶ G

One way to fix this is the following:

import algebra.category.Group.preadditive
import category_theory.limits.shapes.kernels

open category_theory.limits

universe u

namespace AddCommGroup

section
variables {G H : Type u} [add_comm_group G] [add_comm_group H]

def magic : (G →+ H) → (of G ⟶ of H) := id

end

section
variables {G H : AddCommGroup.{u}} (f : G ⟶ H)

def kernel_fork : kernel_fork f :=
kernel_fork.of_ι (magic f.ker.subtype) sorry

end

end AddCommGroup

Is this the intended thing to do in this situation? Does the function magic already exist somewhere in the setup for bundled categories?

[Markus Himmel]

Ah, it looks like this exists for the category Type under the name category_theory.as_hom. Should this exist for all concrete categories?

[Scott Morrison]

hmm... I'm used to this working better "out of the box"... Does a type annotation help?

[Scott Morrison]

I'd be happy to hear results of attempting to generalise as_hom (or just provide one for each?)

[Scott Morrison]

I think there's yet-another-up-arrow notation defined for it, but I've barely used it.

[Markus Himmel]

Scott Morrison said:

hmm... I'm used to this working better "out of the box"... Does a type annotation help?

I talked to Sebastian Ullrich about this a few months ago in the context of my Bachelor's thesis and he explained to me that type annotations do not help in this particular situation.

[Scott Morrison]

Okay, I guess we better see how polymorphic we can make that hook-up-arrow.