Unramifiedness descends along a tower of number fields

For a tower L / M / K of number fields, unramifiedness over K of every prime of 𝓞 L above a place of 𝓞 K descends to the primes of 𝓞 M above it. The prime-by-prime statement is TauCeti.RamificationInertia.isUnramifiedAt_of_isUnramifiedIn, proved there for an arbitrary base ring; what this file adds is the version quantified over the places outside a finite set, which is the shape the unramified-away hypotheses take.

The hypothesis and conclusion are stated as the quantified Algebra.IsUnramifiedAt condition rather than through Algebra.IsUnramifiedIn, which is the form the Artin symbol takes as its defining side condition.

The same descent, read simultaneously at every prime outside a finite set of finite places of K, is NumberField.isUnramifiedAway_of_intermediateField; that is the form a construction defined away from a finite set of primes consumes, since it turns one hypothesis about the top field into the corresponding hypothesis about every subextension.

Main results

• NumberField.isUnramifiedAway_of_intermediateField: unramifiedness outside a finite set of finite places descends to an intermediate field.

theorem NumberField.isUnramifiedAway_of_intermediateField {K : Type u_1} [Field K] [NumberField K] (M : Type u_2) [Field M] [NumberField M] {L : Type u_3} [Field L] [NumberField L] [Algebra K M] [Algebra M L] [Algebra K L] [IsScalarTower K M L] (S : Finset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (hur : ∀ v ∉ S, ∀ (Q : Ideal (RingOfIntegers L)) [inst : Q.IsPrime] [Q.LiesOver v.asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q) (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : v ∉ S → ∀ (Q : Ideal (RingOfIntegers M)) [inst : Q.IsPrime] [Q.LiesOver v.asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q

Unramifiedness outside a finite set of finite places descends to an intermediate field. If every prime of L above a place of K outside S is unramified over K, then so is every prime of an intermediate field M above such a place. This is what makes the unramified hypothesis for a subextension a consequence of the one for the top field rather than a second assumption.