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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
⊢ range (dualMap f) = dualAnnihilator (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 ↑(dualMap (Submodule.subtype (range f)))
⊢ range (dualMap f) = dualAnnihilator (ker f)
have rr_surj : Function.Surjective f.rangeRestrict := by
  rw [← LinearMap.range_eq_top, LinearMap.range_rangeRestrict]
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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap f) = dualAnnihilator (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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
⊢ range (dualMap f) = dualAnnihilator (ker f)
have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj
case h.e'_2
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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap f) = range (dualMap (rangeRestrict f))

case h.e'_3
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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ dualAnnihilator (ker f) = dualAnnihilator (ker (rangeRestrict 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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap f) = dualAnnihilator (ker f)
convert this using 1
no goals
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 ↑(dualMap (Submodule.subtype (range f)))
⊢ Function.Surjective ↑(rangeRestrict f)
rw [← LinearMap.range_eq_top, LinearMap.range_rangeRestrict]
case h.e'_2
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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap (comp (Submodule.subtype (range f)) (rangeRestrict f))) = range (dualMap (rangeRestrict f))
case h.e'_2
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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap f) = range (dualMap (rangeRestrict f))
change LinearMap.range
  ((Submodule.subtype <| LinearMap.range f).comp f.rangeRestrict).dualMap = _
case h.e'_2.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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap (Submodule.subtype (range f))) = ⊤
case h.e'_2
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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap (comp (Submodule.subtype (range f)) (rangeRestrict f))) = range (dualMap (rangeRestrict f))
rw [← LinearMap.dualMap_comp_dualMap, LinearMap.range_comp_of_range_eq_top]
no goals
case h.e'_2.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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap (Submodule.subtype (range f))) = ⊤
rwa [LinearMap.range_eq_top]
case h.e'_3.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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ ker f = ker (rangeRestrict f)
case h.e'_3
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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ dualAnnihilator (ker f) = dualAnnihilator (ker (rangeRestrict f))
apply congr_arg
no goals
case h.e'_3.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 ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ ker f = ker (rangeRestrict f)
exact (LinearMap.ker_rangeRestrict f).symm