English
If i : R0 ≃+* R1 and j : S0 ≃+* S1 are ring isomorphisms commuting with the structure maps, then finrank_R0 S0 = finrank_R1 S1.
Русский
Пусть i, j — кольцевые изоморфизмы, совместимые с алгебрными отображениями; тогда finrank_R0 S0 = finrank_R1 S1.
LaTeX
$$$\\mathrm{Module.finrank}\, R_0 S_0 = \\mathrm{Module.finrank}\\, R_1 S_1$$$
Lean4
/-- If `S₀ / R₀` and `S₁ / R₁` are algebras, `i : R₀ ≃+* R₁` and `j : S₀ ≃+* S₁` are
ring isomorphisms, such that `R₀ → R₁ → S₁` and `R₀ → S₀ → S₁` commute,
then the `finrank` of `S₀ / R₀` is equal to the finrank of `S₁ / R₁`. -/
theorem finrank_eq_of_equiv_equiv {R₀ S₀ : Type*} [CommSemiring R₀] [Semiring S₀] [Algebra R₀ S₀] {R₁ S₁ : Type*}
[CommSemiring R₁] [Semiring S₁] [Algebra R₁ S₁] (i : R₀ ≃+* R₁) (j : S₀ ≃+* S₁)
(hc : (algebraMap R₁ S₁).comp i.toRingHom = j.toRingHom.comp (algebraMap R₀ S₀)) :
Module.finrank R₀ S₀ = Module.finrank R₁ S₁ := by
simpa using (congr_arg Cardinal.toNat (lift_rank_eq_of_equiv_equiv i j hc))
