feat(Algebra/Module/SpanRank): add comparing lemmas for span rank

[sun123zxy]

---

Split from PR #33247

[github-actions]

PR summary e78e242c45

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ le_spanRank_restrictScalars
+ spanFinrank_map_le_of_fg
+ spanRank_eq_spanRank_of_equiv
+ spanRank_eq_spanRank_of_equiv'
+ spanRank_le_spanRank_of_map_eq
+ spanRank_le_spanRank_of_range_eq
+ spanRank_le_spanRank_of_surjective
+ spanRank_map_le
+ spanRank_restrictScalars_eq
- Submodule.spanFinrank_map_le_of_fg
- Submodule.spanRank_map_le

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[erdOne]

I would argue that we don't want lemmas that mention linear maps between submodules.

I think what we want is something like

lemma spanRank_map_eq {σ : R →+* S} [RingHomSurjective σ]
    (f : M →ₛₗ[σ] N) (hf : Function.Injective f) (p : Submodule R M) :
    (p.map f).spanRank = p.spanRank := by
  refine (spanRank_map_le f p).antisymm ?_
  obtain ⟨s, hs, e⟩ := (p.map f).exists_span_set_card_eq_spanRank
  obtain ⟨s, rfl⟩ : ∃ y, f '' y = s := Set.subset_range_iff_exists_image_eq.mp
    ((subset_span.trans e.le).trans LinearMap.map_le_range)
  obtain rfl : span R s = p := by simpa [(map_injective_of_injective hf).eq_iff] using e
  grw [← hs, spanRank_span_le_card, Cardinal.mk_image_eq hf]

lemma spanRank_range_le {σ : R →+* S} [RingHomSurjective σ]
    (f : M →ₛₗ[σ] N) : (LinearMap.range f).spanRank ≤ (⊤ : Submodule R M).spanRank := by
  simpa using spanRank_map_le f ⊤

@[simp]
lemma spanRank_top_eq_spanRank (p : Submodule R M) :
    (⊤ : Submodule R p).spanRank = p.spanRank := by
  simpa using (spanRank_map_eq _ p.subtype_injective ⊤).symm

And then for example if you really want spanRank_le_spanRank_of_range_eq you can get it via simpa [*] using spanRank_range_le f, which I argue you can just do inline.

[erdOne]

This might be a better approach:

variable {R S : Type*} {M : Type u} [CommSemiring R] [Semiring S] [AddCommMonoid M]
  [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M]

lemma le_spanRank_restrictScalars
    (N : Submodule S M) : N.spanRank ≤ (N.restrictScalars R).spanRank := by
  obtain ⟨s, hs, e⟩ := (N.restrictScalars R).exists_span_set_card_eq_spanRank
  obtain rfl : span S s = N :=
    le_antisymm (span_le.mpr (span_le.mp e.le:)) (e.ge.trans (span_le_restrictScalars R S s))
  grw [← hs, spanRank_span_le_card]

lemma spanRank_restrictScalars_eq (H : Function.Surjective (algebraMap R S))
    (N : Submodule S M) : (N.restrictScalars R).spanRank = N.spanRank := by
  refine N.le_spanRank_restrictScalars.antisymm' ?_
  obtain ⟨s, hs, rfl⟩ := N.exists_span_set_card_eq_spanRank
  grw [restrictScalars_span R S H s, ← hs, spanRank_span_le_card]

[sun123zxy]

I would argue that we don't want lemmas that mention linear maps between submodules.

I think what we want is something like

lemma spanRank_map_eq {σ : R →+* S} [RingHomSurjective σ]
    (f : M →ₛₗ[σ] N) (hf : Function.Injective f) (p : Submodule R M) :
    (p.map f).spanRank = p.spanRank := by
  refine (spanRank_map_le f p).antisymm ?_
  obtain ⟨s, hs, e⟩ := (p.map f).exists_span_set_card_eq_spanRank
  obtain ⟨s, rfl⟩ : ∃ y, f '' y = s := Set.subset_range_iff_exists_image_eq.mp
    ((subset_span.trans e.le).trans LinearMap.map_le_range)
  obtain rfl : span R s = p := by simpa [(map_injective_of_injective hf).eq_iff] using e
  grw [← hs, spanRank_span_le_card, Cardinal.mk_image_eq hf]

lemma spanRank_range_le {σ : R →+* S} [RingHomSurjective σ]
    (f : M →ₛₗ[σ] N) : (LinearMap.range f).spanRank ≤ (⊤ : Submodule R M).spanRank := by
  simpa using spanRank_map_le f ⊤

@[simp]
lemma spanRank_top_eq_spanRank (p : Submodule R M) :
    (⊤ : Submodule R p).spanRank = p.spanRank := by
  simpa using (spanRank_map_eq _ p.subtype_injective ⊤).symm

And then for example if you really want spanRank_le_spanRank_of_range_eq you can get it via simpa [*] using spanRank_range_le f, which I argue you can just do inline.

If so, I think I'll apply these changes, remove spanRank_le_spanRank_of_range_eq, spanRank_le_spanRank_of_map_eq but keep spanRank_le_spanRank_of_surjective and the equiv statements. Does this look good to you?