Transport between isomorphic number-field extensions

This file records how properties of primes of rings of integers transport along an isomorphism of field extensions.

Main results

• AlgEquiv.forall_isUnramifiedAt_iff: unramifiedness above a base prime is invariant under an isomorphism of extensions.

theorem AlgEquiv.forall_isUnramifiedAt_iff {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Algebra K L] [Field L'] [Algebra K L'] (e : L ≃ₐ[K] L') (𝔭 : Ideal (NumberField.RingOfIntegers K)) : (∀ (Q : Ideal (NumberField.RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver 𝔭], Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q) ↔ ∀ (Q : Ideal (NumberField.RingOfIntegers L')) [inst : Q.IsPrime] [Q.LiesOver 𝔭], Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q

Unramifiedness above 𝔭 does not depend on the model of the extension.