diff --git a/ElementarGeometrie/Projective/Duality.lean b/ElementarGeometrie/Projective/Duality.lean
index ba857dd..d42b00a 100644
--- a/ElementarGeometrie/Projective/Duality.lean
+++ b/ElementarGeometrie/Projective/Duality.lean
@@ -3,7 +3,7 @@ Copyright (c) 2026 Stefan Kebekus. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stefan Kebekus
 -/
-import Mathlib.LinearAlgebra.Dual.Defs
+import Mathlib.LinearAlgebra.Dual.Lemmas
 import ElementarGeometrie.Projective.Space
 
 /-!
@@ -76,6 +76,106 @@ def toIncidenceStructure (G : IncidenceGeometry X) :
 
 open scoped LinearAlgebra.Projectivization
 
+section Duality
+
+variable {K : Type u} [Field K]
+
+/-- A projective line, as a set of points, determines its underlying subspace:
+the subspaces are recovered as the directions of the points lying on the line. -/
+theorem projLine_inj {U : Type u} [AddCommGroup U] [Module K U] {W W' : Submodule K U}
+    (hWW' : {p : ℙ K U | p.submodule ≤ W} = {p : ℙ K U | p.submodule ≤ W'}) : W = W' := by
+  have key : ∀ {A B : Submodule K U},
+      {p : ℙ K U | p.submodule ≤ A} ⊆ {p | p.submodule ≤ B} → A ≤ B := by
+    intro A B hsub w hw
+    by_cases hw0 : w = 0
+    · rw [hw0]; exact B.zero_mem
+    · have hmem : Projectivization.mk K w hw0 ∈ {p : ℙ K U | p.submodule ≤ B} :=
+        hsub (by
+          simp only [Set.mem_setOf_eq, Projectivization.submodule_mk]
+          exact (Submodule.span_singleton_le_iff_mem _ _).2 hw)
+      rw [Set.mem_setOf_eq, Projectivization.submodule_mk,
+        Submodule.span_singleton_le_iff_mem] at hmem
+      exact hmem
+  exact le_antisymm (key hWW'.le) (key hWW'.ge)
+
+/-- The projective lines of `ℙ K U`, as sets of points, are in bijection with the
+two-dimensional subspaces of `U`. -/
+noncomputable def projLineEquiv (U : Type u) [AddCommGroup U] [Module K U] :
+    {g : Set (ℙ K U) // g ∈ projectiveLines K U} ≃
+      {W : Submodule K U // Module.finrank K W = 2} where
+  toFun g := ⟨Classical.choose g.2, (Classical.choose_spec g.2).1⟩
+  invFun W := ⟨{p | p.submodule ≤ W.1}, ⟨W.1, W.2, rfl⟩⟩
+  left_inv g := Subtype.ext (Classical.choose_spec g.2).2.symm
+  right_inv W := Subtype.ext (projLine_inj (Classical.choose_spec
+    (⟨W.1, W.2, rfl⟩ : {p : ℙ K U | p.submodule ≤ W.1} ∈ projectiveLines K U)).2).symm
+
+@[simp]
+theorem projLineEquiv_apply_coe {U : Type u} [AddCommGroup U] [Module K U]
+    (g : {g : Set (ℙ K U) // g ∈ projectiveLines K U}) :
+    ((projLineEquiv U) g).1 = Classical.choose g.2 := rfl
+
+@[simp]
+theorem projLineEquiv_symm_coe {U : Type u} [AddCommGroup U] [Module K U]
+    (W : {W : Submodule K U // Module.finrank K W = 2}) :
+    ((projLineEquiv U).symm W).1 = {p : ℙ K U | p.submodule ≤ W.1} := rfl
+
+/-- The underlying subspace of the point `equivSubmodule p` is `p.submodule`. -/
+theorem equivSubmodule_coe {U : Type u} [AddCommGroup U] [Module K U] (p : ℙ K U) :
+    ((Projectivization.equivSubmodule K U) p).1 = p.submodule := rfl
+
+/-- The point built from a one-dimensional subspace `S` has `S` as its subspace. -/
+theorem equivSubmodule_symm_submodule {U : Type u} [AddCommGroup U] [Module K U]
+    (S : {H : Submodule K U // Module.finrank K H = 1}) :
+    ((Projectivization.equivSubmodule K U).symm S).submodule = S.1 :=
+  Projectivization.submodule_mk'' S.1 S.2
+
+variable (V : Type u) [AddCommGroup V] [Module K V] [FiniteDimensional K V]
+
+/-- The dual-coannihilator bijection between the `m`-dimensional subspaces of `V*`
+and the `n`-dimensional subspaces of `V`, whenever `m + n = dim V`. -/
+noncomputable def coannEquiv (m n : ℕ) (hmn : m + n = Module.finrank K V) :
+    {Φ : Submodule K (Module.Dual K V) // Module.finrank K Φ = m} ≃
+      {S : Submodule K V // Module.finrank K S = n} where
+  toFun Φ := ⟨Φ.1.dualCoannihilator, by
+    have h2 := Subspace.finrank_add_finrank_dualCoannihilator_eq Φ.1
+    rw [Φ.2, ← hmn] at h2
+    exact Nat.add_left_cancel h2⟩
+  invFun S := ⟨S.1.dualAnnihilator, by
+    have h2 := Subspace.finrank_add_finrank_dualAnnihilator_eq S.1
+    rw [S.2, ← hmn, add_comm m n] at h2
+    exact Nat.add_left_cancel h2⟩
+  left_inv Φ := Subtype.ext Subspace.dualCoannihilator_dualAnnihilator_eq
+  right_inv S := Subtype.ext Subspace.dualAnnihilator_dualCoannihilator_eq
+
+@[simp]
+theorem coannEquiv_apply_coe (m n : ℕ) (hmn : m + n = Module.finrank K V)
+    (Φ : {Φ : Submodule K (Module.Dual K V) // Module.finrank K Φ = m}) :
+    ((coannEquiv V m n hmn) Φ).1 = Φ.1.dualCoannihilator := rfl
+
+variable {V}
+
+/-- The dual-coannihilator is antitone and bijective on subspaces of `V*`. -/
+theorem coann_le_iff {A B : Submodule K (Module.Dual K V)} :
+    B.dualCoannihilator ≤ A.dualCoannihilator ↔ A ≤ B := by
+  rw [← Subspace.dualAnnihilator_le_dualAnnihilator_iff,
+    Subspace.dualCoannihilator_dualAnnihilator_eq, Subspace.dualCoannihilator_dualAnnihilator_eq]
+
+variable (V) in
+/-- The point map of the duality: a point `⟨λ⟩` of `ℙ(V*)` maps to the projective
+line of `ℙ(V)` consisting of the points whose direction annihilates `λ`. -/
+noncomputable def dualityPoint (h : Module.finrank K V = 3) :
+    ℙ K (Module.Dual K V) ≃ {g : Set (ℙ K V) // g ∈ projectiveLines K V} :=
+  (Projectivization.equivSubmodule K (Module.Dual K V)).trans <|
+    (coannEquiv V 1 2 (by omega)).trans (projLineEquiv V).symm
+
+variable (V) in
+/-- The line map of the duality: a projective line of `ℙ(V*)` maps to the point of
+`ℙ(V)` whose direction is the joint kernel. -/
+noncomputable def dualityLine (h : Module.finrank K V = 3) :
+    {g : Set (ℙ K (Module.Dual K V)) // g ∈ projectiveLines K (Module.Dual K V)} ≃ ℙ K V :=
+  (projLineEquiv (Module.Dual K V)).trans <|
+    (coannEquiv V 2 1 (by omega)).trans (Projectivization.equivSubmodule K V).symm
+
 /-- **Point-line duality.** For a three-dimensional vector space `V` over a field
 `K`, the incidence structure of the projective plane `ℙ(V*)` is isomorphic to the
 dual of the incidence structure of `ℙ(V)`. -/
@@ -83,6 +183,24 @@ theorem isomorphic_dual_projectivization (K V : Type u) [Field K] [AddCommGroup
     [Module K V] (h : Module.finrank K V = 3) :
     (toIncidenceStructure (projectivization K (Module.Dual K V))).Isomorphic
       (toIncidenceStructure (projectivization K V)).Dual := by
-  sorry
+  haveI : FiniteDimensional K V := Module.finite_of_finrank_eq_succ h
+  refine ⟨dualityPoint V h, dualityLine V h, fun x g => ?_⟩
+  -- The incidence condition reduces to the antitonicity of `dualCoannihilator`.
+  change x ∈ g.1 ↔ (dualityLine V h g) ∈ (dualityPoint V h x).1
+  have hg : g.1 = {p : ℙ K (Module.Dual K V) | p.submodule ≤ Classical.choose g.2} :=
+    (Classical.choose_spec g.2).2
+  have hφ : (dualityPoint V h x).1 =
+      {p : ℙ K V | p.submodule ≤ (x.submodule).dualCoannihilator} := by
+    simp only [dualityPoint, Equiv.trans_apply, projLineEquiv_symm_coe, coannEquiv_apply_coe,
+      equivSubmodule_coe]
+  have hψ : (dualityLine V h g).submodule = (Classical.choose g.2).dualCoannihilator := by
+    simp only [dualityLine, Equiv.trans_apply, equivSubmodule_symm_submodule, coannEquiv_apply_coe,
+      projLineEquiv_apply_coe]
+  rw [hg, hφ]
+  simp only [Set.mem_setOf_eq]
+  rw [hψ]
+  exact coann_le_iff.symm
+
+end Duality
 
 end IncidenceGeometry