Unramifiedness at a prime transports along an isomorphism of algebras

Algebra.IsUnramifiedAt R q says that the localization of the ambient algebra at q is formally unramified over R. An isomorphism ψ : A ≃ₐ[R] B of R-algebras matches the prime complement of q with that of q.comap ψ, so it induces an isomorphism of the two localizations over R and carries unramifiedness from q to q.comap ψ.

Main results

• AlgEquiv.isUnramifiedAt_of_eq_comap: if B is unramified at q over R, then A is unramified at any prime equal to q.comap ψ.

theorem AlgEquiv.isUnramifiedAt_of_eq_comap {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (ψ : A ≃ₐ[R] B) {q : Ideal B} [q.IsPrime] {p : Ideal A} [p.IsPrime] (hp : p = Ideal.comap ψ q) [Algebra.IsUnramifiedAt R q] : Algebra.IsUnramifiedAt R p

Unramifiedness transports along an isomorphism of R-algebras. If B is unramified over R at a prime q, then A is unramified over R at the corresponding prime q.comap ψ, stated for any prime p of A equal to it.