Zulip Chat Archive

Stream: maths

Topic: proving theorems in the theory of categories


view this post on Zulip Enrico Borba (Jan 16 2020 at 02:13):

I'm trying to prove a statement about all categories but can't state it properly. I'm trying to state that given a morphism ff , the existence of a right inverse gg implies that ff is an epimorphism. Here's my attempt at stating it

  universes v u

  example {C : Type u} [category.{v} C] (A B : C.obj) (f : A ⟶ B) :
      ∃ g: B ⟶ A, f ≫ g = C.id B → category_theory.epi f := sorry

I'm not exactly sure how to state that
1. C is a category
2. A B are objects of C
3. f is a morphism from A to B

view this post on Zulip Simon Hudon (Jan 16 2020 at 02:21):

Instead of (A B : C.obj), use (A B : C). Everything else should work

view this post on Zulip Enrico Borba (Jan 16 2020 at 02:52):

Hmm that doesn't solve it either. I get this output. Sorry for the large log

/home/enricozb/projects/learning/lean/algebra_chapter_0/src/ch1.lean:236:24: error: function expected at
  category
term has type
  Type (max (v+1) (u+1))
/home/enricozb/projects/learning/lean/algebra_chapter_0/src/ch1.lean:236:59: error: failed to synthesize type class instance for
C : Type u,
_inst_1 : ⁇,
A B : C
⊢ category_theory.has_hom C
/home/enricozb/projects/learning/lean/algebra_chapter_0/src/ch1.lean:237:13: error: failed to synthesize type class instance for
C : Type u,
_inst_1 : ⁇,
A B : C,
f : A ⟶ B
⊢ category_theory.has_hom C
/home/enricozb/projects/learning/lean/algebra_chapter_0/src/ch1.lean:237:27: error: invalid field notation, type is not of the form (C ...) where C is a constant
  C
has type
  Type u
/home/enricozb/projects/learning/lean/algebra_chapter_0/src/ch1.lean:237:20: error: don't know how to synthesize placeholder
context:
C : Type u,
_inst_1 : ⁇,
A B : C,
f : A ⟶ B,
g : B ⟶ A
⊢ Type ?

view this post on Zulip Enrico Borba (Jan 16 2020 at 02:55):

Oh shoot I have a definition of category that's conflicting. Here's what I get with your suggested change

/home/enricozb/projects/learning/lean/algebra_chapter_0/src/ch1.lean:237:27: error: invalid field notation, type is not of the form (C ...) where C is a constant
  C
has type
  Type u

view this post on Zulip Simon Hudon (Jan 16 2020 at 02:56):

That fixes one thing. The other one should be fixed by replacing C.id B with \b1 B

view this post on Zulip Reid Barton (Jan 16 2020 at 04:17):

Also that existential scopes over the entire rest of the statement, which is not what you want

view this post on Zulip Reid Barton (Jan 16 2020 at 04:17):

Just make g and the hypothesis on it into more function arguments

view this post on Zulip Enrico Borba (Jan 16 2020 at 05:58):

That worked! Thanks :)


Last updated: May 10 2021 at 08:14 UTC