CoordinateChange.lean

def coordinateLinearMap (α β γ δ : K) : (K × K) →ₗ[K] (K × K) where
  toFun := transform α β γ δ
  map_add' a b := by
    apply Prod.ext
    · change α * (a.1 + b.1) + β * (a.2 + b.2) =
        (α * a.1 + β * a.2) + (α * b.1 + β * b.2)
      ring
    · change γ * (a.1 + b.1) + δ * (a.2 + b.2) =
        (γ * a.1 + δ * a.2) + (γ * b.1 + δ * b.2)
      ring
  map_smul' t a := by
    apply Prod.ext
    · change α * (t * a.1) + β * (t * a.2) = t * (α * a.1 + β * a.2)
      ring
    · change γ * (t * a.1) + δ * (t * a.2) = t * (γ * a.1 + δ * a.2)
      ring

theorem coordinateLinearMap_injective (α β γ δ : K) (hdet : α * δ - β * γ ≠ 0) :
    Function.Injective (coordinateLinearMap α β γ δ)

def coordinateLinearEquiv (α β γ δ : K)
    (hdet : α * δ - β * γ ≠ 0) : (K × K) ≃ₗ[K] (K × K)

def projectiveLinearEquiv (f : (K × K) ≃ₗ[K] (K × K)) :
    Projectivization K (K × K) ≃ Projectivization K (K × K) where
  toFun := Projectivization.map f.toLinearMap f.injective
  invFun := Projectivization.map f.symm.toLinearMap f.symm.injective
  left_inv p := by
    induction p using Projectivization.ind with
    | h v hv =>
      simp only [Projectivization.map_mk]
      change Projectivization.mk K (f.symm (f v)) _ = Projectivization.mk K v hv
      simp only [LinearEquiv.symm_apply_apply]
  right_inv p := by
    induction p using Projectivization.ind with
    | h v hv =>
      simp only [Projectivization.map_mk]
      change Projectivization.mk K (f (f.symm v)) _ = Projectivization.mk K v hv
      simp only [LinearEquiv.apply_symm_apply]

theorem projectiveLinearEquiv_mk (f : (K × K) ≃ₗ[K] (K × K))
    (v : K × K) (hv : v ≠ 0) :
    projectiveLinearEquiv f (Projectivization.mk K v hv) =
      Projectivization.mk K (f v) (map_zero f ▸ f.injective.ne hv)

def projectiveCoordinateChange (α β γ δ : K)
    (hdet : α * δ - β * γ ≠ 0) :
    Projectivization K (K × K) ≃ Projectivization K (K × K)

theorem crossRatio_projectiveCoordinateChange (α β γ δ : K)
    (hdet : α * δ - β * γ ≠ 0) (a b c d : Projectivization K (K × K)) :
    crossRatio (projectiveCoordinateChange α β γ δ hdet a)
      (projectiveCoordinateChange α β γ δ hdet b)
      (projectiveCoordinateChange α β γ δ hdet c)
      (projectiveCoordinateChange α β γ δ hdet d) = crossRatio a b c d