feat(linear_algebra/affine_space): lattice structure on affine subspaces (#3288)

Define a `complete_lattice` instance on affine subspaces of an affine
space, and prove a few basic lemmas relating to it.  (There are plenty
more things that could be proved about it, that I think can reasonably
be added later.)

Author: jsm28

src/algebra/add_torsor.lean

@@ -220,6 +220,14 @@ by rw [←vsub_vadd_eq_vsub_sub, vsub_vadd]
 /-- The pairwise differences of a set of points. -/
 def vsub_set (s : set P) : set G := {g | ∃ x ∈ s, ∃ y ∈ s, g = x -ᵥ y}
 
+/-- `vsub_set` of an empty set. -/
+@[simp] lemma vsub_set_empty : vsub_set G (∅ : set P) = ∅ :=
+begin
+  rw set.eq_empty_iff_forall_not_mem,
+  rintros g ⟨p, hp, hg⟩,
+  exact hp
+end
+
 /-- Each pairwise difference is in the `vsub_set`. -/
 lemma vsub_mem_vsub_set {p1 p2 : P} {s : set P} (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) :
   (p1 -ᵥ p2) ∈ vsub_set G s :=

src/linear_algebra/affine_space.lean

@@ -49,13 +49,16 @@ add_torsor V P
 namespace affine_space
 
 variables (k : Type*) (V : Type*) {P : Type*} [ring k] [add_comm_group V] [module k V]
-variables [S : affine_space k V P]
-include S
+variables [affine_space k V P]
 
 /-- The submodule spanning the differences of a (possibly empty) set
 of points. -/
 def vector_span (s : set P) : submodule k V := submodule.span k (vsub_set V s)
 
+/-- The definition of `vector_span`, for rewriting. -/
+lemma vector_span_def (s : set P) : vector_span k V s = submodule.span k (vsub_set V s) :=
+rfl
+
 /-- The `vsub_set` lies within the `vector_span`. -/
 lemma vsub_set_subset_vector_span (s : set P) : vsub_set V s ⊆ vector_span k V s :=
 submodule.subset_span
@@ -334,8 +337,7 @@ structure affine_subspace (k : Type*) (V : Type*) (P : Type*) [ring k] [add_comm
 namespace affine_subspace
 
 variables (k : Type*) (V : Type*) (P : Type*) [ring k] [add_comm_group V] [module k V]
-          [S : affine_space k V P]
-include S
+          [affine_space k V P]
 
 instance : has_coe (affine_subspace k V P) (set P) := ⟨carrier⟩
 instance : has_mem P (affine_subspace k V P) := ⟨λ p s, p ∈ (s : set P)⟩
@@ -346,21 +348,6 @@ it is in that affine subspace. -/
   p ∈ (s : set P) ↔ p ∈ s :=
 iff.rfl
 
-/-- The whole affine space as a subspace of itself. -/
-def univ : affine_subspace k V P :=
-{ carrier := set.univ,
-  smul_vsub_vadd_mem := λ _ _ _ _ _ _ _, set.mem_univ _ }
-
-/-- `univ`, coerced to a set, is the whole set of points. -/
-@[simp] lemma univ_coe : (univ k V P : set P) = set.univ :=
-rfl
-
-/-- All points are in `univ`. -/
-lemma mem_univ (p : P) : p ∈ univ k V P :=
-set.mem_univ p
-
-instance : inhabited (affine_subspace k V P) := ⟨univ k V P⟩
-
 variables {k V P}
 
 /-- The direction of an affine subspace is the submodule spanned by
@@ -523,6 +510,21 @@ that subspace's direction yields the original subspace. -/
 ext_of_direction_eq (direction_mk' p s.direction)
                     ⟨p, set.mem_inter (self_mem_mk' _ _) hp⟩
 
+/-- If an affine subspace contains a set of points, it contains the
+`span_points` of that set. -/
+lemma span_points_subset_coe_of_subset_coe {s : set P} {s1 : affine_subspace k V P} (h : s ⊆ s1) :
+  span_points k V s ⊆ s1 :=
+begin
+  rintros p ⟨p1, hp1, v, hv, hp⟩,
+  rw hp,
+  have hp1s1 : p1 ∈ (s1 : set P) := set.mem_of_mem_of_subset hp1 h,
+  refine vadd_mem_of_mem_direction _ hp1s1,
+  have hs : vector_span k V s ≤ s1.direction := submodule.span_mono (vsub_set_mono V h),
+  rw submodule.le_def at hs,
+  rw ←submodule.mem_coe,
+  exact set.mem_of_mem_of_subset hv hs
+end
+
 end affine_subspace
 
 section affine_span
@@ -563,6 +565,176 @@ mem_span_points k V p s hp
 
 end affine_span
 
+namespace affine_subspace
+
+variables (k : Type*) (V : Type*) (P : Type*) [ring k] [add_comm_group V] [module k V]
+          [S : affine_space k V P]
+include S
+
+instance : complete_lattice (affine_subspace k V P) :=
+{ sup := λ s1 s2, affine_span k V (s1 ∪ s2),
+  le_sup_left := λ s1 s2, set.subset.trans (set.subset_union_left s1 s2)
+                                           (subset_span_points k V _),
+  le_sup_right :=  λ s1 s2, set.subset.trans (set.subset_union_right s1 s2)
+                                             (subset_span_points k V _),
+  sup_le := λ s1 s2 s3 hs1 hs2, span_points_subset_coe_of_subset_coe (set.union_subset hs1 hs2),
+  inf := λ s1 s2, mk (s1 ∩ s2)
+                     (λ c p1 p2 p3 hp1 hp2 hp3,
+                       ⟨s1.smul_vsub_vadd_mem c p1 p2 p3 hp1.1 hp2.1 hp3.1,
+                       s2.smul_vsub_vadd_mem c p1 p2 p3 hp1.2 hp2.2 hp3.2⟩),
+  inf_le_left := λ _ _, set.inter_subset_left _ _,
+  inf_le_right := λ _ _, set.inter_subset_right _ _,
+  le_inf := λ _ _ _, set.subset_inter,
+  top := { carrier := set.univ,
+    smul_vsub_vadd_mem := λ _ _ _ _ _ _ _, set.mem_univ _ },
+  le_top := λ _ _ _, set.mem_univ _,
+  bot := { carrier := ∅,
+    smul_vsub_vadd_mem := λ _ _ _ _, false.elim },
+  bot_le := λ _ _, false.elim,
+  Sup := λ s, affine_span k V (⋃ s' ∈ s, (s' : set P)),
+  Inf := λ s, mk (⋂ s' ∈ s, (s' : set P))
+                 (λ c p1 p2 p3 hp1 hp2 hp3, set.mem_bInter_iff.2 $ λ s2 hs2,
+                   s2.smul_vsub_vadd_mem c p1 p2 p3 (set.mem_bInter_iff.1 hp1 s2 hs2)
+                                                    (set.mem_bInter_iff.1 hp2 s2 hs2)
+                                                    (set.mem_bInter_iff.1 hp3 s2 hs2)),
+  le_Sup := λ _ _ h, set.subset.trans (set.subset_bUnion_of_mem h) (subset_span_points k V _),
+  Sup_le := λ _ _ h, span_points_subset_coe_of_subset_coe (set.bUnion_subset h),
+  Inf_le := λ _ _, set.bInter_subset_of_mem,
+  le_Inf := λ _ _, set.subset_bInter,
+  .. partial_order.lift (coe : affine_subspace k V P → set P) (λ _ _, ext) }
+
+instance : inhabited (affine_subspace k V P) := ⟨⊤⟩
+
+/-- The `≤` order on subspaces is the same as that on the corresponding
+sets. -/
+lemma le_def (s1 s2 : affine_subspace k V P) : s1 ≤ s2 ↔ (s1 : set P) ⊆ s2 :=
+iff.rfl
+
+/-- One subspace is less than or equal to another if and only if all
+its points are in the second subspace. -/
+lemma le_def' (s1 s2 : affine_subspace k V P) : s1 ≤ s2 ↔ ∀ p ∈ s1, p ∈ s2 :=
+iff.rfl
+
+/-- The `<` order on subspaces is the same as that on the corresponding
+sets. -/
+lemma lt_def (s1 s2 : affine_subspace k V P) : s1 < s2 ↔ (s1 : set P) ⊂ s2 :=
+iff.rfl
+
+/-- One subspace is not less than or equal to another if and only if
+it has a point not in the second subspace. -/
+lemma not_le_iff_exists (s1 s2 : affine_subspace k V P) : ¬ s1 ≤ s2 ↔ ∃ p ∈ s1, p ∉ s2 :=
+set.not_subset
+
+/-- If a subspace is less than another, there is a point only in the
+second. -/
+lemma exists_of_lt {s1 s2 : affine_subspace k V P} (h : s1 < s2) : ∃ p ∈ s2, p ∉ s1 :=
+set.exists_of_ssubset h
+
+/-- A subspace is less than another if and only if it is less than or
+equal to the second subspace and there is a point only in the
+second. -/
+lemma lt_iff_le_and_exists (s1 s2 : affine_subspace k V P) : s1 < s2 ↔ s1 ≤ s2 ∧ ∃ p ∈ s2, p ∉ s1 :=
+by rw [lt_iff_le_not_le, not_le_iff_exists]
+
+variables {P}
+
+/-- The affine span is the `Inf` of subspaces containing the given
+points. -/
+lemma affine_span_eq_Inf (s : set P) : affine_span k V s = Inf {s' | s ⊆ s'} :=
+le_antisymm (span_points_subset_coe_of_subset_coe (set.subset_bInter (λ _ h, h)))
+            (Inf_le (subset_span_points k V _))
+
+variables (P)
+
+/-- The Galois insertion formed by `affine_span` and coercion back to
+a set. -/
+protected def gi : galois_insertion (affine_span k V) (coe : affine_subspace k V P → set P) :=
+{ choice := λ s _, affine_span k V s,
+  gc := λ s1 s2, ⟨λ h, set.subset.trans (subset_span_points k V s1) h,
+                       span_points_subset_coe_of_subset_coe⟩,
+  le_l_u := λ _, subset_span_points k V _,
+  choice_eq := λ _ _, rfl }
+
+/-- The span of the empty set is `⊥`. -/
+@[simp] lemma span_empty : affine_span k V (∅ : set P) = ⊥ :=
+(affine_subspace.gi k V P).gc.l_bot
+
+/-- The span of `univ` is `⊤`. -/
+@[simp] lemma span_univ : affine_span k V (set.univ : set P) = ⊤ :=
+eq_top_iff.2 $ subset_span_points k V _
+
+/-- The span of a union of sets is the sup of their spans. -/
+lemma span_union (s t : set P) : affine_span k V (s ∪ t) = affine_span k V s ⊔ affine_span k V t :=
+(affine_subspace.gi k V P).gc.l_sup
+
+/-- The span of a union of an indexed family of sets is the sup of
+their spans. -/
+lemma span_Union {ι : Type*} (s : ι → set P) :
+  affine_span k V (⋃ i, s i) = ⨆ i, affine_span k V (s i) :=
+(affine_subspace.gi k V P).gc.l_supr
+
+/-- `⊤`, coerced to a set, is the whole set of points. -/
+@[simp] lemma top_coe : ((⊤ : affine_subspace k V P) : set P) = set.univ :=
+rfl
+
+variables {P}
+
+/-- All points are in `⊤`. -/
+lemma mem_top (p : P) : p ∈ (⊤ : affine_subspace k V P) :=
+set.mem_univ p
+
+variables (P)
+
+/-- The direction of `⊤` is the whole module as a submodule. -/
+@[simp] lemma direction_top : (⊤ : affine_subspace k V P).direction = ⊤ :=
+begin
+  cases S.nonempty with p,
+  ext v,
+  refine ⟨imp_intro submodule.mem_top, λ hv, _⟩,
+  have hpv : (v +ᵥ p -ᵥ p : V) ∈ (⊤ : affine_subspace k V P).direction :=
+    vsub_mem_direction (mem_top k V _) (mem_top k V _),
+  rwa vadd_vsub at hpv
+end
+
+/-- `⊥`, coerced to a set, is the empty set. -/
+@[simp] lemma bot_coe : ((⊥ : affine_subspace k V P) : set P) = ∅ :=
+rfl
+
+variables {P}
+
+/-- No points are in `⊥`. -/
+lemma not_mem_bot (p : P) : p ∉ (⊥ : affine_subspace k V P) :=
+set.not_mem_empty p
+
+variables (P)
+
+/-- The direction of `⊥` is the submodule `⊥`. -/
+@[simp] lemma direction_bot : (⊥ : affine_subspace k V P).direction = ⊥ :=
+by rw [direction_eq_vector_span, bot_coe, vector_span_def, vsub_set_empty, submodule.span_empty]
+
+/-- The inf of two affine subspaces, coerced to a set, is the
+intersection of the two sets of points. -/
+@[simp] lemma inf_coe (s1 s2 : affine_subspace k V P) : ((s1 ⊓ s2) : set P) = s1 ∩ s2 :=
+rfl
+
+/-- A point is in the inf of two affine subspaces if and only if it is
+in both of them. -/
+lemma mem_inf_iff (p : P) (s1 s2 : affine_subspace k V P) : p ∈ s1 ⊓ s2 ↔ p ∈ s1 ∧ p ∈ s2 :=
+iff.rfl
+
+/-- The direction of the inf of two affine subspaces is less than or
+equal to the inf of their directions. -/
+lemma direction_inf (s1 s2 : affine_subspace k V P) :
+  (s1 ⊓ s2).direction ≤ s1.direction ⊓ s2.direction :=
+begin
+  repeat { rw [direction_eq_vector_span, vector_span_def] },
+  exact le_inf
+    (Inf_le_Inf (λ p hp, set.subset.trans (vsub_set_mono V (set.inter_subset_left _ _)) hp))
+    (Inf_le_Inf (λ p hp, set.subset.trans (vsub_set_mono V (set.inter_subset_right _ _)) hp))
+end
+
+end affine_subspace
+
 /-- An `affine_map k V1 P1 V2 P2` is a map from `P1` to `P2` that
 induces a corresponding linear map from `V1` to `V2`. -/
 structure affine_map (k : Type*) (V1 : Type*) (P1 : Type*) (V2 : Type*) (P2 : Type*)