Theorems · Theorem · category theory

ModuleCat.ExtendScalars.hom_ext

∀ {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

4 results in Mathlib

Foundations

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

Assumes

CommRingCommRing