Update Completion.lean

ElementarGeometrie/Projective/Completion.lean

@@ -46,12 +46,133 @@ def completionLines : Set (Set (E ⊕ ℙ K V)) :=
         L = Sum.inl '' (s : Set E) ∪ {Sum.inr (Projectivization.mk'' s.direction h)})
     ∨ (∃ g ∈ projectiveLines K V, L = Sum.inr '' g)}
 
+section Helpers
+
+variable {K V E : Type u} [Field K] [AddCommGroup V] [Module K V] [AddTorsor V E]
+
+open AffineSubspace
+
+/-- The point at infinity depends only on the direction, not on the proof. -/
+theorem mk''_congr {H H' : Submodule K V} (h : Module.finrank K H = 1)
+    (h' : Module.finrank K H' = 1) (e : H = H') :
+    Projectivization.mk'' H h = Projectivization.mk'' H' h' := by subst e; rfl
+
+theorem inl_mem_affLine {s : AffineSubspace K E} {h : Module.finrank K s.direction = 1} {p : E} :
+    (Sum.inl p : E ⊕ ℙ K V) ∈
+      Sum.inl '' (s : Set E) ∪ {Sum.inr (Projectivization.mk'' s.direction h)} ↔ p ∈ s := by
+  simp
+
+theorem inr_mem_affLine {s : AffineSubspace K E} {h : Module.finrank K s.direction = 1}
+    {ℓ : ℙ K V} :
+    (Sum.inr ℓ : E ⊕ ℙ K V) ∈
+      Sum.inl '' (s : Set E) ∪ {Sum.inr (Projectivization.mk'' s.direction h)} ↔
+      ℓ = Projectivization.mk'' s.direction h := by
+  simp
+
+omit [AddTorsor V E] in
+theorem inl_mem_inrImage {g : Set (ℙ K V)} {p : E} :
+    (Sum.inl p : E ⊕ ℙ K V) ∈ Sum.inr '' g ↔ False := by simp
+
+omit [AddTorsor V E] in
+theorem inr_mem_inrImage {g : Set (ℙ K V)} {ℓ : ℙ K V} :
+    (Sum.inr ℓ : E ⊕ ℙ K V) ∈ Sum.inr '' g ↔ ℓ ∈ g := by simp
+
+end Helpers
+
+open AffineSubspace in
 /-- The **projective completion** of the affine space `E` as an incidence
 geometry on `E ⊕ ℙ K V`. -/
 noncomputable def projectiveCompletion : IncidenceGeometry (E ⊕ ℙ K V) where
   lines := completionLines K V E
-  two_points := by sorry
-  unique_line := by sorry
+  two_points := by
+    rintro L (⟨s, h, rfl⟩ | ⟨g, hg, rfl⟩)
+    · -- An affine line together with its point at infinity has ≥ 2 points.
+      have hsne : (s : Set E).Nonempty := by
+        rw [AffineSubspace.nonempty_iff_ne_bot]
+        intro hbot
+        rw [hbot, AffineSubspace.direction_bot, finrank_bot] at h
+        exact absurd h (by norm_num)
+      obtain ⟨p, hp⟩ := hsne
+      refine ⟨Sum.inl p, Sum.inr (Projectivization.mk'' s.direction h),
+        Sum.inl_ne_inr, Set.mem_union_left _ ⟨p, hp, rfl⟩, Set.mem_union_right _ rfl⟩
+    · -- A projective line has ≥ 2 points.
+      obtain ⟨a, b, hab, ha, hb⟩ := (projectivization K V).two_points g hg
+      exact ⟨Sum.inr a, Sum.inr b, fun he => hab (Sum.inr_injective he),
+        ⟨a, ha, rfl⟩, ⟨b, hb, rfl⟩⟩
+  unique_line := by
+    rintro (p | ℓ₁) (q | ℓ₂) hPQ
+    · -- Two affine points: the affine line through them, plus its infinity point.
+      have hpq : p ≠ q := fun he => hPQ (by rw [he])
+      have hqp0 : q -ᵥ p ≠ (0 : V) := vsub_ne_zero.2 (Ne.symm hpq)
+      have hdir1 : Module.finrank K (mk' p (K ∙ (q -ᵥ p))).direction = 1 := by
+        rw [direction_mk']; exact finrank_span_singleton hqp0
+      refine ⟨Sum.inl '' (↑(mk' p (K ∙ (q -ᵥ p))) : Set E) ∪
+          {Sum.inr (Projectivization.mk'' (mk' p (K ∙ (q -ᵥ p))).direction hdir1)},
+        ⟨Or.inl ⟨_, hdir1, rfl⟩, Set.mem_union_left _ ⟨p, self_mem_mk' _ _, rfl⟩,
+          Set.mem_union_left _ ⟨q, mem_mk'.2 (Submodule.mem_span_singleton_self _), rfl⟩⟩,
+        ?_⟩
+      rintro L ⟨hL, hpL, hqL⟩
+      rcases hL with ⟨s, h, rfl⟩ | ⟨g, hg, rfl⟩
+      · rw [inl_mem_affLine] at hpL hqL
+        haveI : FiniteDimensional K s.direction := Module.finite_of_finrank_eq_succ h
+        have hle : K ∙ (q -ᵥ p) ≤ s.direction :=
+          (Submodule.span_singleton_le_iff_mem _ _).2 (vsub_mem_direction hqL hpL)
+        have hdir : s.direction = K ∙ (q -ᵥ p) :=
+          (Submodule.eq_of_le_of_finrank_eq hle (by rw [finrank_span_singleton hqp0, h])).symm
+        have hs : s = mk' p (K ∙ (q -ᵥ p)) :=
+          (mk'_eq hpL).symm.trans (congrArg (mk' p) hdir)
+        subst hs; rfl
+      · rw [inl_mem_inrImage] at hpL; exact hpL.elim
+    · -- An affine point and a point at infinity: the affine line in that direction.
+      have hdir1 : Module.finrank K (mk' p ℓ₂.submodule).direction = 1 := by
+        rw [direction_mk']; exact ℓ₂.finrank_submodule
+      refine ⟨Sum.inl '' (↑(mk' p ℓ₂.submodule) : Set E) ∪
+          {Sum.inr (Projectivization.mk'' (mk' p ℓ₂.submodule).direction hdir1)},
+        ⟨Or.inl ⟨_, hdir1, rfl⟩, Set.mem_union_left _ ⟨p, self_mem_mk' _ _, rfl⟩, ?_⟩, ?_⟩
+      · rw [inr_mem_affLine]; symm
+        rw [mk''_congr hdir1 ℓ₂.finrank_submodule (direction_mk' _ _)]
+        exact Projectivization.mk''_submodule ℓ₂
+      · rintro L ⟨hL, hpL, hℓL⟩
+        rcases hL with ⟨s, h, rfl⟩ | ⟨g, hg, rfl⟩
+        · rw [inl_mem_affLine] at hpL
+          rw [inr_mem_affLine] at hℓL
+          have hdir : s.direction = ℓ₂.submodule := by
+            have hsub := congrArg Projectivization.submodule hℓL
+            rw [Projectivization.submodule_mk''] at hsub; exact hsub.symm
+          have hs : s = mk' p ℓ₂.submodule :=
+            (mk'_eq hpL).symm.trans (congrArg (mk' p) hdir)
+          subst hs; rfl
+        · rw [inl_mem_inrImage] at hpL; exact hpL.elim
+    · -- A point at infinity and an affine point: symmetric to the previous case.
+      have hdir1 : Module.finrank K (mk' q ℓ₁.submodule).direction = 1 := by
+        rw [direction_mk']; exact ℓ₁.finrank_submodule
+      refine ⟨Sum.inl '' (↑(mk' q ℓ₁.submodule) : Set E) ∪
+          {Sum.inr (Projectivization.mk'' (mk' q ℓ₁.submodule).direction hdir1)},
+        ⟨Or.inl ⟨_, hdir1, rfl⟩, ?_, Set.mem_union_left _ ⟨q, self_mem_mk' _ _, rfl⟩⟩, ?_⟩
+      · rw [inr_mem_affLine]; symm
+        rw [mk''_congr hdir1 ℓ₁.finrank_submodule (direction_mk' _ _)]
+        exact Projectivization.mk''_submodule ℓ₁
+      · rintro L ⟨hL, hℓL, hqL⟩
+        rcases hL with ⟨s, h, rfl⟩ | ⟨g, hg, rfl⟩
+        · rw [inr_mem_affLine] at hℓL
+          rw [inl_mem_affLine] at hqL
+          have hdir : s.direction = ℓ₁.submodule := by
+            have hsub := congrArg Projectivization.submodule hℓL
+            rw [Projectivization.submodule_mk''] at hsub; exact hsub.symm
+          have hs : s = mk' q ℓ₁.submodule :=
+            (mk'_eq hqL).symm.trans (congrArg (mk' q) hdir)
+          subst hs; rfl
+        · rw [inl_mem_inrImage] at hqL; exact hqL.elim
+    · -- Two points at infinity: the projective line through them.
+      have hne : ℓ₁ ≠ ℓ₂ := fun he => hPQ (by rw [he])
+      obtain ⟨g₀, ⟨hg₀lines, hg₀1, hg₀2⟩, hg₀uniq⟩ := (projectivization K V).unique_line ℓ₁ ℓ₂ hne
+      refine ⟨Sum.inr '' g₀, ⟨Or.inr ⟨g₀, hg₀lines, rfl⟩, ⟨ℓ₁, hg₀1, rfl⟩, ⟨ℓ₂, hg₀2, rfl⟩⟩, ?_⟩
+      rintro L ⟨hL, h1L, h2L⟩
+      rcases hL with ⟨s, h, rfl⟩ | ⟨g, hg, rfl⟩
+      · rw [inr_mem_affLine] at h1L h2L
+        exact absurd (h1L.trans h2L.symm) hne
+      · rw [inr_mem_inrImage] at h1L h2L
+        rw [hg₀uniq g ⟨hg, h1L, h2L⟩]
 
 /-- The **points at infinity** of the projective completion: the points coming
 from `ℙ K V`. -/