Theorems · Theorem · category theory

ModuleCat.isoMk_inv

∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R}
  (φ : (CategoryTheory.forget₂ (ModuleCat R) Ab).obj M ≅ (CategoryTheory.forget₂ (ModuleCat R) Ab).obj N)
  (hφ :
    ∀ (r : R),
      CategoryTheory.CategoryStruct.comp φ.hom (N.smul r) = CategoryTheory.CategoryStruct.comp (M.smul r) φ.hom),
  (ModuleCat.isoMk φ hφ).inv = ModuleCat.homMk φ.inv ⋯

Defined in

Mathlib.Algebra.Category.ModuleCat.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

Ring