case intro
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Injective R Q
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.mk Q
f : X✝ ⟶ Y✝
mn : CategoryTheory.Mono f
h : ↑Y✝ →ₗ[R] ↑(ModuleCat.mk Q)
eq1 : ∀ (x : ↑X✝), ↑h (↑f x) = ↑g x
⊢ ∃ h, f ≫ h = g
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Injective R Q
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.mk Q
f : X✝ ⟶ Y✝
mn : CategoryTheory.Mono f
⊢ ∃ h, f ≫ h = g
rcases Module.Injective.out _ _ f ((ModuleCat.mono_iff_injective f).mp mn) g with ⟨h, eq1⟩
no goals
case intro
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Injective R Q
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.mk Q
f : X✝ ⟶ Y✝
mn : CategoryTheory.Mono f
h : ↑Y✝ →ₗ[R] ↑(ModuleCat.mk Q)
eq1 : ∀ (x : ↑X✝), ↑h (↑f x) = ↑g x
⊢ ∃ h, f ≫ h = g
exact ⟨h, LinearMap.ext eq1⟩