review suggestions

leanprover-community · Jan 7, 2025 · 5000705 · 5000705
1 parent 4aef670
commit 5000705
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 10 deletions.
diff --git a/Mathlib/LinearAlgebra/Basis/Exact.lean b/Mathlib/LinearAlgebra/Basis/Exact.lean
@@ -71,11 +71,12 @@ private lemma top_le_span_of_aux (v : κ ⊕ σ → M)
 
 lemma Submodule.top_le_span_of_exact_of_retraction (hg : Function.Surjective g)
     (hsa : ∀ i, s (v (a i)) = 0) (hlib : LinearIndependent R (s ∘ v ∘ b))
-    (hab : Set.range (v ∘ a) ∪ Set.range (v ∘ b) = Set.range v)
+    (hab : Codisjoint (Set.range a) (Set.range b))
     (hsp : ⊤ ≤ Submodule.span R (Set.range v)) :
     ⊤ ≤ Submodule.span R (Set.range <| g ∘ v ∘ a) := by
   apply top_le_span_of_aux hs hfg (Sum.elim (v ∘ a) (v ∘ b)) hg hsa hlib
-  rwa [Set.Sum.elim_range, hab]
+  simp only [codisjoint_iff, Set.sup_eq_union, Set.top_eq_univ] at hab
+  rwa [Set.Sum.elim_range, Set.range_comp, Set.range_comp, ← Set.image_union, hab, Set.image_univ]
 
 /-- Let `0 → K → M → P → 0` be a split exact sequence of `R`-modules, let `s : M → K` be a
 retraction of `f` and `v` be a basis of `M` indexed by `κ ⊕ σ`. Then
@@ -86,7 +87,7 @@ For convenience this is stated for an arbitrary type `ι` with two maps `κ →
 noncomputable def Basis.ofSplitExact (hg : Function.Surjective g) (v : Basis ι R M)
     (hainj : Function.Injective a) (hsa : ∀ i, s (v (a i)) = 0)
     (hlib : LinearIndependent R (s ∘ v ∘ b))
-    (hab : Set.range (v ∘ a) ∪ Set.range (v ∘ b) = Set.range v) :
+    (hab : Codisjoint (Set.range a) (Set.range b)) :
     Basis κ R P :=
   Basis.mk (v.linearIndependent.linearIndependent_of_exact_of_retraction hs hfg hainj hsa)
     (Submodule.top_le_span_of_exact_of_retraction hs hfg hg hsa hlib hab (by rw [v.span_eq]))
diff --git a/Mathlib/LinearAlgebra/Dimension/Finite.lean b/Mathlib/LinearAlgebra/Dimension/Finite.lean
@@ -72,6 +72,12 @@ lemma rank_eq_zero_iff :
     apply ha
     simpa using DFunLike.congr_fun (linearIndependent_iff.mp hs (Finsupp.single i a) (by simpa)) i
 
+/-- A free module of rank zero is trivial. -/
+lemma subsingleton_of_rank_zero [StrongRankCondition R] [Free R M] (h : Module.rank R M = 0) :
+    Subsingleton M := by
+  rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h
+  exact (Module.Free.repr R M).subsingleton
+
 variable [Nontrivial R]
 
 section

diff --git a/Mathlib/LinearAlgebra/Dimension/Free.lean b/Mathlib/LinearAlgebra/Dimension/Free.lean
@@ -165,11 +165,6 @@ variable {M M'}
 
 namespace Module
 
-/-- A free module of rank zero is trivial. -/
-lemma subsingleton_of_rank_zero (h : Module.rank R M = 0) : Subsingleton M := by
-  rw [← Basis.mk_eq_rank'' (Module.Free.chooseBasis R M), Cardinal.mk_eq_zero_iff] at h
-  exact (Module.Free.repr R M).subsingleton
-
 /-- See `rank_lt_aleph0` for the inverse direction without `Module.Free R M`. -/
 lemma rank_lt_aleph0_iff : Module.rank R M < ℵ₀ ↔ Module.Finite R M := by
   rw [Free.rank_eq_card_chooseBasisIndex, mk_lt_aleph0_iff]

diff --git a/Mathlib/RingTheory/Smooth/StandardSmooth.lean b/Mathlib/RingTheory/Smooth/StandardSmooth.lean
@@ -501,8 +501,8 @@ noncomputable def aevalDifferentialEquiv (P : SubmersivePresentation R S) :
         P.aevalDifferential).det := by
     convert P.jacobian_isUnit
     rw [LinearMap.toMatrix_eq_toMatrix', jacobian_eq_jacobiMatrix_det,
-      aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix]
-    simp [RingHom.map_det, RingHom.algebraMap_toAlgebra]
+      aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, P.algebraMap_eq]
+    simp [RingHom.map_det]
   LinearEquiv.ofIsUnitDet this
 
 variable (P : SubmersivePresentation R S)