Zulip Chat Archive

Stream: maths

Topic: Adjunctions

Adam Topaz (Oct 15 2020 at 13:06):

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

Adam Topaz (Oct 15 2020 at 13:07):

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

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 )

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: Dec 20 2023 at 11:08 UTC