From 6470e9cbcd87bbe3fa76c297480a7affb3d9946d Mon Sep 17 00:00:00 2001 From: Joseph Myers Date: Fri, 22 May 2026 12:34:53 +0000 Subject: [PATCH] refactor(LinearAlgebra/Orientation,LinearAlgebra/AffineSpace/FiniteDimensional): instances for arbitrary orientations Based on suggestions by @kim-em on Zulip https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/PRs.20towards.20IMO.20geometry.202024.20P4/near/596946072 add convenience scoped instances for choosing an arbitrary orientation of a module, and for the `finrank` of the span of the vertices of a simplex. Note: I don't understand why the latter scoped instance is only found automatically in one of the two places using it; in `Sphere/Power.lean` it's necessary to use `Affine.Simplex.fact_finrank_direction_affineSpan_eq` rather than relying on typeclass inference, but in `Angle/Sphere.lean` typeclass inference suffices. --- Archive/Imo/Imo2019Q2.lean | 13 ++----------- Mathlib/Geometry/Euclidean/Angle/Sphere.lean | 8 ++------ Mathlib/Geometry/Euclidean/Sphere/Power.lean | 9 +++------ .../AffineSpace/FiniteDimensional.lean | 10 ++++++++++ Mathlib/LinearAlgebra/Orientation.lean | 9 +++++++++ 5 files changed, 26 insertions(+), 23 deletions(-) diff --git a/Archive/Imo/Imo2019Q2.lean b/Archive/Imo/Imo2019Q2.lean index 7d447ae03db0c8..8c817f3c79f68e 100644 --- a/Archive/Imo/Imo2019Q2.lean +++ b/Archive/Imo/Imo2019Q2.lean @@ -93,11 +93,6 @@ structure Imo2019q2Cfg where -- A hypothesis implicit in the first named angle. C_ne_Q₁ : C ≠ Q₁ -/-- A default choice of orientation, for lemmas that need to pick one. -/ -@[implicit_reducible] -def someOrientation [hd2 : Fact (finrank ℝ V = 2)] : Module.Oriented ℝ V (Fin 2) := - ⟨Basis.orientation (finBasisOfFinrankEq _ _ hd2.out)⟩ - variable {V Pt} namespace Imo2019q2Cfg @@ -263,6 +258,8 @@ end Oriented /-! ### More obvious configuration properties -/ +open scoped Module.Oriented.Arbitrary + section variable [hd2 : Fact (finrank ℝ V = 2)] @@ -275,7 +272,6 @@ theorem A₁_ne_B : cfg.A₁ ≠ cfg.B := by rw [AffineSubspace.eq_iff_direction_eq_of_mem (left_mem_affineSpan_pair _ _ _) hwbtw.mem_affineSpan] exact cfg.PQ_parallel_AB.direction_eq - haveI := someOrientation V have haQ : (2 : ℤ) • ∡ cfg.C cfg.B cfg.Q = (2 : ℤ) • ∡ cfg.C cfg.B cfg.A := by rw [Collinear.two_zsmul_oangle_eq_right _ cfg.A_ne_B cfg.Q_ne_B] rw [Set.pair_comm, Set.insert_comm] @@ -389,7 +385,6 @@ end Oriented theorem not_collinear_QPA₂ : ¬Collinear ℝ ({cfg.Q, cfg.P, cfg.A₂} : Set Pt) := by - haveI := someOrientation V rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂, ← affineIndependent_iff_not_collinear_set] have h : Cospherical ({cfg.B, cfg.A, cfg.A₂} : Set Pt) := by @@ -464,7 +459,6 @@ end Oriented theorem cospherical_QPB₂A₂ : Cospherical ({cfg.Q, cfg.P, cfg.B₂, cfg.A₂} : Set Pt) := - haveI := someOrientation V cospherical_of_two_zsmul_oangle_eq_of_not_collinear cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂A₂ cfg.not_collinear_QPA₂ @@ -515,13 +509,11 @@ end Oriented theorem not_collinear_CA₂A₁ : ¬Collinear ℝ ({cfg.C, cfg.A₂, cfg.A₁} : Set Pt) := by - haveI := someOrientation V rw [collinear_iff_of_two_zsmul_oangle_eq cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA, Set.pair_comm, Set.insert_comm, Set.pair_comm] exact cfg.not_collinear_ABC theorem cospherical_A₁Q₁CA₂ : Cospherical ({cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂} : Set Pt) := by - haveI := someOrientation V rw [Set.insert_comm cfg.Q₁, Set.insert_comm cfg.A₁, Set.pair_comm, Set.insert_comm cfg.A₁, Set.pair_comm] exact cospherical_of_two_zsmul_oangle_eq_of_not_collinear @@ -555,7 +547,6 @@ end Oriented theorem Q₁_mem_ω : cfg.Q₁ ∈ cfg.ω := - haveI := someOrientation V Affine.Triangle.mem_circumsphere_of_two_zsmul_oangle_eq (by decide : (0 : Fin 3) ≠ 1) (by decide : (0 : Fin 3) ≠ 2) (by decide) cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂ diff --git a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean index 34ba17744df3da..6904707feb63cf 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Sphere.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Sphere.lean @@ -425,19 +425,15 @@ theorem mem_circumsphere_of_two_zsmul_oangle_eq {t : Triangle ℝ P} {p : P} {i end Oriented +open scoped Affine.Simplex Module.Oriented.Arbitrary in /-- The circumradius of a triangle may be expressed explicitly as half the length of a side divided by the sine of the angle at the third point (a version of the law of sines or sine rule). -/ theorem dist_div_sin_angle_div_two_eq_circumradius (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) / 2 = t.circumradius := by - set S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points) with hS + let S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points) let t' : Triangle ℝ S := t.restrict S le_rfl - have hf2 : Fact (finrank ℝ S.direction = 2) := ⟨by - rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan] - simp⟩ - have : Module.Oriented ℝ S.direction (Fin 2) := - ⟨Basis.orientation (finBasisOfFinrankEq _ _ hf2.out)⟩ convert t'.dist_div_sin_oangle_div_two_eq_circumradius h₁₂ h₁₃ h₂₃ using 3 · rw [← Real.Angle.sin_toReal, Real.abs_sin_eq_sin_abs_of_abs_le_pi (Real.Angle.abs_toReal_le_pi _), diff --git a/Mathlib/Geometry/Euclidean/Sphere/Power.lean b/Mathlib/Geometry/Euclidean/Sphere/Power.lean index 96899bc1fdbccd..a4c2800f637501 100644 --- a/Mathlib/Geometry/Euclidean/Sphere/Power.lean +++ b/Mathlib/Geometry/Euclidean/Sphere/Power.lean @@ -160,6 +160,7 @@ private lemma cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi_aux apply similar_of_side_angle_side h_notcol_p₁pp₄ h_notcol_p₃pp₂ h_angle_eq ?_ grind [dist_comm] +open scoped Affine.Simplex Module.Oriented.Arbitrary in /-- If `p` lies strictly between `p₁` and `p₂` on one line and strictly between `p₃` and `p₄` on another line, and if `dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p`, then the points `p₁`, `p₂`, `p₃`, and `p₄` are cospherical. -/ @@ -171,7 +172,7 @@ theorem cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi {p₁ p₂ p₃ p₄ have hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄ := angle_eq_pi_iff_sbtw.mp hp₃p₄ have hindep : AffineIndependent ℝ ![p₁, p, p₃] := affineIndependent_iff_not_collinear_set.mpr hn set t : Affine.Triangle ℝ P := ⟨_, hindep⟩ with ht - set S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points) with hS + let S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points) have hp₂ : p₂ ∈ S := by suffices hmem : p₂ ∈ affineSpan ℝ {p₁, p} by exact affineSpan_mono ℝ (by simp [ht]; grind) hmem simp [hp₁p₂_sbtw.wbtw.collinear.mem_affineSpan_of_mem_of_ne _ _ _ hp₁p₂_sbtw.left_ne] @@ -195,16 +196,12 @@ theorem cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi {p₁ p₂ p₃ p₄ canonicalizer; a minimization would help. The original proof was: `grind [Set.image_insert_eq, Set.image_singleton]` -/ simpa [Set.image_insert_eq, Set.image_singleton] using Cospherical.subtype_val h_cospherical' - have hf2 : Fact (finrank ℝ S.direction = 2) := ⟨by - rw [hS, direction_affineSpan, t.independent.finrank_vectorSpan] - simp⟩ - letI : Module.Oriented ℝ S.direction (Fin 2) := - ⟨Basis.orientation (finBasisOfFinrankEq _ _ hf2.out)⟩ have hncol : ¬ Collinear ℝ {p₁', p', p₃'} := by rw [← affineIndependent_iff_not_collinear_set, ← s_isom.toAffineMap.affineIndependent_iff s_isom.injective] convert hindep ext i; fin_cases i <;> rfl + have : Fact (finrank ℝ S.direction = 2) := Affine.Simplex.fact_finrank_direction_affineSpan_eq exact cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi_aux h_dist' hp₁'p₂' hp₃'p₄' hncol /-- **Intersecting Secants Theorem**. -/ diff --git a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean index b118fc3ce80573..831ba214cddf1c 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean @@ -168,6 +168,16 @@ theorem AffineIndependent.vectorSpan_eq_top_of_card_eq_finrank_add_one [FiniteDi vectorSpan k (Set.range p) = ⊤ := Submodule.eq_top_of_finrank_eq <| hi.finrank_vectorSpan hc +namespace Affine.Simplex + +/-- A convenience instance for use when restricting to the affine subspace spanned by the vertices +of a simplex. -/ +scoped instance fact_finrank_direction_affineSpan_eq {n : ℕ} {s : Simplex k P n} : + Fact (finrank k (affineSpan k (Set.range s.points)).direction = n) := + ⟨by rw [direction_affineSpan]; exact s.independent.finrank_vectorSpan (Fintype.card_fin _)⟩ + +end Affine.Simplex + variable (k) /-- The `vectorSpan` of `n + 1` points in an indexed family has diff --git a/Mathlib/LinearAlgebra/Orientation.lean b/Mathlib/LinearAlgebra/Orientation.lean index e4cad6ec900673..7af3a21607e0e7 100644 --- a/Mathlib/LinearAlgebra/Orientation.lean +++ b/Mathlib/LinearAlgebra/Orientation.lean @@ -191,6 +191,15 @@ theorem orientation_isEmpty [IsEmpty ι] (b : Basis ι R M) : end Module.Basis +namespace Module.Oriented.Arbitrary + +/-- An arbitrary choice of orientation. -/ +scoped instance (priority := 100) {n : ℕ} [Module.Finite R M] [Module.Free R M] + [Fact (finrank R M = n)] : Module.Oriented R M (Fin n) := + ⟨Basis.orientation (finBasisOfFinrankEq _ _ Fact.out)⟩ + +end Module.Oriented.Arbitrary + end OrderedCommRing section LinearOrderedCommRing