Theorems · Theorem · category theory

AddMonCat.equivalence_counitIso

AddMonCat.equivalence.counitIso =
  CategoryTheory.Iso.refl
    ({ obj := fun X => AddMonCat.of (Additive ↑X),
          map := fun {X Y} f => AddMonCat.ofHom (MonoidHom.toAdditive (MonCat.Hom.hom f)),
          map_id := AddMonCat.equivalence._proof_3, map_comp := @AddMonCat.equivalence._proof_4 }.comp
      { obj := fun X => MonCat.of (Multiplicative ↑X),
        map := fun {X Y} f => MonCat.ofHom (AddMonoidHom.toMultiplicative (AddMonCat.Hom.hom f)),
        map_id := AddMonCat.equivalence._proof_1, map_comp := @AddMonCat.equivalence._proof_2 })

Defined in

Mathlib.Algebra.Category.MonCat.Basic

Cited by

0 results in Mathlib

Foundations

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