Intrinsic and affine-model completions

The intrinsic completion at the place attached to a height-one prime of a Dedekind k-algebra is canonically the prime's adic completion. The comparison is a continuous k-algebra equivalence preserving the normalized valuation. It restricts to the valuation rings, identifies their maximal ideals and residue fields, and commutes with the original field embeddings and reduction maps. Maximal-ideal compatibility follows from Mathlib's IsLocalRing.map_ringEquiv_maximalIdeal applied to the valuation-ring equivalence. Thus local calculations made with places can be used in the adic completions appearing in finite adeles.

The field comparison uses Mathlib's HeightOneSpectrum.adicCompletion.equiv and adicCompletion.uniformEquiv; the residue comparison uses IsLocalRing.ResidueField.mapAlgEquiv. No finiteness assumption on the residue fields is needed.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Section I.7.

noncomputable def TauCeti.Place.completionEquivAdicCompletionOfValuationEq (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra R F] [IsFractionRing R F] [Algebra k F] (p : IsDedekindDomain.HeightOneSpectrum R) (P : Place k F) (hP : P.valuation = IsDedekindDomain.HeightOneSpectrum.valuation F p) : P.Completion ≃A[k] IsDedekindDomain.HeightOneSpectrum.adicCompletion F p

The completion of a place with the affine model's valuation is its adic completion, over the constants. The equality transports the dependent completion structures.

Equations

• TauCeti.Place.completionEquivAdicCompletionOfValuationEq k F p P hP = { toAlgEquiv := AlgEquiv.ofRingEquiv ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

noncomputable def TauCeti.Place.completionEquivAdicCompletion (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : (ofPrime k F p).Completion ≃A[k] IsDedekindDomain.HeightOneSpectrum.adicCompletion F p

The completion of the adic place is the affine-model adic completion, over the constants.

Equations

• TauCeti.Place.completionEquivAdicCompletion k F p = TauCeti.Place.completionEquivAdicCompletionOfValuationEq k F p (TauCeti.Place.ofPrime k F p) ⋯

@[simp]

theorem TauCeti.Place.completionEquivAdicCompletion_completionEmbedding (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (x : F) : (completionEquivAdicCompletion k F p) ((ofPrime k F p).completionEmbedding x) = (algebraMap F (IsDedekindDomain.HeightOneSpectrum.adicCompletion F p)) x

The comparison carries the intrinsic field embedding to the adic field embedding.

@[simp]

theorem TauCeti.Place.valuation_completionEquivAdicCompletion (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (x : (ofPrime k F p).Completion) : Valued.v ((completionEquivAdicCompletion k F p) x) = (ofPrime k F p).completionPlace.valuation x

The comparison preserves the normalized valuation on completed functions.

@[simp]

theorem TauCeti.Place.isUniformizer_completionEquivAdicCompletion_iff (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (x : (ofPrime k F p).Completion) : Valued.v.IsUniformizer ((completionEquivAdicCompletion k F p) x) ↔ (ofPrime k F p).completionPlace.valuation.IsUniformizer x

The comparison preserves uniformizers for the normalized completed valuations.

@[simp]

theorem TauCeti.Place.completionEquivAdicCompletion_mem_integers_iff (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (x : (ofPrime k F p).Completion) : (completionEquivAdicCompletion k F p) x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F p ↔ x ∈ (ofPrime k F p).completionPlace.integers

The field comparison identifies the two rings of integers.

noncomputable def TauCeti.Place.completionIntegersEquivAdicCompletionIntegers (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : ↥(ofPrime k F p).completionPlace.integers ≃A[k] ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F p)

The continuous restriction of the completion comparison to the two valuation rings, over the constants.

Equations

• TauCeti.Place.completionIntegersEquivAdicCompletionIntegers k F p = { toAlgEquiv := AlgEquiv.ofRingEquiv ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.Place.completionIntegersEquivAdicCompletionIntegers_apply (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (x : ↥(ofPrime k F p).completionPlace.integers) : ↑((completionIntegersEquivAdicCompletionIntegers k F p) x) = (completionEquivAdicCompletion k F p) ↑x

The valuation-ring comparison is the restriction of the field comparison.

@[simp]

theorem TauCeti.Place.completionIntegersEquivAdicCompletionIntegers_completionIntegersEmbedding_algebraMap (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (r : R) : (completionIntegersEquivAdicCompletionIntegers k F p) ((ofPrime k F p).completionIntegersEmbedding ((algebraMap R ↥(ofPrime k F p).integers) r)) = (algebraMap R ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F p)) r

The valuation-ring comparison carries completed model elements to their adic images.

noncomputable def TauCeti.Place.completionResidueFieldEquivAdicCompletionIntegers (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : (ofPrime k F p).completionPlace.ResidueField ≃ₐ[k] IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers F p)

The completed residue fields agree under the valuation-ring comparison.

Equations

• TauCeti.Place.completionResidueFieldEquivAdicCompletionIntegers k F p = IsLocalRing.ResidueField.mapAlgEquiv (TauCeti.Place.completionIntegersEquivAdicCompletionIntegers k F p).toAlgEquiv

theorem TauCeti.Place.completionResidueFieldEquivAdicCompletionIntegers_apply_algebraMap (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (r : R) : (completionResidueFieldEquivAdicCompletionIntegers k F p) ((ofPrime k F p).residueFieldEquivCompletion ((algebraMap R (ofPrime k F p).ResidueField) r)) = (residueFieldAlgEquivAdicCompletionIntegers k) ((Ideal.Quotient.mk p.asIdeal) r)

Both residue comparison routes agree on each affine-model representative.

theorem TauCeti.Place.residueFieldAlgEquivAdicCompletionIntegers_eq_trans (k : Type u_1) (F : Type u_2) {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : residueFieldAlgEquivAdicCompletionIntegers k = (quotientAlgEquivResidueFieldOfPrime k F p).trans ((ofPrime k F p).residueFieldEquivCompletion.trans (completionResidueFieldEquivAdicCompletionIntegers k F p))

The affine-model residue equivalence is the composite of quotientAlgEquivResidueFieldOfPrime, residueFieldEquivCompletion, and completionResidueFieldEquivAdicCompletionIntegers.