R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
⊢ range (dualMap f) = range (dualMap (mkQ (ker f)))
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
⊢ range (dualMap f) = dualAnnihilator (ker f)
rw [← f.ker.range_dualMap_mkQ_eq]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range (dualMap f) = range (dualMap (mkQ (ker f)))
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
⊢ range (dualMap f) = range (dualMap (mkQ (ker f)))
let f' := LinearMap.quotKerEquivOfSurjective f hf
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range (dualMap f) = range (comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f')))

R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range (comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f'))) = range (dualMap (mkQ (ker f)))
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range (dualMap f) = range (dualMap (mkQ (ker f)))
trans LinearMap.range (f.dualMap.comp f'.symm.dualMap.toLinearMap)
case hf
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range ↑(LinearEquiv.dualMap (LinearEquiv.symm f')) = ⊤
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range (dualMap f) = range (comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f')))
rw [LinearMap.range_comp_of_range_eq_top]
no goals
case hf
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range ↑(LinearEquiv.dualMap (LinearEquiv.symm f')) = ⊤
apply LinearEquiv.range
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f')) = dualMap (mkQ (ker f))
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range (comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f'))) = range (dualMap (mkQ (ker f)))
apply congr_arg
case h.h.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
φ : Dual R (M ⧸ ker f)
x : M
⊢ ↑(↑(comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f'))) φ) x = ↑(↑(dualMap (mkQ (ker f))) φ) x
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f')) = dualMap (mkQ (ker f))
ext (φ x)
no goals
case h.h.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
φ : Dual R (M ⧸ ker f)
x : M
⊢ ↑(↑(comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f'))) φ) x = ↑(↑(dualMap (mkQ (ker f))) φ) x
simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, LinearMap.dualMap_apply,
  LinearEquiv.dualMap_apply, mkQ_apply, LinearMap.quotKerEquivOfSurjective,
  LinearEquiv.trans_symm, LinearEquiv.trans_apply, LinearEquiv.ofTop_symm_apply,
  LinearMap.quotKerEquivRange_symm_apply_image, mkQ_apply, Function.comp]