Rank theorems over domains

This file proves some Module.rank and Module.finrank theorems for modules over domains.

Main results

Let M/S/R be a tower where R, S are domains.

We obtain the following tower laws:

• Module.rank_mul_rank_of_isFractionRing_isLocalization & variants: when (R⁰)⁻¹ S = (S⁰)⁻¹ S.
• Module.rank_mul_rank_of_field_isLocalization & variants: wrapper for the above that only asks (R⁰)⁻¹ S to be a field.
• Module.IsTorsionFree.erank_mul_erank, Module.IsTorsionFree.finrank_mul_finrank: when M is torsion-free over S. We only get truncated cardinalities.
• Algebra.IsAlgebraic.rank_mul_rank & variants: when S/R is algebraic.

theorem Module.lift_rank_mul_lift_rank_of_isFractionRing_isLocalization (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] (FS : Type u_2) [CommRing FS] [Algebra S FS] [IsFractionRing S FS] [h : IsLocalization (Algebra.algebraMapSubmonoid S (nonZeroDivisors R)) FS] (M : Type w) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : Cardinal.lift.{w, v} (Module.rank R S) * Cardinal.lift.{v, w} (Module.rank S M) = Cardinal.lift.{v, w} (Module.rank R M)

Tower law over domains. When M is a module over an algebra S/R of domains such that (R⁰)⁻¹ S = (S⁰)⁻¹ S, we obtain a tower law.

See _root.lift_rank_mul_lift_rank for when your modules are free.

theorem Module.rank_mul_rank_of_isFractionRing_isLocalization (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] (FS : Type u_2) [CommRing FS] [Algebra S FS] [IsFractionRing S FS] [h : IsLocalization (Algebra.algebraMapSubmonoid S (nonZeroDivisors R)) FS] (M₁ : Type v) [AddCommGroup M₁] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] : Module.rank R S * Module.rank S M₁ = Module.rank R M₁

Tower law over domains. When M is a module over an algebra S/R of domains such that (R⁰)⁻¹ S = (S⁰)⁻¹ S, we obtain a tower law.

See _root.rank_mul_rank for when your modules are free.

theorem Module.finrank_mul_finrank_of_isFractionRing_isLocalization (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] (FS : Type u_2) [CommRing FS] [Algebra S FS] [IsFractionRing S FS] [h : IsLocalization (Algebra.algebraMapSubmonoid S (nonZeroDivisors R)) FS] (M : Type w) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : finrank R S * finrank S M = finrank R M

Tower law over domains. When M is a module over an algebra S/R of domains such that (R⁰)⁻¹ S = (S⁰)⁻¹ S, we obtain a tower law.

See Module.finrank_mul_finrank for when your modules are free.

theorem Module.lift_rank_mul_lift_rank_of_field_isLocalization (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] (FS : Type u_2) [Field FS] [Algebra S FS] [h : IsLocalization (Algebra.algebraMapSubmonoid S (nonZeroDivisors R)) FS] (M : Type w) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : Cardinal.lift.{w, v} (Module.rank R S) * Cardinal.lift.{v, w} (Module.rank S M) = Cardinal.lift.{v, w} (Module.rank R M)

Tower law over domains. When M is a module over an algebra S/R of domains such that (R⁰)⁻¹ S is a field, we obtain a tower law.

See _root.lift_rank_mul_lift_rank for when your modules are free.

theorem Module.rank_mul_rank_of_field_isLocalization (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] (FS : Type u_2) [Field FS] [Algebra S FS] [h : IsLocalization (Algebra.algebraMapSubmonoid S (nonZeroDivisors R)) FS] (M₁ : Type v) [AddCommGroup M₁] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] : Module.rank R S * Module.rank S M₁ = Module.rank R M₁

Tower law over domains. When M is a module over an algebra S/R of domains such that (R⁰)⁻¹ S is a field, we obtain a tower law.

See _root.rank_mul_rank for when your modules are free.

theorem Module.finrank_mul_finrank_of_field_isLocalization (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] (FS : Type u_2) [Field FS] [Algebra S FS] [h : IsLocalization (Algebra.algebraMapSubmonoid S (nonZeroDivisors R)) FS] (M : Type w) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : finrank R S * finrank S M = finrank R M

Tower law over domains. When M is a module over an algebra S/R of domains such that (R⁰)⁻¹ S is a field, we obtain a tower law.

See Module.finrank_mul_finrank for when your modules are free.

theorem Module.IsTorsionFree.erank_mul_erank (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] (M : Type w) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [IsTorsionFree S M] : Cardinal.toENat (Module.rank R S) * Cardinal.toENat (Module.rank S M) = Cardinal.toENat (Module.rank R M)

Tower law for torsion-free modules. The tower law for ENat Module.rank of a S-torsion-free module over an algebra S/R of domains. See Module.IsTorsionFree.finrank_mul_finrank for a finrank version.

theorem Module.IsTorsionFree.finrank_mul_finrank (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] (M : Type w) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [IsTorsionFree S M] : finrank R S * finrank S M = finrank R M

Tower law for torsion-free modules. The tower law for Module.finrank of a S-torsion-free module over an algebra S/R of domains. See Module.finrank_mul_finrank for when your modules are free.

theorem Algebra.IsAlgebraic.lift_rank_mul_lift_rank (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] [Algebra.IsAlgebraic R S] (M : Type w) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : Cardinal.lift.{w, v} (Module.rank R S) * Cardinal.lift.{v, w} (Module.rank S M) = Cardinal.lift.{v, w} (Module.rank R M)

Tower law over algebraic extensions of domains. If S has no zero divisors, S is algebraic over R, and M is a S-module, then $$\operatorname{rank}_R(S) * \operatorname{rank}_S(M) = \operatorname{rank}_R(M)$$.

See Algebra.IsAlgebraic.rank_mul_rank for a non–universe polymorphic version, and _root_.lift_rank_mul_lift_rank for when your modules are free.

theorem Algebra.IsAlgebraic.rank_mul_rank (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] [Algebra.IsAlgebraic R S] (M₁ : Type v) [AddCommGroup M₁] [Module R M₁] [Module S M₁] [IsScalarTower R S M₁] : Module.rank R S * Module.rank S M₁ = Module.rank R M₁

Tower law over algebraic extensions of domains. If S has no zero divisors, S is algebraic over R, and M is a S-module, then $$\operatorname{rank}_R(S) * \operatorname{rank}_S(M) = \operatorname{rank}_R(M)$$.

See Algebra.IsAlgebraic.lift_rank_mul_lift_rank for a universe polymorphic version, and _root_.rank_mul_rank for when your modules are free.

theorem Algebra.IsAlgebraic.finrank_mul_finrank (R : Type u_1) (S : Type v) [CommRing R] [CommRing S] [NoZeroDivisors S] [Algebra R S] [Algebra.IsAlgebraic R S] (M : Type w) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : Module.finrank R S * Module.finrank S M = Module.finrank R M

Tower law over algebraic extensions of domains. If S has no zero divisors, S is algebraic over R, and M is a S-module, then $$\operatorname{rank}_R(S) * \operatorname{rank}_S(M) = \operatorname{rank}_R(M)$$.

See Module.finrank_mul_finrank for when your modules are free.