English
If there exist compatible ring isomorphisms between base rings such that the corresponding algebras align, and one has finite over A1 B1, then the corresponding A2 B2 is finite.
Русский
При существовании совместимых кольцевых изоморфизмов между базами и согласованиях алгебр, если A1 B1финитны, то A2 B2 также финитны.
LaTeX
$$$\\forall (e_1 : A_1 \\simeq A_2) (e_2 : B_1 \\simeq B_2),\\; (he : (algebraMap A_2 B_2) \\circ e_1 = (algebraMap B_2 B_2) \\circ e_2) \\rightarrow [Module.Finite A_1 B_1] \\Rightarrow [Module.Finite A_2 B_2]$$
Lean4
theorem of_equiv_equiv {A₁ B₁ A₂ B₂ : Type*} [CommSemiring A₁] [CommSemiring B₁] [CommSemiring A₂] [Semiring B₂]
[Algebra A₁ B₁] [Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂) (e₂ : B₁ ≃+* B₂)
(he : RingHom.comp (algebraMap A₂ B₂) ↑e₁ = RingHom.comp ↑e₂ (algebraMap A₁ B₁)) [Module.Finite A₁ B₁] :
Module.Finite A₂ B₂ := by
letI := e₁.toRingHom.toAlgebra
letI := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
haveI : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq (fun x ↦ by simp [RingHom.algebraMap_toAlgebra])
let e : B₁ ≃ₐ[A₂] B₂ :=
{ e₂ with
commutes' := fun r ↦ by simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm r) }
haveI := Module.Finite.of_restrictScalars_finite A₁ A₂ B₁
exact Module.Finite.equiv e.toLinearEquiv
