## Stream: maths

### Topic: concrete_category.coe_{id,comp}

#### Johan Commelin (May 06 2021 at 08:03):

Mathlib currently has:

@[simp] lemma coe_id {X : C} (x : X) : ((𝟙 X) : X → X) x = x :=
congr_fun ((forget _).map_id X) x

@[simp] lemma coe_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
(f ≫ g) x = g (f x) :=
congr_fun ((forget _).map_comp _ _) x


#### Johan Commelin (May 06 2021 at 08:03):

Should those become unapplied versions. And then also have id_apply and comp_apply?

#### Johan Commelin (May 06 2021 at 08:03):

That seems to be what happens with docs#Profinite.id_apply and friends.

#### Kevin Buzzard (May 06 2021 at 08:04):

What are the statements of the unapplied versions?

#### Kevin Buzzard (May 06 2021 at 08:05):

aah, you mean docs#Profinite.coe_id etc. Yeah, that sounds better than what we have! But not as simp lemmas I guess (the unapplied versions)

Last updated: Jun 17 2021 at 16:20 UTC