English
If A is finitely presented and e: A ≃ₐ[R] B is an algebra equivalence, then B is finitely presented; equivalently, finite presentation is preserved under algebraic equivalence.
Русский
Если A имеет конечную презентацию и e: A ≃ₐ[R] B, то B также имеет конечную презентацию; эквивалентность сохраняет конечную презентацию.
LaTeX
$$$[\\text{FinitePresentation } R A] \\Rightarrow \\text{FinitePresentation } R B$ given an AlgEquiv R A B$$
Lean4
/-- If `e : A ≃ₐ[R] B` and `A` is finitely presented, then so is `B`. -/
theorem equiv [FinitePresentation R A] (e : A ≃ₐ[R] B) : FinitePresentation R B :=
by
obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
use n, AlgHom.comp (↑e) f
constructor
· rw [AlgHom.coe_comp]
exact Function.Surjective.comp e.surjective hf.1
suffices (RingHom.ker (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom) = RingHom.ker f.toRingHom
by
rw [this]
exact hf.2
have hco : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom = RingHom.comp (e.toRingEquiv : A ≃+* B) f.toRingHom :=
by
have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom = e.toAlgHom.toRingHom.comp f.toRingHom := rfl
have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
rw [h, h1]
rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]
