Theorems · Theorem · linear algebra

IsBaseChange.lift_rank_eq_of_le_nonZeroDivisors

∀ {R : Type uR} (S : Type uS) {M : Type uM} {N : Type uN} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Algebra R S]
  [inst_7 : Module S N] [IsScalarTower R S N] {p : Submonoid R} [IsLocalization p S] (f : M →ₗ[R] N)
  [IsLocalizedModule p f],
  p ≤ nonZeroDivisors R →
    ∀ [Module.Free S N] [StrongRankCondition S] {T : Type uT} [inst_13 : CommRing T] [inst_14 : Algebra R T],
      Algebra.algebraMapSubmonoid T p ≤ nonZeroDivisors T →
        ∀ [StrongRankCondition (TensorProduct R S T)] {P : Type uP} [inst_16 : AddCommGroup P] [inst_17 : Module R P]
          [inst_18 : Module T P] [inst_19 : IsScalarTower R T P] {g : M →ₗ[R] P},
          IsBaseChange T g → Cardinal.lift.{uM, uP} (Module.rank T P) = Cardinal.lift.{uP, uM} (Module.rank R M)

Defined in

Mathlib.LinearAlgebra.Dimension.Localization

Cited by

3 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAddCommGroupAddCommGroupModuleModuleAlgebraModuleIsScalarTowerIsLocalizationIsLocalizedModuleModule.FreeStrongRankConditionCommRingAlgebraStrongRankConditionAddCommGroupModuleModuleIsScalarTower