Theorems · Definition · category theory

ModuleCat.freeHomEquiv

{R : Type u} → [inst : Ring R] → {X : Type u} → {M : ModuleCat R} → ((ModuleCat.free R).obj X ⟶ M) ≃ (X ⟶ ↑M)

The bijection ((free R).obj X ⟶ M) ≃ (X → M) when X is a type and M a module.

Defined in

Mathlib.Algebra.Category.ModuleCat.Adjunctions

Cited by

3 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Ring