ClassFieldTower.Sawin.IsUnramifiedAtFinitePlacesOutside.congrTop
Replacing the top number field by an equivalent algebra preserves unramifiedness outside the same set of finite places of the base.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
namespace ClassFieldTower.Sawin.IsUnramifiedAtFinitePlacesOutsideLean source · statement
theorem congrTop
{K : Type u} {L : Type v} {M : Type w}
[Field K] [NumberField K]
[Field L] [NumberField L]
[Field M] [NumberField M]
[Algebra K L] [Algebra K M]
(e : L ≃ₐ[K] M) {S : Set (HeightOneSpectrum (𝓞 K))}
(h : IsUnramifiedAtFinitePlacesOutside K L S) :
IsUnramifiedAtFinitePlacesOutside K M S