parallel and oriented angle

Stream: Is there code for X?

[yulia wang]

Hi all! I’m trying to formalize the classical “parallel ⇔ angle criteria” using oriented angles.
To avoid side-of-transversal conditions, I represent the angle between a (undirected) line ℓ and a transversal t by “2 × oriented angle” of the chosen rays at their intersection. Doubling kills the choice of direction, so it really gives an angle mod π between lines.
With this, I can state one lemma unifying the three school-geometry criteria:
For lines ℓ₁, ℓ₂ and a transversal t meeting them, the following are equivalent (all equalities in Real.Angle with the 2× convention):

1. ℓ₁ ∥ ℓ₂
2. corresponding angles are equal
3. alternate interior angles are equal
4. same-side interior angles are supplementary (sum to π).
   Does this look like a reasonable definition/statement in mathlib? Is “doubling” the right idiom here, or is there a better established way to work modulo π? Any naming/assumption advice is appreciated!

import Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

open Module Complex
open Affine AffineSubspace EuclideanGeometry Orientation Real
namespace EuclideanGeometry

variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
  [NormedAddTorsor V P] [hd2 : Fact (finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)]


theorem two_zsmul_oangle_of_parallel'_right {p₁ p₂ p₃ p₄ p: P}
    (h₁₂₃₄ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₃, p₄]) (h_collinear : Collinear ℝ {p, p₂, p₄}) :
    (2 : ℤ) • ∡ p₁ p₂ p = (2 : ℤ) • ∡ p₃ p₄ p := by
    sorry

theorem two_zsmul_oangle_of_parallel'_left {p₁ p₂ p₃ p₄ p: P}
    (h₁₂₃₄ : line[ℝ, p₁, p₂] ∥ line[ℝ, p₃, p₄]) (h_collinear : Collinear ℝ {p, p₂, p₄}) :
    (2 : ℤ) • ∡ p p₂ p₁ = (2 : ℤ) • ∡ p p₄ p₃ := by
    sorry

theorem parallel_of_two_zsmul_oangle_left {p₁ p₂ p₃ p₄ p: P}
    (h_oangle_eq : (2 : ℤ) • ∡ p p₂ p₁ = (2 : ℤ) • ∡ p p₄ p₃) (h_collinear : Collinear ℝ {p, p₂, p₄})
    (h_p1_neq_p2 : p₁ ≠ p₂) (h_p3_neq_p4 : p₃ ≠ p₄) :
    line[ℝ, p₁, p₂] ∥ line[ℝ, p₃, p₄] := by
    sorry

theorem parallel_of_two_zsmul_oangle_right {p₁ p₂ p₃ p₄ p: P}
    (h_oangle_eq : (2 : ℤ) • ∡ p₁ p₂ p = (2 : ℤ) • ∡ p₃ p₄ p) (h_collinear : Collinear ℝ {p, p₂, p₄})
    (h_p1_neq_p2 : p₁ ≠ p₂) (h_p3_neq_p4 : p₃ ≠ p₄) :
    line[ℝ, p₁, p₂] ∥ line[ℝ, p₃, p₄] := by
    sorry

end EuclideanGeometry

[Jovan Gerbscheid]

I think you also need the side conditions that p isn't p2 or p4. And you can also add the iff forms of the lemmas. It might be nice to have API for angles mod π, but I think the consensus is currently that the two_zsmul form is more convenient than adding new angle mod π API.

I also wonder if it makes sense to have a definition of angle between two lines (as 1 dimensional subspaces) (which could default to 0 if the dimensions are wrong) which would include the factor of 2.

[yulia wang]

Thank you very much ! I’ve:

• added the side conditions p ≠ p2 and p ≠ p4;
• upgraded the statements to iff;
• kept the two_zsmul formulation
  Updated code is below.

import Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

open Module Complex
open Affine AffineSubspace EuclideanGeometry Orientation Real
namespace EuclideanGeometry

variable {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P]
  [NormedAddTorsor V P] [hd2 : Fact (finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)]


theorem two_zsmul_oangle_eq_iff_parallel_right {p₁ p₂ p₃ p₄ p: P} (h_collinear : Collinear ℝ {p, p₂, p₄})
    (h_p_neq_p2 : p ≠ p₂) (h_p_neq_p4 : p ≠ p₄) (h_p1_neq_p2 : p₁ ≠ p₂) (h_p3_neq_p4 : p₃ ≠ p₄):
    line[ℝ, p₁, p₂] ∥ line[ℝ, p₃, p₄] ↔ (2 : ℤ) • ∡ p₁ p₂ p = (2 : ℤ) • ∡ p₃ p₄ p := by
    sorry

theorem two_zsmul_oangle_of_parallel'_left {p₁ p₂ p₃ p₄ p: P} (h_collinear : Collinear ℝ {p, p₂, p₄})
    (h_p_neq_p2 : p ≠ p₂) (h_p_neq_p4 : p ≠ p₄) (h_p1_neq_p2 : p₁ ≠ p₂) (h_p3_neq_p4 : p₃ ≠ p₄) :
    line[ℝ, p₁, p₂] ∥ line[ℝ, p₃, p₄] ↔ (2 : ℤ) • ∡ p p₂ p₁ = (2 : ℤ) • ∡ p p₄ p₃ := by
    sorry

end EuclideanGeometry

[yulia wang]

two_zsmul_oangle_of_parallel'_left has already been modified to two_zsmul_oangle_eq_iff_parallel_left