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.

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

theorem Projectivization.orthogonal_comm {F : Type u_1} [Field F] {m : Type u_2} [Fintype m] {v 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 w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) : mk F v hv = 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.

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

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

theorem Projectivization.cross_mk_of_cross_ne_zero {F : Type u_1} [Field F] [DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) (h : (crossProduct v) w ≠ 0) : (mk F v hv).cross (mk F w hw) = 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 w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) (h : mk F v hv ≠ mk F w hw) : (mk F v hv).cross (mk F w hw) = mk F ((crossProduct v) w) ⋯

theorem Projectivization.cross_comm {F : Type u_1} [Field F] [DecidableEq F] (v 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 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 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 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 w : Projectivization F (Fin 3 → F)} (h : v ≠ w) : w.orthogonal (v.cross w)