Number of planar points in 3d linear space over finite field

Stream: new members

[Xipan Xiao]

I am trying to prove the following statement: Let k = Z/pZ a finite field, any plane in k^3 contains exactly p^2 points. The mathematic proof is like: for any plane defined by ax + by + cz = d, without loss of generality suppose c is non-zero, then given any pair (x, y), there is a unique z = (d - ax - by) / c. So the number of points on this plane is just the number of pairs (x, y) in k^2, hence p^2.
I proved a lemma unique_zmod_solution, which says given the equation ax + by + cz = d with c non-zero, there is one and only z solving it:

open FiniteField

variable {p : ℕ} [Fact p.Prime]

theorem unique_zmod_solution (a b c d x y : ZMod p) (hc : c ≠ 0) : ∃! z : ZMod p, a * x + b * y + c * z = d := by
  use c⁻¹ * (d - (a * x + b * y))
  constructor
  · field_simp [hc]
  · {
    intros z hz
    calc
      z = c⁻¹ * (d - (a * x + b * y)) := by
        field_simp [hz]
        rw [← sub_eq_zero]
        ring
        rw [mul_comm, add_assoc, add_comm]
        calc
          a * x + b * y + (c * z - d) = a * x + b * y + c * z - d := by ring
          _ = d - d := by rw [hz]
          _ = 0 := by ring
  }

Then I'm trying to construct a set representing the plane and count the points in the set, and tried many code pieces suggested copilit, but none worked. My most recent attempt was to build a bijection between two sets but I kept getting type errors.

theorem plane_has_p_squared_points:
  ∀ (a b c d : ZMod p), a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 →
  (Set.toFinset {(x, y, z) : (ZMod p) × (ZMod p) × (ZMod p) | a * x + b * y + c * z = d}).card = p^2 := by
    intros a b c d h_nonzero
    have h1 : ∀ x y : ZMod p, ∃! z : ZMod p, a * x + b * y + c * z = d := by
      intros x y
      exact unique_zmod_solution a b c d x y h_nonzero.2.2
    -- Now we need to show that the set of solutions is finite and has cardinality p^2
    let S := { (x, y, z) : (ZMod p) × (ZMod p) × (ZMod p) | a * x + b * y + c * z = d }
    let f : S → (ZMod p) × (ZMod p) := fun ⟨(x, y, z), h⟩ => (x, y)
    let g : (ZMod p) × (ZMod p) → S := fun (x, y) =>
      ⟨(x, y, Classical.choose (h1 x y)), Classical.choose_spec (h1 x y)⟩
    have hf : Function.LeftInverse g f := by
      intro ⟨(x, y, z), h⟩
      simp only
      have : z = Classical.choose (h1 x y) := by
      apply Classical.choose_spec (h1 x y)
      exact h
      rw [this]
    have hg : Function.RightInverse g f := by
      intro (x, y)
      simp only
    exact Fintype.card_congr (Equiv.ofBijective ⟨f, g, hf, hg⟩)

Is this the right direction at all? I'm a beginner and am struggling with "how to express math with lean code". Any help/hint/suggestions are appreciated. Thansk.

[Kevin Buzzard]

import Mathlib

open FiniteField

variable {p : ℕ} [Fact p.Prime]

theorem unique_zmod_solution (a b c d x y : ZMod p) (hc : c ≠ 0) :
    ∃! z : ZMod p, a * x + b * y + c * z = d := by
  use c⁻¹ * (d - (a * x + b * y))
  constructor
  · field_simp
  · intros z hz
    field_simp
    polyrith

is a much simpler way of doing the first part.

[Kevin Buzzard]

It's difficult to say too much about the second part because it doesn't compile so it's not really clear what your question is. I would recommend reading a book like #mil rather than trying to learn Lean with a language model, language models are not good at Lean right now.

[Kevin Buzzard]

Maybe you want to start like this:

def bijection (a b c d : ZMod p) (hc : c ≠ 0) :
    {(x, y, z) : (ZMod p) × (ZMod p) × (ZMod p) | a * x + b * y + c * z = d} ≃
    (ZMod p) × (ZMod p) where
toFun xyzpf := (xyzpf.1.1, xyzpf.1.2.1) -- xyzpf is x,y,z plus proof of the equality
invFun xy := ⟨(xy.1, xy.2, c⁻¹ * (d - (a * xy.1 + b * xy.2))), by field_simp⟩
left_inv := sorry
right_inv := sorry