Zulip Chat Archive

Stream: new members

Topic: constructing a morphism in a category


Yaël Dillies (Sep 23 2021 at 08:22):

What you need to prove is something that'll look like

example (X : category) (x : X) : x \hom x

Note that I've never done any category theory and this is just my best guess at translating. What might shock you is that you don't want a theorem but a definition. Mathematicians tend to state everything in terms of theorems, but definitions are very important too and should be underlined as such.

Kevin Buzzard (Sep 23 2021 at 08:23):

this is a bit misleading because we're talking to a beginner and categories aren't bundled so this code doesn't work. It's probably best to actually answer the question rather than just guess

Kevin Buzzard (Sep 23 2021 at 08:27):

import category_theory.category
import tactic

open category_theory

-- "there exists f : x ⟶ x such that...something true is true"
example (C : Type) [category C] (x : C) :  f : x  x, true :=
begin
  use 𝟙 x,
end

Scott Morrison (Sep 23 2021 at 08:39):

Is you just want the bare existence of such a morphism you might instead write:

import category_theory.category
import tactic

open category_theory

example (C : Type) [category C] (x : C) : nonempty (x  x) :=
begin
  use 𝟙 x,
end

or just

example (C : Type) [category C] (x : C) : x  x := 𝟙 x

Elias Fåkvam (Sep 23 2021 at 09:10):

Thank you both! This was very helpful. I found it interesting that you wrote two different goals, i was curious if they were equivalent, and think i managed to answer my own question thanks to your help.

variables (C : Type) [category C]
example (x : C) : ( f : x  x, true)  nonempty (x  x) :=
begin
  split,
  intro h1,
  cases h1 with f,
  use f,
  intro h2,
  use 𝟙 x,
end

Last updated: Dec 20 2023 at 11:08 UTC