constructing a morphism in a category

Stream: new members

[Yaël Dillies]

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]

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]

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]

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]

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