feat(LinearAlgebra/AffineSpace/AffineSubspace): using AffineSubspace.direction to reinterpret AffineSubspace as Submodule (leanprover-community#38731)

* add `AffineSubspace.vsub_self_of_zero_mem` that states `s -ᵥ s = s ` if `0 ∈ s`
* add `AffineSubspace.direction_eq_self_iff_zero_mem` that states that `0 ∈ s` iff the directions coerce back to the affine subspace. 
* add corresponding `CanLift` instance.
* modify doc-string of `AffineSubspace.direction` to state that this can be used for reinterpretation of an affine subspace as a submodule.
* add `Coe` instance based on `Submodule.toAffineSubspace` and adds corresponding @[coe] attribute. 

The PR also performs a slight cleanup of the file: statements about `SetLike` or `Submodule.toAffineSubspace` have been moved closer to their respective definitions. Because the PR was temporarily broken, I also added

* the lemma `carrier_eq_coe (s : AffineSubspace k P) : s.carrier = s`

Co-authored-by: Martin Winter <martin.winter.math@gmail.com>

Author: martinwintermath

Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean

@@ -154,17 +154,6 @@ structure AffineSubspace (k : Type*) {V : Type*} (P : Type*) [Ring k] [AddCommGr
     ∀ (c : k) {p₁ p₂ p₃ : P},
       p₁ ∈ carrier → p₂ ∈ carrier → p₃ ∈ carrier → c • (p₁ -ᵥ p₂ : V) +ᵥ p₃ ∈ carrier
 
-namespace Submodule
-
-variable {k V : Type*} [Ring k] [AddCommGroup V] [Module k V]
-
-/-- Reinterpret `p : Submodule k V` as an `AffineSubspace k V`. -/
-def toAffineSubspace (p : Submodule k V) : AffineSubspace k V where
-  carrier := p
-  smul_vsub_vadd_mem _ _ _ _ h₁ h₂ h₃ := p.add_mem (p.smul_mem _ (p.sub_mem h₁ h₂)) h₃
-
-end Submodule
-
 namespace AffineSubspace
 
 variable (k : Type*) {V : Type*} (P : Type*) [Ring k] [AddCommGroup V] [Module k V]
@@ -176,17 +165,74 @@ instance : SetLike (AffineSubspace k P) P where
 
 instance : PartialOrder (AffineSubspace k P) := .ofSetLike (AffineSubspace k P) P
 
+@[simp] lemma carrier_eq_coe (s : AffineSubspace k P) : s.carrier = s := rfl
+
 /-- A point is in an affine subspace coerced to a set if and only if it is in that affine
 subspace. -/
 theorem mem_coe (p : P) (s : AffineSubspace k P) : p ∈ (s : Set P) ↔ p ∈ s := by simp
 
 variable {k P}
 
+/-- Two affine subspaces are equal if they have the same points. -/
+theorem coe_injective : Function.Injective ((↑) : AffineSubspace k P → Set P) :=
+  SetLike.coe_injective
+
+@[ext (iff := false)]
+theorem ext {p q : AffineSubspace k P} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q :=
+  SetLike.ext h
+
+protected theorem ext_iff (s₁ s₂ : AffineSubspace k P) : s₁ = s₂ ↔ (s₁ : Set P) = s₂ :=
+  SetLike.ext'_iff
+
+end AffineSubspace
+
+namespace Submodule
+
+variable {k V : Type*} [Ring k] [AddCommGroup V] [Module k V]
+
+/-- Reinterprets `p : Submodule k V` as an `AffineSubspace k V`. -/
+@[coe] def toAffineSubspace (p : Submodule k V) : AffineSubspace k V where
+  carrier := p
+  smul_vsub_vadd_mem _ _ _ _ h₁ h₂ h₃ := p.add_mem (p.smul_mem _ (p.sub_mem h₁ h₂)) h₃
+
+instance : Coe (Submodule k V) (AffineSubspace k V) := ⟨toAffineSubspace⟩
+
+@[simp]
+theorem mem_toAffineSubspace {p : Submodule k V} {x : V} :
+    x ∈ (p : AffineSubspace k V) ↔ x ∈ p := Iff.rfl
+
+end Submodule
+
+namespace AffineSubspace
+
+variable {k : Type*} {V : Type*} {P : Type*} [Ring k] [AddCommGroup V] [Module k V]
+  [AffineSpace V P]
+
+lemma vsub_self_of_zero_mem {s : AffineSubspace k V} (hs : 0 ∈ s) :
+    (s : Set V) -ᵥ s = s := by
+  ext x
+  constructor
+  · rintro ⟨a, ha, b, hb, rfl⟩
+    simpa using s.smul_vsub_vadd_mem 1 ha hb hs
+  · exact fun h => ⟨x, h, 0, hs, by simp⟩
+
+@[simp] lemma vsub_self_eq_iff_zero_mem {s : AffineSubspace k V} [Nonempty s] :
+    (s : Set V) -ᵥ s = s ↔ 0 ∈ s := by
+  refine ⟨fun h ↦ ?_, vsub_self_of_zero_mem⟩
+  obtain x : s := Classical.choice inferInstance
+  suffices (x : V) - x ∈ (s : Set _) by aesop
+  rw [← h, mem_vsub]
+  aesop
+
 /-- The direction of an affine subspace is the submodule spanned by
 the pairwise differences of points.  (Except in the case of an empty
 affine subspace, where the direction is the zero submodule, every
 vector in the direction is the difference of two points in the affine
-subspace.) -/
+subspace.)
+
+This can also be used to reinterpret an affine subspace that contains
+zero as a submodule, see `direction_eq_self_iff_zero_mem`.
+-/
 def direction (s : AffineSubspace k P) : Submodule k V :=
   vectorSpan k (s : Set P)
 
@@ -301,16 +347,17 @@ theorem mem_direction_iff_eq_vsub_left {s : AffineSubspace k P} {p : P} (hp : p
   rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_left hp]
   exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩
 
-/-- Two affine subspaces are equal if they have the same points. -/
-theorem coe_injective : Function.Injective ((↑) : AffineSubspace k P → Set P) :=
-  SetLike.coe_injective
-
-@[ext (iff := false)]
-theorem ext {p q : AffineSubspace k P} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q :=
-  SetLike.ext h
+/-- An affine subspace contains zero if and only if it equals its directions. -/
+@[simp] lemma direction_eq_self_iff_zero_mem {s : AffineSubspace k V} :
+    s.direction = s ↔ 0 ∈ s where
+  mp h := by rw [← h]; simp
+  mpr h := by
+    ext x
+    rw [Submodule.mem_toAffineSubspace, ← SetLike.mem_coe]
+    simp [s.coe_direction_eq_vsub_set ⟨0, h⟩, vsub_self_of_zero_mem h]
 
-protected theorem ext_iff (s₁ s₂ : AffineSubspace k P) : s₁ = s₂ ↔ (s₁ : Set P) = s₂ :=
-  SetLike.ext'_iff
+instance : CanLift (AffineSubspace k V) (Submodule k V) (·) (0 ∈ ·) :=
+  ⟨fun _ hs => ⟨_, direction_eq_self_iff_zero_mem.mpr hs⟩⟩
 
 /-- Two affine subspaces with the same direction and nonempty intersection are equal. -/
 theorem ext_of_direction_eq {s₁ s₂ : AffineSubspace k P} (hd : s₁.direction = s₂.direction)
@@ -401,11 +448,6 @@ namespace Submodule
 
 variable {k V : Type*} [Ring k] [AddCommGroup V] [Module k V]
 
-@[simp]
-theorem mem_toAffineSubspace {p : Submodule k V} {x : V} :
-    x ∈ p.toAffineSubspace ↔ x ∈ p :=
-  Iff.rfl
-
 @[simp]
 theorem toAffineSubspace_direction (s : Submodule k V) : s.toAffineSubspace.direction = s := by
   ext x; simp [← s.toAffineSubspace.vadd_mem_iff_mem_direction _ s.zero_mem]