Zulip Chat Archive

Stream: maths

Topic: bifunctor and End homs

view this post on Zulip Yury G. Kudryashov (Sep 29 2019 at 23:58):

Hi, what of the following do we already have in mathlib (no universes for simplicity)?

variables {C D : Type} [category C] [category D] (X : C) (Y : D)
definition n1 : End X × End Y  End (X, Y) := sorry
definition n2 : (End X)ᵒᵖ * End (op X) := sorry
definition n3 : (End (op X) × End Y) →* End (X  Y) := sorry
definition n4 : ((End X)ᵒᵖ × End Y) →* End (X  Y) := sorry
definition n5 {M : Type} [monoid M] : (Mᵒᵖ →* End X)  (M →* End Y)  (M  End (X  Y)) := sorry

Of course, most of these definitions are trivial but I'd prefer to avoid code duplication.

Last updated: May 14 2021 at 20:13 UTC