R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
b : (Submodule R (Module.Dual R M))ᵒᵈ
⊢ (↑OrderDual.toDual ∘ dualAnnihilator) a ≤ b ↔ a ≤ (dualCoannihilator ∘ ↑OrderDual.ofDual) b
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ GaloisConnection (↑OrderDual.toDual ∘ dualAnnihilator) (dualCoannihilator ∘ ↑OrderDual.ofDual)
intro a b
case h₂
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
⊢ (↑OrderDual.toDual ∘ dualAnnihilator) a ≤ ↑OrderDual.toDual a✝ ↔
    a ≤ (dualCoannihilator ∘ ↑OrderDual.ofDual) (↑OrderDual.toDual a✝)
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
b : (Submodule R (Module.Dual R M))ᵒᵈ
⊢ (↑OrderDual.toDual ∘ dualAnnihilator) a ≤ b ↔ a ≤ (dualCoannihilator ∘ ↑OrderDual.ofDual) b
induction b using OrderDual.rec
case h₂
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
⊢ a✝ ≤ dualAnnihilator a ↔ a ≤ dualCoannihilator a✝
case h₂
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
⊢ (↑OrderDual.toDual ∘ dualAnnihilator) a ≤ ↑OrderDual.toDual a✝ ↔
    a ≤ (dualCoannihilator ∘ ↑OrderDual.ofDual) (↑OrderDual.toDual a✝)
simp only [Function.comp_apply, OrderDual.toDual_le_toDual, OrderDual.ofDual_toDual]
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
⊢ x ∈ dualAnnihilator a
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
⊢ a ≤ dualCoannihilator a✝ → a✝ ≤ dualAnnihilator a
intro h x hx
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
⊢ ∀ (w : M), w ∈ a → ↑x w = 0
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
⊢ x ∈ dualAnnihilator a
simp only [mem_dualAnnihilator, mem_dualCoannihilator]
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
⊢ ↑x y = 0
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
⊢ ∀ (w : M), w ∈ a → ↑x w = 0
intro y hy
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : y ∈ dualCoannihilator a✝
⊢ ↑x y = 0
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
⊢ ↑x y = 0
have := h hy
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : ∀ (φ : Module.Dual R M), φ ∈ a✝ → ↑φ y = 0
⊢ ↑x y = 0
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : y ∈ dualCoannihilator a✝
⊢ ↑x y = 0
simp only [mem_dualAnnihilator, mem_dualCoannihilator] at this
no goals
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : ∀ (φ : Module.Dual R M), φ ∈ a✝ → ↑φ y = 0
⊢ ↑x y = 0
exact this x hx