## Stream: maths

### Topic: proving theorems in the theory of categories

#### 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 $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 (Jan 16 2020 at 02:21):

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

#### 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 ?


#### 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


#### 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

#### 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

#### Reid Barton (Jan 16 2020 at 04:17):

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

#### Enrico Borba (Jan 16 2020 at 05:58):

That worked! Thanks :)

Last updated: May 10 2021 at 08:14 UTC