From 591c34b6f59f9bf4629a3edd0568744d0ae5b04a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 19 Mar 2021 14:35:20 +0000 Subject: [PATCH] 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`. --- src/algebra/module/submodule_lattice.lean | 181 ++++++++++++++++++++++ src/linear_algebra/basic.lean | 148 +----------------- 2 files changed, 183 insertions(+), 146 deletions(-) create mode 100644 src/algebra/module/submodule_lattice.lean diff --git a/src/algebra/module/submodule_lattice.lean b/src/algebra/module/submodule_lattice.lean new file mode 100644 index 0000000000000..d31a37ae57f82 --- /dev/null +++ b/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 diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index 92bcae1154215..60006b12a9635 100644 --- a/src/linear_algebra/basic.lean +++ b/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 :=