Maps and towers of chosen finite DVR extensions

The chosen place in a finite extension of a DVR is part of the data: a field embedding alone does not say how the corresponding local rings are related. This file therefore packages a compatible field embedding and local-ring map, with the square between them as an explicit law. These maps form the category of chosen extensions. It also records the finite separable field towers that occur between such extensions; these maps are the compatible pieces used by later common-refinement arguments.

A map is determined by its field component, and conversely a K-embedding of the extension fields under which the chosen places correspond extends uniquely to a map: the local-ring component is the localisation of the restriction of the field embedding to the integral closures. The existence of a common refinement for two arbitrary chosen extensions is proved in TauCeti.AlgebraicGeometry.Curves.StableReduction.DVRExtension.CommonRefinement.

Main declarations

• TauCeti.FiniteDVRExtension.Hom: a map of chosen extensions, and the category instance TauCeti.FiniteDVRExtension.finiteDVRExtensionCategory.
• TauCeti.FiniteDVRExtension.Hom.comap_prime: the chosen places correspond under the field component of a map.
• TauCeti.FiniteDVRExtension.Hom.ext_field: a map is determined by its field component.
• TauCeti.FiniteDVRExtension.Hom.ofAlgHom: the map extending a field embedding under which the chosen places correspond.

structure TauCeti.FiniteDVRExtension.Hom {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E F : FiniteDVRExtension R K) : Type u

A map of chosen finite DVR extensions.

field embeds the extension fields over K, while localMap embeds the selected local rings over R. The commutative-square law says that the field embedding restricts to the local-ring map. The local map is local, so the chosen closed point is respected rather than merely mapping one subring into another.

• field : E.extensionField →ₐ[K] F.extensionField

  The embedding of the extension fields over K.

• localMap : E.localRing →ₐ[R] F.localRing

  The map of chosen local rings over R.

• field_local (x : E.localRing) : self.field ((algebraMap E.localRing E.extensionField) x) = (algebraMap F.localRing F.extensionField) (self.localMap x)

  The field and local-ring maps commute with the fraction maps.

• isLocalHom_localMap : IsLocalHom self.localMap.toRingHom

  The map preserves the chosen maximal ideals.

theorem TauCeti.FiniteDVRExtension.Hom.ext {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} {f g : E.Hom F} (hfield : f.field = g.field) (hlocal : f.localMap = g.localMap) : f = g

Two maps are equal when their field and local-ring components agree.

@[instance_reducible]

instance TauCeti.FiniteDVRExtension.finiteDVRExtensionCategory {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] : CategoryTheory.Category.{u, u + 1} (FiniteDVRExtension R K)

Chosen extensions and their compatible maps form a category over a fixed R and K.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FiniteDVRExtension.Hom.id_field {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : (CategoryTheory.CategoryStruct.id E).field = AlgHom.id K E.extensionField

@[simp]

theorem TauCeti.FiniteDVRExtension.Hom.id_localMap {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] (E : FiniteDVRExtension R K) : (CategoryTheory.CategoryStruct.id E).localMap = AlgHom.id R E.localRing

@[simp]

theorem TauCeti.FiniteDVRExtension.Hom.comp_field {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F G : FiniteDVRExtension R K} (f : E ⟶ F) (g : F ⟶ G) : (CategoryTheory.CategoryStruct.comp f g).field = g.field.comp f.field

@[simp]

theorem TauCeti.FiniteDVRExtension.Hom.comp_localMap {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F G : FiniteDVRExtension R K} (f : E ⟶ F) (g : F ⟶ G) : (CategoryTheory.CategoryStruct.comp f g).localMap = g.localMap.comp f.localMap

@[simp]

theorem TauCeti.FiniteDVRExtension.Hom.localMap_algebraMap {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} (T : E ⟶ F) (x : E.integralClosure) : T.localMap ((algebraMap E.integralClosure E.localRing) x) = (algebraMap F.integralClosure F.localRing) ((AlgHom.restrictScalars R T.field).mapIntegralClosure x)

The local-ring component of a map agrees, on the integral closure, with the restriction of the field component to the integral closures.

@[simp]

theorem TauCeti.FiniteDVRExtension.Hom.comap_prime {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} (T : E ⟶ F) : Ideal.comap (AlgHom.restrictScalars R T.field).mapIntegralClosure F.prime = E.prime

The chosen places correspond under the field component of a map: the chosen prime of the target pulls back, along the restriction of the field embedding to the integral closures, to the chosen prime of the source.

theorem TauCeti.FiniteDVRExtension.Hom.ext_field {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} {f g : E ⟶ F} (h : f.field = g.field) : f = g

A map of chosen extensions is determined by its field component.

noncomputable def TauCeti.FiniteDVRExtension.Hom.ofAlgHom {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} (φ : E.extensionField →ₐ[K] F.extensionField) (hφ : Ideal.comap (AlgHom.restrictScalars R φ).mapIntegralClosure F.prime = E.prime) : E ⟶ F

The map of chosen extensions extending a K-embedding φ of the extension fields under which the chosen places correspond. Its local-ring component is the localisation of the restriction of φ to the integral closures.

Equations

• TauCeti.FiniteDVRExtension.Hom.ofAlgHom φ hφ = { field := φ, localMap := IsLocalization.liftAlgHom ⋯, field_local := ⋯, isLocalHom_localMap := ⋯ }

@[simp]

theorem TauCeti.FiniteDVRExtension.Hom.field_ofAlgHom {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} (φ : E.extensionField →ₐ[K] F.extensionField) (hφ : Ideal.comap (AlgHom.restrictScalars R φ).mapIntegralClosure F.prime = E.prime) : (ofAlgHom φ hφ).field = φ

@[instance_reducible]

def TauCeti.FiniteDVRExtension.Hom.fieldAlgebra {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} (T : E.Hom F) : Algebra E.extensionField F.extensionField

The algebra structure induced by the compatible field embedding.

Equations

• T.fieldAlgebra = T.field.toAlgebra

instance TauCeti.FiniteDVRExtension.Hom.fieldTower {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} (T : E.Hom F) : IsScalarTower K E.extensionField F.extensionField

The scalar tower induced by the compatible field embedding.

instance TauCeti.FiniteDVRExtension.Hom.fieldFinite {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} (T : E.Hom F) : FiniteDimensional E.extensionField F.extensionField

Finiteness of the upper field over the lower field follows from its finiteness over K.

instance TauCeti.FiniteDVRExtension.Hom.fieldSeparable {R K : Type u} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] [Field K] [Algebra R K] [IsFractionRing R K] {E F : FiniteDVRExtension R K} (T : E.Hom F) : Algebra.IsSeparable E.extensionField F.extensionField

Separability of the upper field over the lower field follows from its separability over K.