[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hf : LinearMap.ker f = ⊥
⊢ Function.Injective ↑f
[PROOFSTEP]
convert LinearMap.ker_eq_bot.1 hf
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
rw [mono_iff_ker_eq_bot, LinearMap.ker_eq_bot]
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
rw [epi_iff_range_eq_top, LinearMap.range_eq_top]
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi ((forget (ModuleCat R)).map f)
[PROOFSTEP]
erw [CategoryTheory.epi_iff_surjective, ← epi_iff_surjective]
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi f
[PROOFSTEP]
exact hf
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono ((forget (ModuleCat R)).map f)
[PROOFSTEP]
erw [CategoryTheory.mono_iff_injective, ← mono_iff_injective]
[GOAL]
R : Type u
inst✝² : Ring R
X Y : ModuleCat R
f✝ : X ⟶ Y
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X✝ Y✝ : ModuleCat R
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono f
[PROOFSTEP]
exact hf
