The completed integer rings of an extension of Dedekind domains

Let R ⊆ B be Dedekind domains with fraction fields K ⊆ L, and let w be a height-one prime of B lying over the height-one prime v of R. The canonical map K_v → L_w restricts to a ring homomorphism adicCompletionIntegersExtension : 𝒪_v →+* 𝒪_w between the rings of integers of the two completions.

This file turns that restriction into an algebra structure of 𝒪_w over 𝒪_v, in the AdicCompletionExtension scope where the algebra structure of L_w over K_v already lives, and proves the facts needed to use the extension 𝒪_w / 𝒪_v as an extension of Dedekind domains: it is compatible with L_w as a K_v-algebra, it is torsion-free, it is compatible with the global map R → B, and the maximal ideal of 𝒪_w lies over that of 𝒪_v. These are the hypotheses that ideal-theoretic constructions such as differentIdeal 𝒪_v 𝒪_w, Ideal.LiesOver, and the ramification index and inertia degree of 𝒪_w / 𝒪_v take as input, and they make the local extension comparable with the global one along B → 𝒪_w.

Main definitions

• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersExtensionAlgebra: the algebra structure of 𝒪_w over 𝒪_v given by adicCompletionIntegersExtension, available in the AdicCompletionExtension scope.

Main results

• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersExtension_injective: the map on completed integer rings is injective.
• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersExtension_algebraMap: it extends the global map R → B.
• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers_isScalarTower: 𝒪_v, 𝒪_w and L_w form a scalar tower, so the two ways of letting 𝒪_v act on L_w agree.
• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers_isTorsionFree: 𝒪_w is a torsion-free 𝒪_v-module.
• IsDedekindDomain.HeightOneSpectrum.isLocalHom_algebraMap_adicCompletionIntegers: the canonical map 𝒪_v → 𝒪_w is a local ring homomorphism.
• IsDedekindDomain.HeightOneSpectrum.maximalIdeal_adicCompletionIntegers_liesOver: the maximal ideal of 𝒪_w lies over the maximal ideal of 𝒪_v.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §4 and §6.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersExtension_injective {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] : Function.Injective ⇑(adicCompletionIntegersExtension K L v w)

The map 𝒪_v → 𝒪_w on completed integer rings is injective: it is a restriction of a ring homomorphism out of the field K_v.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersExtension_algebraMap {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (r : R) : (adicCompletionIntegersExtension K L v w) ((algebraMap R ↥(adicCompletionIntegers K v)) r) = (algebraMap B ↥(adicCompletionIntegers L w)) ((algebraMap R B) r)

The map 𝒪_v → 𝒪_w on completed integer rings extends the global map R → B.

@[reducible]

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersExtensionAlgebra {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] : Algebra ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w)

The algebra structure on 𝒪_w over 𝒪_v induced by adicCompletionIntegersExtension, available in the AdicCompletionExtension scope.

Equations

• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersExtensionAlgebra K L v w = (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersExtension K L v w).toAlgebra

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegersExtensionAlgebra {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] : algebraMap ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w) = adicCompletionIntegersExtension K L v w

The algebra map of adicCompletionIntegersExtensionAlgebra is adicCompletionIntegersExtension.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers_isScalarTower {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] : IsScalarTower (↥(adicCompletionIntegers K v)) (↥(adicCompletionIntegers L w)) (adicCompletion L w)

The completed integer rings 𝒪_v ⊆ 𝒪_w and the completion L_w form a scalar tower. Here 𝒪_v acts on L_w through K_v, so this says the two ways of letting 𝒪_v act on L_w agree.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers_isTorsionFree {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] : Module.IsTorsionFree ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w)

𝒪_w is a torsion-free 𝒪_v-module.

theorem IsDedekindDomain.HeightOneSpectrum.isLocalHom_algebraMap_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] : IsLocalHom (algebraMap ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w))

The canonical map 𝒪_v → 𝒪_w of completed integer rings is a local ring homomorphism.

theorem IsDedekindDomain.HeightOneSpectrum.maximalIdeal_adicCompletionIntegers_liesOver {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] (L : Type u_4) [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] : (IsLocalRing.maximalIdeal ↥(adicCompletionIntegers L w)).LiesOver (IsLocalRing.maximalIdeal ↥(adicCompletionIntegers K v))

The maximal ideal of 𝒪_w lies over the maximal ideal of 𝒪_v.