Zulip Chat Archive

Stream: maths

Topic: Adjunctions


view this post on Zulip Adam Topaz (Oct 15 2020 at 13:06):

@Eric Wieser Looks like mathlib already has docs#category_theory.adjunction.comp

view this post on Zulip Adam Topaz (Oct 15 2020 at 13:07):

We should define the adjunction between R-algebras and R-modules (this is the tensor algebra).

view this post on Zulip Adam Topaz (Oct 15 2020 at 13:08):

(Continuing the discussion from here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Generalizing.20over.20morphisms/near/213317745 )

view this post on Zulip Adam Topaz (Oct 15 2020 at 13:27):

I know mathlib has general direct sums, but does it have the functoriality of the free R- module on a type S? (Functoriality in S)


Last updated: May 10 2021 at 07:15 UTC