Common refinements of chosen finite DVR extensions

Two chosen finite extensions E and F of a discrete valuation ring R admit a common refinement: a third chosen extension receiving maps from both, in the category TauCeti.FiniteDVRExtension.finiteDVRExtensionCategory. In categorical language this is a binary cofan on E and F; this file proves that one always exists.

A common field is easy: embed both extension fields into a separable closure of K and take the Galois closure N of the compositum. The chosen places need more care. Lying over gives primes of the integral closure of R in N above each chosen place separately, but they need not agree, and one cannot in general keep both embeddings. For example, if E and F have the same split quadratic extension field but different chosen places, one field embedding must be twisted. Since N / K is Galois, its Galois group acts transitively on the primes above the closed point of R, so one embedding can be twisted by an automorphism until the two primes coincide. The common prime then restricts to both chosen places, and TauCeti.FiniteDVRExtension.Hom.ofAlgHom upgrades the two field embeddings to maps of chosen extensions.

Main results

• TauCeti.FiniteDVRExtension.exists_isPrime_liesOver_comap_mapIntegralClosure_eq: the chosen place lifts along any embedding of the extension field.
• TauCeti.FiniteDVRExtension.exists_binaryCofan_of_isGalois: chosen extensions whose fields embed in a common finite Galois extension of K admit a common refinement with an explicit identification of its extension field with that field.
• TauCeti.FiniteDVRExtension.nonempty_binaryCofan: any two chosen extensions admit a common refinement.

References

The Galois-twist argument is the standard proof that some place of a compositum restricts to any prescribed pair of places, using transitivity of the Galois group on the places above a fixed one; see J. Neukirch, Algebraic Number Theory, Chapter II, §§8–9.

theorem TauCeti.FiniteDVRExtension.exists_isPrime_liesOver_comap_mapIntegralClosure_eq {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) (L : Type u_1) [CommRing L] [Nontrivial L] [Algebra R L] (k : E.extensionField →ₐ[R] L) : ∃ (Q : Ideal ↥(_root_.integralClosure R L)), Q.IsPrime ∧ Q.LiesOver (IsLocalRing.maximalIdeal R) ∧ Ideal.comap k.mapIntegralClosure Q = E.prime

The chosen place of a chosen extension lifts along any R-algebra embedding of its extension field into a nontrivial commutative ring L: some prime of the integral closure of R in L lies above the closed point of R and restricts to the chosen place.

theorem TauCeti.FiniteDVRExtension.exists_binaryCofan_of_isGalois {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E F : FiniteDVRExtension R K) (N : Type u) [Field N] [Algebra K N] [FiniteDimensional K N] [IsGalois K N] [Algebra R N] [IsScalarTower R K N] (k₁ : E.extensionField →ₐ[K] N) (k₂ : F.extensionField →ₐ[K] N) : ∃ (P : CategoryTheory.Limits.BinaryCofan E F), Nonempty (P.pt.extensionField ≃ₐ[K] N)

Chosen extensions whose extension fields embed over K into a common finite Galois extension N of K admit a common refinement whose extension field is K-isomorphic to N.

theorem TauCeti.FiniteDVRExtension.nonempty_binaryCofan {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E F : FiniteDVRExtension R K) : Nonempty (CategoryTheory.Limits.BinaryCofan E F)

Any two chosen finite extensions of a discrete valuation ring admit a common refinement: a chosen extension receiving maps from both, respecting the field embeddings and chosen places.