Theorems · Definition · category theory

ModuleCat.freeDesc

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

The morphism of modules (free R).obj X ⟶ M corresponding to a map f : X ⟶ M.

Defined in

Mathlib.Algebra.Category.ModuleCat.Adjunctions

Cited by

4 results in Mathlib

Foundations

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

Assumes

Ring