case h
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ φ ∈ LinearMap.range (LinearMap.dualMap (mkQ W)) ↔ φ ∈ dualAnnihilator W
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ LinearMap.range (LinearMap.dualMap (mkQ W)) = dualAnnihilator W
ext φ
case h
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ (∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ) ↔ φ ∈ dualAnnihilator W
case h
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ φ ∈ LinearMap.range (LinearMap.dualMap (mkQ W)) ↔ φ ∈ dualAnnihilator W
rw [LinearMap.mem_range]
case h.mp
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ (∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ) → φ ∈ dualAnnihilator W

case h.mpr
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ φ ∈ dualAnnihilator W → ∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ
case h
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ (∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ) ↔ φ ∈ dualAnnihilator W
constructor
case h.mp.intro
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
ψ : Dual R (M ⧸ W)
⊢ ↑(LinearMap.dualMap (mkQ W)) ψ ∈ dualAnnihilator W
case h.mp
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ (∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ) → φ ∈ dualAnnihilator W
rintro ⟨ψ, rfl⟩
case h.mp.intro
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
ψ : Dual R (M ⧸ W)
this : ↑(LinearMap.dualMap (mkQ W)) ψ ∈ LinearMap.range (LinearMap.dualMap (mkQ W))
⊢ ↑(LinearMap.dualMap (mkQ W)) ψ ∈ dualAnnihilator W
case h.mp.intro
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
ψ : Dual R (M ⧸ W)
⊢ ↑(LinearMap.dualMap (mkQ W)) ψ ∈ dualAnnihilator W
have := LinearMap.mem_range_self W.mkQ.dualMap ψ
no goals
case h.mp.intro
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
ψ : Dual R (M ⧸ W)
this : ↑(LinearMap.dualMap (mkQ W)) ψ ∈ LinearMap.range (LinearMap.dualMap (mkQ W))
⊢ ↑(LinearMap.dualMap (mkQ W)) ψ ∈ dualAnnihilator W
simpa only [ker_mkQ] using LinearMap.range_dualMap_le_dualAnnihilator_ker W.mkQ this
case h.mpr
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
hφ : φ ∈ dualAnnihilator W
⊢ ∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ
case h.mpr
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ φ ∈ dualAnnihilator W → ∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ
intro hφ
no goals
case h.mpr
R : Type u_1
M : Type u_2
M' : Type ?u.1403652
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
hφ : φ ∈ dualAnnihilator W
⊢ ∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ
exists W.dualCopairing ⟨φ, hφ⟩