# Zulip Chat Archive

## Stream: maths

### Topic: Morphisms in concrete categories

#### Markus Himmel (Jul 22 2020 at 14:17):

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 (Jul 22 2020 at 14:20):

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 (Jul 22 2020 at 14:36):

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

#### Scott Morrison (Jul 22 2020 at 14:37):

I'd be happy to hear results of attempting to generalise `as_hom`

(or just provide one for each?)

#### Scott Morrison (Jul 22 2020 at 14:37):

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

#### Markus Himmel (Jul 22 2020 at 14:39):

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 (Jul 22 2020 at 14:42):

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

Last updated: May 14 2021 at 19:21 UTC