# Zulip Chat Archive

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