finrank_bot_le_finrank_of_isScalarTower_of_free

English

If M is finite over S and there is a scalar tower, then finrank_R S ≤ finrank_R T for S → T.

Русский

При башне скаляров R → S → T и конечности M над S, финразмерность S ≤ финразмерность T.

LaTeX

$$$$ \\text{finrank}_R(S) \\le \\text{finrank}_R(T) $$$$

Lean4

/-- Also see `Module.finrank_bot_le_finrank_of_isScalarTower`
for a version with different typeclass constraints. -/
theorem finrank_bot_le_finrank_of_isScalarTower_of_free (S T : Type*) [Semiring S] [Semiring T] [Module R T]
    [Module S T] [Module R S] [IsScalarTower R S T] [IsScalarTower S T T] [FaithfulSMul S T] [Module.Finite S T]
    [Module.Free R S] : finrank R S ≤ finrank R T :=
  by
  by_cases H : Module.Finite R S
  · have := Module.Finite.trans (R := R) S T
    exact finrank_bot_le_finrank_of_isScalarTower R S T
  · rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
    · exact zero_le _
    · rwa [← not_lt, Module.rank_lt_aleph0_iff]

Похожие утверждения