case h
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₂
⊢ φ ∈ ker (dualMap f) ↔ φ ∈ Submodule.dualAnnihilator (range 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₂
⊢ ker (dualMap f) = Submodule.dualAnnihilator (range f)
ext φ
case h.mp
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₂
hφ : φ ∈ ker (dualMap f)
⊢ φ ∈ Submodule.dualAnnihilator (range f)

case h.mpr
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₂
hφ : φ ∈ Submodule.dualAnnihilator (range f)
⊢ φ ∈ ker (dualMap f)
case h
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₂
⊢ φ ∈ ker (dualMap f) ↔ φ ∈ Submodule.dualAnnihilator (range f)
constructor <;> intro hφ
case h.mp
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₂
hφ : ↑(dualMap f) φ = 0
⊢ φ ∈ Submodule.dualAnnihilator (range f)
case h.mp
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₂
hφ : φ ∈ ker (dualMap f)
⊢ φ ∈ Submodule.dualAnnihilator (range f)
rw [mem_ker] at hφ
case h.mp
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₂
hφ : ↑(dualMap f) φ = 0
⊢ ∀ (w : M₂), w ∈ range f → ↑φ w = 0
case h.mp
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₂
hφ : ↑(dualMap f) φ = 0
⊢ φ ∈ Submodule.dualAnnihilator (range f)
rw [Submodule.mem_dualAnnihilator]
case h.mp.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₂
hφ : ↑(dualMap f) φ = 0
x : M₁
⊢ ↑φ (↑f x) = 0
case h.mp
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₂
hφ : ↑(dualMap f) φ = 0
⊢ ∀ (w : M₂), w ∈ range f → ↑φ w = 0
rintro y ⟨x, rfl⟩
no goals
case h.mp.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₂
hφ : ↑(dualMap f) φ = 0
x : M₁
⊢ ↑φ (↑f x) = 0
rw [← dualMap_apply, hφ, zero_apply]
case h.mpr.h
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₂
hφ : φ ∈ Submodule.dualAnnihilator (range f)
x : M₁
⊢ ↑(↑(dualMap f) φ) x = ↑0 x
case h.mpr
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₂
hφ : φ ∈ Submodule.dualAnnihilator (range f)
⊢ φ ∈ ker (dualMap f)
ext x
case h.mpr.h
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₂
hφ : φ ∈ Submodule.dualAnnihilator (range f)
x : M₁
⊢ ↑φ (↑f x) = ↑0 x
case h.mpr.h
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₂
hφ : φ ∈ Submodule.dualAnnihilator (range f)
x : M₁
⊢ ↑(↑(dualMap f) φ) x = ↑0 x
rw [dualMap_apply]
case h.mpr.h
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₂
hφ : ∀ (w : M₂), w ∈ range f → ↑φ w = 0
x : M₁
⊢ ↑φ (↑f x) = ↑0 x
case h.mpr.h
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₂
hφ : φ ∈ Submodule.dualAnnihilator (range f)
x : M₁
⊢ ↑φ (↑f x) = ↑0 x
rw [Submodule.mem_dualAnnihilator] at hφ
no goals
case h.mpr.h
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₂
hφ : ∀ (w : M₂), w ∈ range f → ↑φ w = 0
x : M₁
⊢ ↑φ (↑f x) = ↑0 x
exact hφ (f x) ⟨x, rfl⟩