proving theorems in the theory of categories

Stream: maths

[Enrico Borba]

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 $f$ , the existence of a right inverse $g$ implies that $f$ 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

[Simon Hudon]

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

[Enrico Borba]

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 ?

[Enrico Borba]

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

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

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

[Enrico Borba]

That worked! Thanks :)