Commit 2023-05-30 07:01 c57f43bf

View on Github →

feat: port Algebra.Category.ModuleCat.Adjunctions (#4457)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

added def CategoryTheory.Free.embedding

added def CategoryTheory.Free.embeddingLiftIso

added def CategoryTheory.Free.ext

added def CategoryTheory.Free.lift

added def CategoryTheory.Free.liftUnique

added theorem CategoryTheory.Free.lift_map_single

added def CategoryTheory.Free.of

added theorem CategoryTheory.Free.single_comp_single

added def CategoryTheory.Free

added theorem ModuleCat.Free.associativity

added theorem ModuleCat.Free.left_unitality

added theorem ModuleCat.Free.right_unitality

added def ModuleCat.Free.ε

added theorem ModuleCat.Free.ε_apply

added def ModuleCat.Free.μ

added theorem ModuleCat.Free.μ_natural

added def ModuleCat.adj

added def ModuleCat.free

added def ModuleCat.monoidalFree