refactor(linear_algebra/basic): move the lattice structure to its own file (#6767)

The entire lattice structure is thoroughly uninteresting.
By moving it to its own shorter file, it should be easier to unify with the lattice of `submonoid`

I'd hope in future we can generate this automatically for any `subobject A` with an injection into `set A`.

Author: eric-wieser

src/algebra/module/submodule_lattice.lean

@@ -0,0 +1,181 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
+-/
+import algebra.module.submodule
+
+/-!
+# The lattice structure on `submodule`s
+
+This file defines the lattice structure on submodules, `submodule.complete_lattice`, with `⊥`
+defined as `{0}` and `⊓` defined as intersection of the underlying carrier.
+If `p` and `q` are submodules of a module, `p ≤ q` means that `p ⊆ q`.
+
+Many results about operations on this lattice structure are defined in `linear_algebra/basic.lean`,
+most notably those which use `span`.
+
+## Implementation notes
+
+This structure should match the `add_submonoid.complete_lattice` structure, and we should try
+to unify the APIs where possible.
+
+-/
+
+variables {R : Type*} {M : Type*}
+
+section add_comm_monoid
+variables [semiring R] [add_comm_monoid M] [semimodule R M]
+variables {p q : submodule R M}
+
+namespace submodule
+
+instance : partial_order (submodule R M) :=
+{ le := λ p q, ∀ ⦃x⦄, x ∈ p → x ∈ q,
+  ..partial_order.lift (coe : submodule R M → set M) coe_injective }
+
+lemma le_def : p ≤ q ↔ (p : set M) ⊆ q := iff.rfl
+
+@[simp, norm_cast] lemma coe_subset_coe : (p : set M) ⊆ q ↔ p ≤ q := iff.rfl
+
+lemma le_def' : p ≤ q ↔ ∀ x ∈ p, x ∈ q := iff.rfl
+
+lemma lt_def : p < q ↔ (p : set M) ⊂ q := iff.rfl
+
+lemma not_le_iff_exists : ¬ (p ≤ q) ↔ ∃ x ∈ p, x ∉ q := set.not_subset
+
+lemma exists_of_lt {p q : submodule R M} : p < q → ∃ x ∈ q, x ∉ p := set.exists_of_ssubset
+
+lemma lt_iff_le_and_exists : p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p :=
+by rw [lt_iff_le_not_le, not_le_iff_exists]
+
+/-- The set `{0}` is the bottom element of the lattice of submodules. -/
+instance : has_bot (submodule R M) :=
+⟨{ carrier := {0}, smul_mem' := by simp { contextual := tt }, .. (⊥ : add_submonoid M)}⟩
+
+instance inhabited' : inhabited (submodule R M) := ⟨⊥⟩
+
+@[simp] lemma bot_coe : ((⊥ : submodule R M) : set M) = {0} := rfl
+@[simp] lemma bot_to_add_submonoid : (⊥ : submodule R M).to_add_submonoid = ⊥ := rfl
+
+section
+variables (R)
+@[simp] lemma mem_bot {x : M} : x ∈ (⊥ : submodule R M) ↔ x = 0 := set.mem_singleton_iff
+end
+
+instance unique_bot : unique (⊥ : submodule R M) :=
+⟨infer_instance, λ x, subtype.ext $ (mem_bot R).1 x.mem⟩
+
+lemma nonzero_mem_of_bot_lt {I : submodule R M} (bot_lt : ⊥ < I) : ∃ a : I, a ≠ 0 :=
+begin
+  have h := (submodule.lt_iff_le_and_exists.1 bot_lt).2,
+  tidy,
+end
+
+instance : order_bot (submodule R M) :=
+{ bot := ⊥,
+  bot_le := λ p x, by simp {contextual := tt},
+  ..submodule.partial_order }
+
+protected lemma eq_bot_iff (p : submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x = (0 : M) :=
+⟨ λ h, h.symm ▸ λ x hx, (mem_bot R).mp hx,
+  λ h, eq_bot_iff.mpr (λ x hx, (mem_bot R).mpr (h x hx)) ⟩
+
+protected lemma ne_bot_iff (p : submodule R M) : p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ (0 : M) :=
+by { haveI := classical.prop_decidable, simp_rw [ne.def, p.eq_bot_iff, not_forall] }
+
+/-- The universal set is the top element of the lattice of submodules. -/
+instance : has_top (submodule R M) :=
+⟨{ carrier := set.univ, smul_mem' := λ _ _ _, trivial, .. (⊤ : add_submonoid M)}⟩
+
+@[simp] lemma top_coe : ((⊤ : submodule R M) : set M) = set.univ := rfl
+
+@[simp] lemma top_to_add_submonoid : (⊤ : submodule R M).to_add_submonoid = ⊤ := rfl
+
+@[simp] lemma mem_top {x : M} : x ∈ (⊤ : submodule R M) := trivial
+
+instance : order_top (submodule R M) :=
+{ top := ⊤,
+  le_top := λ p x _, trivial,
+  ..submodule.partial_order }
+
+lemma eq_top_iff' {p : submodule R M} : p = ⊤ ↔ ∀ x, x ∈ p :=
+eq_top_iff.trans ⟨λ h x, h trivial, λ h x _, h x⟩
+
+instance : has_Inf (submodule R M) :=
+⟨λ S, {
+  carrier   := ⋂ s ∈ S, (s : set M),
+  zero_mem' := by simp,
+  add_mem'  := by simp [add_mem] {contextual := tt},
+  smul_mem' := by simp [smul_mem] {contextual := tt} }⟩
+
+private lemma Inf_le' {S : set (submodule R M)} {p} : p ∈ S → Inf S ≤ p :=
+set.bInter_subset_of_mem
+
+private lemma le_Inf' {S : set (submodule R M)} {p} : (∀q ∈ S, p ≤ q) → p ≤ Inf S :=
+set.subset_bInter
+
+instance : has_inf (submodule R M) :=
+⟨λ p q, {
+  carrier   := p ∩ q,
+  zero_mem' := by simp,
+  add_mem'  := by simp [add_mem] {contextual := tt},
+  smul_mem' := by simp [smul_mem] {contextual := tt} }⟩
+
+instance : complete_lattice (submodule R M) :=
+{ sup          := λ a b, Inf {x | a ≤ x ∧ b ≤ x},
+  le_sup_left  := λ a b, le_Inf' $ λ x ⟨ha, hb⟩, ha,
+  le_sup_right := λ a b, le_Inf' $ λ x ⟨ha, hb⟩, hb,
+  sup_le       := λ a b c h₁ h₂, Inf_le' ⟨h₁, h₂⟩,
+  inf          := (⊓),
+  le_inf       := λ a b c, set.subset_inter,
+  inf_le_left  := λ a b, set.inter_subset_left _ _,
+  inf_le_right := λ a b, set.inter_subset_right _ _,
+  Sup          := λtt, Inf {t | ∀t'∈tt, t' ≤ t},
+  le_Sup       := λ s p hs, le_Inf' $ λ q hq, hq _ hs,
+  Sup_le       := λ s p hs, Inf_le' hs,
+  Inf          := Inf,
+  le_Inf       := λ s a, le_Inf',
+  Inf_le       := λ s a, Inf_le',
+  ..submodule.order_top,
+  ..submodule.order_bot }
+
+@[simp] theorem inf_coe : (p ⊓ q : set M) = p ∩ q := rfl
+
+@[simp] theorem mem_inf {p q : submodule R M} {x : M} :
+  x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q := iff.rfl
+
+@[simp] theorem Inf_coe (P : set (submodule R M)) : (↑(Inf P) : set M) = ⋂ p ∈ P, ↑p := rfl
+
+@[simp] theorem infi_coe {ι} (p : ι → submodule R M) :
+  (↑⨅ i, p i : set M) = ⋂ i, ↑(p i) :=
+by rw [infi, Inf_coe]; ext a; simp; exact
+⟨λ h i, h _ i rfl, λ h i x e, e ▸ h _⟩
+
+@[simp] lemma mem_Inf {S : set (submodule R M)} {x : M} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p :=
+set.mem_bInter_iff
+
+@[simp] theorem mem_infi {ι} (p : ι → submodule R M) {x} :
+  x ∈ (⨅ i, p i) ↔ ∀ i, x ∈ p i :=
+by rw [← mem_coe, infi_coe, set.mem_Inter]; refl
+
+lemma mem_sup_left {S T : submodule R M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T :=
+show S ≤ S ⊔ T, from le_sup_left
+
+lemma mem_sup_right {S T : submodule R M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T :=
+show T ≤ S ⊔ T, from le_sup_right
+
+lemma mem_supr_of_mem {ι : Sort*} {b : M} {p : ι → submodule R M} (i : ι) (h : b ∈ p i) :
+  b ∈ (⨆i, p i) :=
+have p i ≤ (⨆i, p i) := le_supr p i,
+@this b h
+
+/-! Note that `submodule.mem_supr` is provided in `linear_algebra/basic.lean`. -/
+
+lemma mem_Sup_of_mem {S : set (submodule R M)} {s : submodule R M}
+  (hs : s ∈ S) : ∀ {x : M}, x ∈ s → x ∈ Sup S :=
+show s ≤ Sup S, from le_Sup hs
+
+end submodule
+
+end add_comm_monoid

src/linear_algebra/basic.lean

@@ -7,6 +7,7 @@ import algebra.big_operators.pi
 import algebra.module.pi
 import algebra.module.prod
 import algebra.module.submodule
+import algebra.module.submodule_lattice
 import algebra.group.prod
 import data.finsupp.basic
 import data.dfinsupp
@@ -17,8 +18,7 @@ import order.compactly_generated
 # Linear algebra
 
 This file defines the basics of linear algebra. It sets up the "categorical/lattice structure" of
-modules over a ring, submodules, and linear maps. If `p` and `q` are submodules of a module, `p ≤ q`
-means that `p ⊆ q`.
+modules over a ring, submodules, and linear maps.
 
 Many of the relevant definitions, including `module`, `submodule`, and `linear_map`, are found in
 `src/algebra/module`.
@@ -487,27 +487,8 @@ variables (p p' : submodule R M) (q q' : submodule R M₂)
 variables {r : R} {x y : M}
 open set
 
-instance : partial_order (submodule R M) :=
-{ le := λ p p', ∀ ⦃x⦄, x ∈ p → x ∈ p',
-  ..partial_order.lift (coe : submodule R M → set M) coe_injective }
-
 variables {p p'}
 
-lemma le_def : p ≤ p' ↔ (p : set M) ⊆ p' := iff.rfl
-
-@[simp, norm_cast] lemma coe_subset_coe : (p : set M) ⊆ p' ↔ p ≤ p' := iff.rfl
-
-lemma le_def' : p ≤ p' ↔ ∀ x ∈ p, x ∈ p' := iff.rfl
-
-lemma lt_def : p < p' ↔ (p : set M) ⊂ p' := iff.rfl
-
-lemma not_le_iff_exists : ¬ (p ≤ p') ↔ ∃ x ∈ p, x ∉ p' := not_subset
-
-lemma exists_of_lt {p p' : submodule R M} : p < p' → ∃ x ∈ p', x ∉ p := exists_of_ssubset
-
-lemma lt_iff_le_and_exists : p < p' ↔ p ≤ p' ∧ ∃ x ∈ p', x ∉ p :=
-by rw [lt_iff_le_not_le, not_le_iff_exists]
-
 /-- If two submodules `p` and `p'` satisfy `p ⊆ p'`, then `of_le p p'` is the linear map version of
 this inclusion. -/
 def of_le (h : p ≤ p') : p →ₗ[R] p' :=
@@ -524,90 +505,6 @@ lemma subtype_comp_of_le (p q : submodule R M) (h : p ≤ q) :
   q.subtype.comp (of_le h) = p.subtype :=
 by { ext ⟨b, hb⟩, refl }
 
-/-- The set `{0}` is the bottom element of the lattice of submodules. -/
-instance : has_bot (submodule R M) :=
-⟨{ carrier := {0}, smul_mem' := by simp { contextual := tt }, .. (⊥ : add_submonoid M)}⟩
-
-instance inhabited' : inhabited (submodule R M) := ⟨⊥⟩
-
-@[simp] lemma bot_coe : ((⊥ : submodule R M) : set M) = {0} := rfl
-
-section
-variables (R)
-@[simp] lemma mem_bot : x ∈ (⊥ : submodule R M) ↔ x = 0 := mem_singleton_iff
-end
-
-instance unique_bot : unique (⊥ : submodule R M) :=
-⟨infer_instance, λ x, subtype.ext $ (mem_bot R).1 x.mem⟩
-
-lemma nonzero_mem_of_bot_lt {I : submodule R M} (bot_lt : ⊥ < I) : ∃ a : I, a ≠ 0 :=
-begin
-  have h := (submodule.lt_iff_le_and_exists.1 bot_lt).2,
-  tidy,
-end
-
-instance : order_bot (submodule R M) :=
-{ bot := ⊥,
-  bot_le := λ p x, by simp {contextual := tt},
-  ..submodule.partial_order }
-
-protected lemma eq_bot_iff (p : submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x = (0 : M) :=
-⟨ λ h, h.symm ▸ λ x hx, (mem_bot R).mp hx,
-  λ h, eq_bot_iff.mpr (λ x hx, (mem_bot R).mpr (h x hx)) ⟩
-
-protected lemma ne_bot_iff (p : submodule R M) : p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ (0 : M) :=
-by { haveI := classical.prop_decidable, simp_rw [ne.def, p.eq_bot_iff, not_forall] }
-
-/-- The universal set is the top element of the lattice of submodules. -/
-instance : has_top (submodule R M) :=
-⟨{ carrier := univ, smul_mem' := λ _ _ _, trivial, .. (⊤ : add_submonoid M)}⟩
-
-@[simp] lemma top_coe : ((⊤ : submodule R M) : set M) = univ := rfl
-
-@[simp] lemma mem_top : x ∈ (⊤ : submodule R M) := trivial
-
-instance : order_top (submodule R M) :=
-{ top := ⊤,
-  le_top := λ p x _, trivial,
-  ..submodule.partial_order }
-
-instance : has_Inf (submodule R M) :=
-⟨λ S, {
-  carrier   := ⋂ s ∈ S, (s : set M),
-  zero_mem' := by simp,
-  add_mem'  := by simp [add_mem] {contextual := tt},
-  smul_mem' := by simp [smul_mem] {contextual := tt} }⟩
-
-private lemma Inf_le' {S : set (submodule R M)} {p} : p ∈ S → Inf S ≤ p :=
-bInter_subset_of_mem
-
-private lemma le_Inf' {S : set (submodule R M)} {p} : (∀p' ∈ S, p ≤ p') → p ≤ Inf S :=
-subset_bInter
-
-instance : has_inf (submodule R M) :=
-⟨λ p p', {
-  carrier   := p ∩ p',
-  zero_mem' := by simp,
-  add_mem'  := by simp [add_mem] {contextual := tt},
-  smul_mem' := by simp [smul_mem] {contextual := tt} }⟩
-
-instance : complete_lattice (submodule R M) :=
-{ sup          := λ a b, Inf {x | a ≤ x ∧ b ≤ x},
-  le_sup_left  := λ a b, le_Inf' $ λ x ⟨ha, hb⟩, ha,
-  le_sup_right := λ a b, le_Inf' $ λ x ⟨ha, hb⟩, hb,
-  sup_le       := λ a b c h₁ h₂, Inf_le' ⟨h₁, h₂⟩,
-  inf          := (⊓),
-  le_inf       := λ a b c, subset_inter,
-  inf_le_left  := λ a b, inter_subset_left _ _,
-  inf_le_right := λ a b, inter_subset_right _ _,
-  Sup          := λtt, Inf {t | ∀t'∈tt, t' ≤ t},
-  le_Sup       := λ s p hs, le_Inf' $ λ p' hp', hp' _ hs,
-  Sup_le       := λ s p hs, Inf_le' hs,
-  Inf          := Inf,
-  le_Inf       := λ s a, le_Inf',
-  Inf_le       := λ s a, Inf_le',
-  ..submodule.order_top,
-  ..submodule.order_bot }
 
 instance add_comm_monoid_submodule : add_comm_monoid (submodule R M) :=
 { add := (⊔),
@@ -620,15 +517,8 @@ instance add_comm_monoid_submodule : add_comm_monoid (submodule R M) :=
 @[simp] lemma add_eq_sup (p q : submodule R M) : p + q = p ⊔ q := rfl
 @[simp] lemma zero_eq_bot : (0 : submodule R M) = ⊥ := rfl
 
-lemma eq_top_iff' {p : submodule R M} : p = ⊤ ↔ ∀ x, x ∈ p :=
-eq_top_iff.trans ⟨λ h x, @h x trivial, λ h x _, h x⟩
-
 variables (R)
 
-@[simp] lemma bot_to_add_submonoid : (⊥ : submodule R M).to_add_submonoid = ⊥ := rfl
-
-@[simp] lemma top_to_add_submonoid : (⊤ : submodule R M).to_add_submonoid = ⊤ := rfl
-
 lemma subsingleton_iff : subsingleton M ↔ subsingleton (submodule R M) :=
 add_submonoid.subsingleton_iff.trans $ begin
   rw [←subsingleton_iff_bot_eq_top, ←subsingleton_iff_bot_eq_top],
@@ -650,25 +540,6 @@ by haveI := semimodule.subsingleton R M; apply_instance
 
 instance [nontrivial M] : nontrivial (submodule R M) := (nontrivial_iff R).mp ‹_›
 
-@[simp] theorem inf_coe : (p ⊓ p' : set M) = p ∩ p' := rfl
-
-@[simp] theorem mem_inf {p p' : submodule R M} :
-  x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' := iff.rfl
-
-@[simp] theorem Inf_coe (P : set (submodule R M)) : (↑(Inf P) : set M) = ⋂ p ∈ P, ↑p := rfl
-
-@[simp] theorem infi_coe {ι} (p : ι → submodule R M) :
-  (↑⨅ i, p i : set M) = ⋂ i, ↑(p i) :=
-by rw [infi, Inf_coe]; ext a; simp; exact
-⟨λ h i, h _ i rfl, λ h i x e, e ▸ h _⟩
-
-@[simp] lemma mem_Inf {S : set (submodule R M)} {x : M} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p :=
-set.mem_bInter_iff
-
-@[simp] theorem mem_infi {ι} (p : ι → submodule R M) :
-  x ∈ (⨅ i, p i) ↔ ∀ i, x ∈ p i :=
-by rw [← mem_coe, infi_coe, mem_Inter]; refl
-
 theorem disjoint_def {p p' : submodule R M} :
   disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = (0:M) :=
 show (∀ x, x ∈ p ∧ x ∈ p' → x ∈ ({0} : set M)) ↔ _, by simp
@@ -875,17 +746,6 @@ begin
   { exact λ a x i hi, ⟨i, smul_mem _ a hi⟩ },
 end
 
-lemma mem_sup_left {S T : submodule R M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T :=
-show S ≤ S ⊔ T, from le_sup_left
-
-lemma mem_sup_right {S T : submodule R M} : ∀ {x : M}, x ∈ T → x ∈ S ⊔ T :=
-show T ≤ S ⊔ T, from le_sup_right
-
-lemma mem_supr_of_mem {ι : Sort*} {b : M} {p : ι → submodule R M} (i : ι) (h : b ∈ p i) :
-  b ∈ (⨆i, p i) :=
-have p i ≤ (⨆i, p i) := le_supr p i,
-@this b h
-
 lemma sum_mem_bsupr {ι : Type*} {s : finset ι} {f : ι → M} {p : ι → submodule R M}
   (h : ∀ i ∈ s, f i ∈ p i) :
   ∑ i in s, f i ∈ ⨆ i ∈ s, p i :=
@@ -896,10 +756,6 @@ lemma sum_mem_supr {ι : Type*} [fintype ι] {f : ι → M} {p : ι → submodul
   ∑ i, f i ∈ ⨆ i, p i :=
 sum_mem _ $ λ i hi, mem_supr_of_mem i (h i)
 
-lemma mem_Sup_of_mem {S : set (submodule R M)} {s : submodule R M}
-  (hs : s ∈ S) : ∀ {x : M}, x ∈ s → x ∈ Sup S :=
-show s ≤ Sup S, from le_Sup hs
-
 @[simp] theorem mem_supr_of_directed {ι} [nonempty ι]
   (S : ι → submodule R M) (H : directed (≤) S) {x} :
   x ∈ supr S ↔ ∃ i, x ∈ S i :=