concrete_category.coe_{id,comp}

Stream: maths

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

What are the statements of the unapplied versions?

[Kevin Buzzard]

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)