Theorems · Theorem · linear algebra

IsBaseChange.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 uM} [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 → Module.rank T P = Module.rank R M

Defined in

Mathlib.LinearAlgebra.Dimension.Localization

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAddCommGroupAddCommGroupModuleModuleAlgebraModuleIsScalarTowerIsLocalizationIsLocalizedModuleModule.FreeStrongRankConditionCommRingAlgebraStrongRankConditionAddCommGroupModuleModuleIsScalarTower