Zulip Chat Archive

Stream: maths

Topic: concrete_category.coe_{id,comp}


view this post on Zulip 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

view this post on Zulip Johan Commelin (May 06 2021 at 08:03):

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

view this post on Zulip Johan Commelin (May 06 2021 at 08:03):

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

view this post on Zulip Kevin Buzzard (May 06 2021 at 08:04):

What are the statements of the unapplied versions?

view this post on Zulip 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