Dot Product and Cross Product on Projective Spaces

This file defines the dot product and cross product on projective spaces.

Definitions

• Projectivization.orthogonal v w is defined as vanishing of the dot product.
• Projectivization.cross v w for v w : ℙ F (Fin 3 → F) is defined as the cross product of v and w provided that v ≠ w. If v = w, then the cross product would be zero, so we instead define cross v v = v.

def Projectivization.orthogonal {F : Type u_1} [Field F] {m : Type u_2} [Fintype m] : Projectivization F (m → F) → Projectivization F (m → F) → Prop

Orthogonality on the projective plane.

Equations

• Projectivization.orthogonal = Quotient.lift₂ (fun (v w : { v : m → F // v ≠ 0 }) => Matrix.dotProduct ↑v ↑w = 0) ⋯

theorem Projectivization.orthogonal_mk {F : Type u_1} [Field F] {m : Type u_2} [Fintype m] {v : m → F} {w : m → F} (hv : v ≠ 0) (hw : w ≠ 0) : (Projectivization.mk F v hv).orthogonal (Projectivization.mk F w hw) ↔ Matrix.dotProduct v w = 0

theorem Projectivization.orthogonal_comm {F : Type u_1} [Field F] {m : Type u_2} [Fintype m] {v : Projectivization F (m → F)} {w : Projectivization F (m → F)} : v.orthogonal w ↔ w.orthogonal v

theorem Projectivization.exists_not_self_orthogonal {F : Type u_1} [Field F] {m : Type u_2} [Fintype m] (v : Projectivization F (m → F)) : ∃ (w : Projectivization F (m → F)), ¬v.orthogonal w

theorem Projectivization.exists_not_orthogonal_self {F : Type u_1} [Field F] {m : Type u_2} [Fintype m] (v : Projectivization F (m → F)) : ∃ (w : Projectivization F (m → F)), ¬w.orthogonal v

theorem Projectivization.mk_eq_mk_iff_crossProduct_eq_zero {F : Type u_1} [Field F] {v : Fin 3 → F} {w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) : Projectivization.mk F v hv = Projectivization.mk F w hw ↔ (crossProduct v) w = 0

def Projectivization.cross {F : Type u_1} [Field F] [DecidableEq F] : Projectivization F (Fin 3 → F) → Projectivization F (Fin 3 → F) → Projectivization F (Fin 3 → F)

Cross product on the projective plane.

Equations

• Projectivization.cross = Quotient.map₂' (fun (v w : { v : Fin 3 → F // v ≠ 0 }) => if h : (crossProduct ↑v) ↑w = 0 then v else ⟨(crossProduct ↑v) ↑w, h⟩) ⋯

theorem Projectivization.cross_mk {F : Type u_1} [Field F] [DecidableEq F] {v : Fin 3 → F} {w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) : (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = if h : (crossProduct v) w = 0 then Projectivization.mk F v hv else Projectivization.mk F ((crossProduct v) w) h

theorem Projectivization.cross_mk_of_cross_eq_zero {F : Type u_1} [Field F] [DecidableEq F] {v : Fin 3 → F} {w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) (h : (crossProduct v) w = 0) : (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = Projectivization.mk F v hv

theorem Projectivization.cross_mk_of_cross_ne_zero {F : Type u_1} [Field F] [DecidableEq F] {v : Fin 3 → F} {w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) (h : (crossProduct v) w ≠ 0) : (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = Projectivization.mk F ((crossProduct v) w) h

theorem Projectivization.cross_self {F : Type u_1} [Field F] [DecidableEq F] (v : Projectivization F (Fin 3 → F)) : v.cross v = v

theorem Projectivization.cross_mk_of_ne {F : Type u_1} [Field F] [DecidableEq F] {v : Fin 3 → F} {w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) (h : Projectivization.mk F v hv ≠ Projectivization.mk F w hw) : (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = Projectivization.mk F ((crossProduct v) w) ⋯

theorem Projectivization.cross_comm {F : Type u_1} [Field F] [DecidableEq F] (v : Projectivization F (Fin 3 → F)) (w : Projectivization F (Fin 3 → F)) : v.cross w = w.cross v

theorem Projectivization.cross_orthogonal_left {F : Type u_1} [Field F] [DecidableEq F] {v : Projectivization F (Fin 3 → F)} {w : Projectivization F (Fin 3 → F)} (h : v ≠ w) : (v.cross w).orthogonal v

theorem Projectivization.cross_orthogonal_right {F : Type u_1} [Field F] [DecidableEq F] {v : Projectivization F (Fin 3 → F)} {w : Projectivization F (Fin 3 → F)} (h : v ≠ w) : (v.cross w).orthogonal w

theorem Projectivization.orthogonal_cross_left {F : Type u_1} [Field F] [DecidableEq F] {v : Projectivization F (Fin 3 → F)} {w : Projectivization F (Fin 3 → F)} (h : v ≠ w) : v.orthogonal (v.cross w)

theorem Projectivization.orthogonal_cross_right {F : Type u_1} [Field F] [DecidableEq F] {v : Projectivization F (Fin 3 → F)} {w : Projectivization F (Fin 3 → F)} (h : v ≠ w) : w.orthogonal (v.cross w)