The two-chart model is a relative normalization

Let F' / F be an integral extension of algebraic function fields over k, let x ∈ F be transcendental over k, and let x' ∈ F' be its image. The morphism of two-chart models map : twoChartModel hF' hx' ⟶ twoChartModel hF hx is finite (TauCeti.AlgebraicGeometry.twoChartModel.isFinite_map), and the local rings of twoChartModel hF' hx' are valuation rings, hence integrally closed. So twoChartModel hF' hx' is the normalization of twoChartModel hF hx in its function field F', along the generic point Spec k(X') ⟶ X' ⟶ X, where X = twoChartModel hF hx and X' = twoChartModel hF' hx'.

Through normalizationIso, Mathlib's universal property of relative normalization (AlgebraicGeometry.Scheme.Hom.normalizationDesc and AlgebraicGeometry.Scheme.Hom.normalization.hom_ext) applies to the two-chart model: if the generic point of X' factors through an integral morphism T ⟶ X, then X' ⟶ X factors uniquely through T compatibly with it.

Main definitions

• TauCeti.AlgebraicGeometry.twoChartModel.normalizationIso: the isomorphism over X from the normalization of X in the function field of X' to X'.

Main results

• TauCeti.AlgebraicGeometry.twoChartModel.normalizationIso_hom_map: normalizationIso lies over X.
• TauCeti.AlgebraicGeometry.twoChartModel.toNormalization_normalizationIso_hom: it is compatible with the generic point of X'.
• TauCeti.AlgebraicGeometry.twoChartModel.normalizationIso_inv_fromNormalization and TauCeti.AlgebraicGeometry.twoChartModel.fromSpecStalk_normalizationIso_inv: the same compatibilities for the inverse.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.2 and Appendix B.
• The Stacks Project, Tag 035H (relative normalization).

noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.normalizationIso {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) : AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h)) ≅ twoChartModel hF' hx'

The two-chart model of F' is the normalization of the two-chart model of F in F'. The morphism from the relative normalization of twoChartModel hF hx in the function field of twoChartModel hF' hx', along the generic point composed with map, to twoChartModel hF' hx' is an isomorphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.normalizationIso_hom_map {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) : CategoryTheory.CategoryStruct.comp (normalizationIso hF hF' hx hx' h hxt).hom (map hF hF' hx hx' h) = AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h))

normalizationIso lies over the two-chart model of F.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.normalizationIso_hom_map_assoc {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) {Z : AlgebraicGeometry.Scheme} (h✝ : twoChartModel hF hx ⟶ Z) : CategoryTheory.CategoryStruct.comp (normalizationIso hF hF' hx hx' h hxt).hom (CategoryTheory.CategoryStruct.comp (map hF hF' hx hx' h) h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h))) h✝

normalizationIso lies over the two-chart model of F.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.toNormalization_normalizationIso_hom {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h))) (normalizationIso hF hF' hx hx' h hxt).hom = (twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))

normalizationIso carries the canonical morphism into the relative normalization to the generic point of the two-chart model of F'.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.toNormalization_normalizationIso_hom_assoc {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) {Z : AlgebraicGeometry.Scheme} (h✝ : twoChartModel hF' hx' ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h))) (CategoryTheory.CategoryStruct.comp (normalizationIso hF hF' hx hx' h hxt).hom h✝) = CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) h✝

normalizationIso carries the canonical morphism into the relative normalization to the generic point of the two-chart model of F'.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.normalizationIso_inv_fromNormalization {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) : CategoryTheory.CategoryStruct.comp (normalizationIso hF hF' hx hx' h hxt).inv (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h))) = map hF hF' hx hx' h

The inverse of normalizationIso lies over the two-chart model of F.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.normalizationIso_inv_fromNormalization_assoc {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) {Z : AlgebraicGeometry.Scheme} (h✝ : twoChartModel hF hx ⟶ Z) : CategoryTheory.CategoryStruct.comp (normalizationIso hF hF' hx hx' h hxt).inv (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h))) h✝) = CategoryTheory.CategoryStruct.comp (map hF hF' hx hx' h) h✝

The inverse of normalizationIso lies over the two-chart model of F.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.fromSpecStalk_normalizationIso_inv {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) : CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (normalizationIso hF hF' hx hx' h hxt).inv = AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h))

The inverse of normalizationIso carries the generic point of the two-chart model of F' to the canonical morphism into the relative normalization.

@[simp]

theorem TauCeti.AlgebraicGeometry.twoChartModel.fromSpecStalk_normalizationIso_inv_assoc {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (h : (algebraMap F F') x = x') (hxt : Transcendental k x) {Z : AlgebraicGeometry.Scheme} (h✝ : AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (CategoryTheory.CategoryStruct.comp (normalizationIso hF hF' hx hx' h hxt).inv h✝) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp ((twoChartModel hF' hx').fromSpecStalk (genericPoint ↥(twoChartModel hF' hx'))) (map hF hF' hx hx' h))) h✝

The inverse of normalizationIso carries the generic point of the two-chart model of F' to the canonical morphism into the relative normalization.