From eb1a9ac8a6d72b312e7cf8777805e7177fa7f766 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Thu, 18 Apr 2024 00:28:22 +0200 Subject: [PATCH] refactor, to be discussed: change FiniteDimensional.two_le_rank_of_rank_lt_rank to one_lt_rank.... This is what my application for ample sets expects; in this setting, both are proven the same way. To be discussed if this is a good change or not! --- SphereEversion/Global/Immersion.lean | 8 ++------ .../ToMathlib/LinearAlgebra/FiniteDimensional.lean | 4 ++-- 2 files changed, 4 insertions(+), 8 deletions(-) diff --git a/SphereEversion/Global/Immersion.lean b/SphereEversion/Global/Immersion.lean index 3db04846..19509b04 100644 --- a/SphereEversion/Global/Immersion.lean +++ b/SphereEversion/Global/Immersion.lean @@ -77,13 +77,9 @@ theorem immersionRel_ample (h : finrank ℝ E < finrank ℝ E') : (immersionRel rintro ⟨⟨m, m'⟩, φ : TangentSpace I m →L[ℝ] TangentSpace I' m'⟩ (p : DualPair (TangentSpace I m)) (hφ : Injective φ) haveI : FiniteDimensional ℝ (TangentSpace I m) := (by infer_instance : FiniteDimensional ℝ E) - have hcodim := two_le_rank_of_rank_lt_rank p.ker_pi_ne_top h φ.toLinearMap - -- FIXME: prove an analogue of `two_le_rank_of_rank_lt_rank` with `1 < ...` instead - have hcodim' : 1 < Module.rank ℝ (E' ⧸ Submodule.map (↑φ) (LinearMap.ker ↑p.π)) := by - rw [← Cardinal.two_le_iff_one_lt] - exact hcodim + have hcodim := one_lt_rank_of_rank_lt_rank p.ker_pi_ne_top h φ.toLinearMap rw [immersionRel_slice_eq I I' hφ] - exact AmpleSet.of_one_lt_codim hcodim' + exact AmpleSet.of_one_lt_codim hcodim /-- This is lemma `lem:open_ample_immersion` from the blueprint. -/ theorem immersionRel_open_ample (h : finrank ℝ E < finrank ℝ E') : diff --git a/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean b/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean index c090735e..70183d7d 100644 --- a/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean +++ b/SphereEversion/ToMathlib/LinearAlgebra/FiniteDimensional.lean @@ -5,9 +5,9 @@ open FiniteDimensional Submodule variable {𝕜 : Type*} [Field 𝕜] {E : Type*} [AddCommGroup E] [Module 𝕜 E] {E' : Type*} [AddCommGroup E'] [Module 𝕜 E'] -theorem two_le_rank_of_rank_lt_rank [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 E'] {π : E →ₗ[𝕜] 𝕜} +theorem one_lt_rank_of_rank_lt_rank [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 E'] {π : E →ₗ[𝕜] 𝕜} (hπ : LinearMap.ker π ≠ ⊤) (h : finrank 𝕜 E < finrank 𝕜 E') (φ : E →ₗ[𝕜] E') : - 2 ≤ Module.rank 𝕜 (E' ⧸ Submodule.map φ (LinearMap.ker π)) := by + 1 < Module.rank 𝕜 (E' ⧸ Submodule.map φ (LinearMap.ker π)) := by suffices 2 ≤ finrank 𝕜 (E' ⧸ π.ker.map φ) by rw [← finrank_eq_rank] exact_mod_cast this