case intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ ↑(dualMap f) ψ ∈ Submodule.dualAnnihilator (ker f)
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ range (dualMap f) ≤ Submodule.dualAnnihilator (ker f)
rintro _ ⟨ψ, rfl⟩
case intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ ∀ (w : M₁), ↑f w = 0 → ↑(↑(dualMap f) ψ) w = 0
case intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ ↑(dualMap f) ψ ∈ Submodule.dualAnnihilator (ker f)
simp_rw [Submodule.mem_dualAnnihilator, mem_ker]
case intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
x : M₁
hx : ↑f x = 0
⊢ ↑(↑(dualMap f) ψ) x = 0
case intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ ∀ (w : M₁), ↑f w = 0 → ↑(↑(dualMap f) ψ) w = 0
rintro x hx
no goals
case intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
x : M₁
hx : ↑f x = 0
⊢ ↑(↑(dualMap f) ψ) x = 0
rw [dualMap_apply, hx, map_zero]