Theorems · Theorem · category theory

ModuleCat.ExtendScalars.hom_ext_iff

∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} {M : ModuleCat R}
  {N : ModuleCat S} {α β : (ModuleCat.extendScalars f).obj M ⟶ N},
  α = β ↔
    ∀ (m : ↑M),
      (CategoryTheory.ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (CategoryTheory.ConcreteCategory.hom β) (1 ⊗ₜ[R] m)

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRing