Zulip Chat Archive

Stream: maths

Topic: Morphisms in concrete categories


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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