feat(RingTheory/Algebraic): tower law for Module.finrank over domains

[xroblot]

Adds Module.finrank_mul_finrank', a variant of the tower law finrank R S * finrank S T = finrank R T for a tower of domains R → S → T.

---

[github-actions]

PR summary e404830901

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ _root_.Module.finrank_mul_finrank'

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e404830).

• +1 new declarations
• −0 removed declarations

+Module.finrank_mul_finrank'

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit e404830901
Reference commit c368140668

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[tb65536]

You can replace the finiteness assumptions with [Algebra.IsAlgebraic S T] (since algebraic is transitive).

[tb65536]

Actually, I haven't golfed this yet, but you can remove a lot of the assumptions from finrank_of_isFractionRing!

theorem _root_.Module.rank_eq_zero_of_not_faithfulSMul
    {R S : Type*} [Semiring R] [AddCommMonoid S] [Module R S]
    (h : ¬ FaithfulSMul R S) : Module.rank R S = 0 := by
  contrapose! h
  rw [← Cardinal.one_le_iff_ne_zero, Module.one_le_rank_iff] at h
  obtain ⟨f, hf⟩ := h
  refine ⟨fun {x y} h ↦ hf ?_⟩
  have := f.map_smul x 1
  have := f.map_smul y 1
  simp_all

theorem _root_.Module.finrank_eq_zero_of_not_faithfulSMul
    {R S : Type*} [Semiring R] [AddCommMonoid S] [Module R S]
    (h : ¬ FaithfulSMul R S) : Module.finrank R S = 0 :=
  Module.finrank_eq_zero_of_rank_eq_zero (Module.rank_eq_zero_of_not_faithfulSMul h)

theorem _root_.Transcendental.linearIndependent_pow
    {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] {x : S}
    (h : Transcendental R x) : LinearIndependent R (x ^ ·) := by
  sorry

theorem _root_.Module.finrank_eq_zero_of_not_isAlgebraic
    {R S : Type*} [CommRing R] [Nontrivial R] [CommRing S] [Algebra R S]
    (h : ¬ Algebra.IsAlgebraic R S) : Module.finrank R S = 0 := by
  rw [Algebra.isAlgebraic_def, not_forall] at h
  obtain ⟨x, hx : Transcendental R x⟩ := h
  exact Cardinal.toNat_apply_of_aleph0_le hx.linearIndependent_pow.aleph0_le_rank

theorem _root_.Algebra.IsAlgebraic.finrank_of_isFractionRing' (R R' S S' : Type*)
    [CommRing R] [CommRing R'] [CommRing S] [CommRing S']
    [Algebra R S] [Algebra R R'] [Algebra S S'] [Algebra R' S'] [Algebra R S']
    [IsScalarTower R R' S'] [IsScalarTower R S S']
    [IsFractionRing R R'] [IsFractionRing S S']
    [NoZeroDivisors S] : Module.finrank R' S' = Module.finrank R S := by
  rcases iff_iff_and_or_not_and_not.mp (IsFractionRing.nontrivial_iff_nontrivial R R')
    with ⟨_, _⟩ | ⟨_, _⟩; swap
  · rw [not_nontrivial_iff_subsingleton] at *
    simp
  by_cases hfs : FaithfulSMul R S; swap
  · rw [Module.finrank_eq_zero_of_not_faithfulSMul hfs]
    replace hfs : ¬ FaithfulSMul R' S' := by
      contrapose! hfs
      rw [faithfulSMul_iff_algebraMap_injective] at *
      have : Function.Injective (algebraMap S S') := FaithfulSMul.algebraMap_injective S S'
      apply Function.Injective.of_comp (f := algebraMap S S')
      rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq R R' S']
      apply hfs.comp
      exact FaithfulSMul.algebraMap_injective R R'
    rw [Module.finrank_eq_zero_of_not_faithfulSMul hfs]
  · have : NoZeroDivisors R := NoZeroDivisors.of_faithfulSMul R S
    have : NoZeroDivisors R' := IsLocalization.noZeroDivisors R⁰
    by_cases halg : Algebra.IsAlgebraic R S
    · apply finrank_of_isFractionRing
    · rw [Module.finrank_eq_zero_of_not_isAlgebraic halg]
      replace halg : ¬ Algebra.IsAlgebraic R' S' := by
        contrapose! halg
        have : Algebra.IsAlgebraic R R' := IsLocalization.isAlgebraic R' R⁰
        have : Algebra.IsAlgebraic R S' := Algebra.IsAlgebraic.trans R R' S'
        apply Algebra.IsAlgebraic.tower_bot_of_injective (R := R) (S := S) (A := S')
        exact FaithfulSMul.algebraMap_injective S S'
      rw [Module.finrank_eq_zero_of_not_isAlgebraic halg]

[tb65536]

(although actually there might just be a more direct proof with localizations)