wrote a definition for free objects, requesting feedback

Stream: new members

[drocta]

I tried to write a definition of free objects in a category over a type, and what I wrote type-checks, but I'm not certain it does the right thing, and if it does, I suspect there is a cleaner/better way to write it, but I don't know how.
My code does not yet conform to the mathlib library style conventions.
Would anyone be willing to look over my code to evaluate whether it does the right thing, and whether there are substantially better ways I could organize it?

import category_theory.category
import category_theory.concrete_category

open category_theory

section

universes u_1 u_2

-- typical example for c is a typeclass, like topological_space , with hom being something like continuous.
variables (c : Type u_1 -> Type u_2) (hom : (Pi {alpha beta : Type u_1}, c alpha -> c beta -> (alpha -> beta) -> Prop))
variable my_concrete_category : concrete_category @hom

def is_free_over (X : bundled c) (generators_of_X : Type u_1 ) (i : generators_of_X -> (@forget c @hom my_concrete_category).obj X) : Prop :=
  forall (Y : bundled c) (f : generators_of_X -> ((@forget c @hom my_concrete_category).obj Y)),
    ∃! (g : has_hom.hom X Y), f = ((@forget c @hom my_concrete_category).map g) ∘ i

#check is_free_over

end

Thank you

[Johan Commelin]

Your lines are a bit long. Also, if you want syntax highlighting on Zulip, wrap your code like this:

```lean

```

[Johan Commelin]

@drocta I find this code quite hard to parse... you don't seem to be opposed to unicode, since you use ∃ and ∘. So why don't you use u₁ u₂ and Type u₁ → Type u₂ and X ⟶ Y to make things more readable?

[drocta]

Thank you for your feedback! (have edited the previous comment to include the syntax highlighting)
I had been trying to avoid using unicode characters, but I kind of gave in for the exists-unique and the composition because I didn't see anything that would let me say something like exists! (g : blah) , bluh , and because I didn't remember the ascii way of saying function composition.
But, I suppose I may as well give in and use the long arrow for the morphism types.
Would using it for the short arrows and the subscripts improve the clarity all that much?

I had wanted to use forget without specifying the implicit parameters, or at least to define a version with them filled in before the place that I currently use forget, but when I change the definition to be like that ( :

def is_free_over (X : bundled c) (generators_of_X : Type u_1 ) (i : generators_of_X -> forget.obj X) : Prop :=
  forall (Y : bundled c) (f : generators_of_X -> (forget.obj Y)),
    ∃! (g : X ⟶ Y), f = (forget.map g) ∘ i

)
It no longer type-checks, and I'm not really sure why.
Which is unfortunate, as I feel that that would make it much nicer to read. Though, I guess in that case it doesn't refer to the concrete category my_concrete_category anywhere so it makes some sense to me that it doesn't work.

I have to admit that I don't really understand how the type classes work.
Is there a better way to refer to (X : objects_of_my_concrete_category) which would make the forget calls work without having to specify their implicit arguments?

Thank you again!

[Johan Commelin]

I'm not sure why it would fail... I agree that this is sometimes annoying...