Commit 2025-07-28 17:03 7cd7d2ce

View on Github →

feat: if F is fully faithful, then so is F.mapGrp (#27580) Follow up to #23874. Also remove the corresponding noncomputable as they are now unnecessary. From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

added def CategoryTheory.Functor.mapCommGrp

added def CategoryTheory.Functor.mapCommGrpCompIso

added def CategoryTheory.Functor.mapCommGrpIdIso

added def CategoryTheory.Functor.mapCommGrpNatIso

added def CategoryTheory.Functor.mapCommGrpNatTrans

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

added def CategoryTheory.Adjunction.mapCommMon

added def CategoryTheory.Equivalence.mapCommMon

added def CategoryTheory.Functor.mapCommMonCompIso

added def CategoryTheory.Functor.mapCommMonIdIso

added def CategoryTheory.Functor.mapCommMonNatIso

added def CategoryTheory.Functor.mapCommMonNatTrans

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

added def CategoryTheory.Adjunction.mapGrp

added def CategoryTheory.Equivalence.mapGrp

added def CategoryTheory.Functor.mapGrp

added def CategoryTheory.Functor.mapGrpCompIso

added def CategoryTheory.Functor.mapGrpIdIso

added def CategoryTheory.Functor.mapGrpNatIso

added def CategoryTheory.Functor.mapGrpNatTrans

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

added def CategoryTheory.Adjunction.mapMon

added def CategoryTheory.Equivalence.mapMon

added def CategoryTheory.Functor.mapMonCompIso

added def CategoryTheory.Functor.mapMonIdIso

added def CategoryTheory.Functor.mapMonNatIso

added def CategoryTheory.Functor.mapMonNatTrans