Commit 2025-02-08 18:21 2477cf96

View on Github →

feat(Algebra/Category): adjunctions in CommRingCat (#21427)

Estimated changes

Modified Mathlib/Algebra/Category/MonCat/Adjunctions.lean

added def AddCommMonCat.adj

added def AddCommMonCat.free

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

added def AddCommMonCat.equivalence

added def AddMonCat.equivalence

Modified Mathlib/Algebra/Category/Ring/Adjunctions.lean

added def CommRingCat.coyoneda

added def CommRingCat.coyonedaAdj

added def CommRingCat.coyonedaUnique

added def CommRingCat.forget₂Adj

added def CommRingCat.monoidAlgebra

added def CommRingCat.monoidAlgebraAdj

Modified Mathlib/Algebra/Category/Ring/Basic.lean

Modified Mathlib/CategoryTheory/Adjunction/Over.lean

added def CategoryTheory.Under.equivalenceOfIsInitial