R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : CategoryTheory.Injective (ModuleCat.mk Q)
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ↑f
g : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), ↑h (↑f x) = ↑g x
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : CategoryTheory.Injective (ModuleCat.mk Q)
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ↑f
g : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), ↑h (↑f x) = ↑g x
skip
case intro
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : CategoryTheory.Injective (ModuleCat.mk Q)
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ↑f
h : ModuleCat.mk Y ⟶ ModuleCat.mk Q
⊢ ∃ h_1, ∀ (x : X), ↑h_1 (↑f x) = ↑(f ≫ h) x
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : CategoryTheory.Injective (ModuleCat.mk Q)
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ↑f
g : X →ₗ[R] Q
⊢ ∃ h, ∀ (x : X), ↑h (↑f x) = ↑g x
rcases@CategoryTheory.Injective.factors (ModuleCat R) _ ⟨Q⟩ _ ⟨X⟩ ⟨Y⟩ g f
    ((ModuleCat.mono_iff_injective _).mpr hf) with
  ⟨h, rfl⟩
no goals
case intro
R : Type u
inst✝³ : Ring R
Q : TypeMax
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : CategoryTheory.Injective (ModuleCat.mk Q)
X Y : TypeMax
ins1 : AddCommGroup X
ins2 : AddCommGroup Y
ins3 : Module R X
ins4 : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ↑f
h : ModuleCat.mk Y ⟶ ModuleCat.mk Q
⊢ ∃ h_1, ∀ (x : X), ↑h_1 (↑f x) = ↑(f ≫ h) x
exact ⟨h, fun x => rfl⟩