Documentation

TauCeti.AlgebraicGeometry.Curves.TwoChartModel.AlgHom

Morphisms of two-chart models are embeddings of function fields #

Let F / k and F' / k be algebraic function fields, and x ∈ F, x' ∈ F' transcendental over k. The two-chart models X = twoChartModel hF hx and X' = twoChartModel hF' hx' are regular proper curves over k with function fields F and F'. This file proves that the dominant k-morphisms X' ⟶ X are exactly the k-embeddings F → F', with no compatibility between x and x' required.

Every k-embedding φ : F →ₐ[k] F' gives a k-morphism Spec F' ⟶ X from the generic point of X', through the generic point of X. The local rings of X' are valuation rings (TauCeti.AlgebraicGeometry.twoChartModel.valuationRing_stalk) and X is proper over k, so this morphism extends uniquely to a k-morphism homOfAlgHom φ : X' ⟶ X (AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom). Its pullback of rational functions is φ, and since X is separated, a dominant k-morphism is determined by its pullback of rational functions: the construction is a bijection, and it is functorial. In particular a k-isomorphism F ≃ F' gives an isomorphism of the models, so the two-chart model does not depend on the choice of the transcendental function: twoChartModel hF hx ≅ twoChartModel hF hy for any two transcendental x, y ∈ F. When the embedding carries x to x', the morphism is the one glued from the chart maps (TauCeti.AlgebraicGeometry.twoChartModel.map).

This is the morphism half of the anti-equivalence between function fields of one variable and regular projective curves.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.homOfAlgHom {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) (hxt : Transcendental k x) (hx't : Transcendental k x') (φ : F →ₐ[k] F') :
twoChartModel hF' hx' ⟶ twoChartModel hF hx

The morphism of two-chart models induced by a k-embedding φ : F →ₐ[k] F' of function fields, for transcendental x ∈ F and x' ∈ F': the unique dominant k-morphism twoChartModel hF' hx' ⟶ twoChartModel hF hx whose pullback of rational functions is φ (eq_homOfAlgHom_iff). No relation between x and x' is required.

Instances For
    source
    instance TauCeti.AlgebraicGeometry.twoChartModel.instIsOverHomOfAlgHomSpecOf {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} (φ : F →ₐ[k] F') :
    AlgebraicGeometry.Scheme.Hom.IsOver (homOfAlgHom hF hF' hx hx' hxt hx't φ) (AlgebraicGeometry.Spec ↧k)

    homOfAlgHom φ is a morphism over k.

    source
    instance TauCeti.AlgebraicGeometry.twoChartModel.instIsDominantHomOfAlgHom {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} (φ : F →ₐ[k] F') :
    AlgebraicGeometry.IsDominant (homOfAlgHom hF hF' hx hx' hxt hx't φ)

    homOfAlgHom φ is dominant: it sends the generic point to the generic point.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.twoChartModel.functionFieldEquiv_functionFieldMap_homOfAlgHom {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} (φ : F →ₐ[k] F') (z : F) :
    (functionFieldEquiv hx't) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.functionFieldMap (homOfAlgHom hF hF' hx hx' hxt hx't φ))) ((functionFieldEquiv hxt).symm z)) = φ z

    The pullback of rational functions along homOfAlgHom φ is φ: under the identifications k(X) ≃ F and k(X') ≃ F' of the function fields of the two models, the pullback along homOfAlgHom φ : X' ⟶ X is φ.

    source
    theorem TauCeti.AlgebraicGeometry.twoChartModel.eq_homOfAlgHom_iff {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} (φ : F →ₐ[k] F') (f : twoChartModel hF' hx' ⟶ twoChartModel hF hx) [AlgebraicGeometry.Scheme.Hom.IsOver f (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsDominant f] :
    f = homOfAlgHom hF hF' hx hx' hxt hx't φ ↔ ∀ (z : F), (functionFieldEquiv hx't) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.functionFieldMap f)) ((functionFieldEquiv hxt).symm z)) = φ z

    A dominant morphism of two-chart models is determined by its pullback of rational functions: a dominant k-morphism f : X' ⟶ X is homOfAlgHom φ exactly when, under the identifications k(X) ≃ F and k(X') ≃ F', its pullback of rational functions is φ.

    Functoriality #

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.twoChartModel.homOfAlgHom_id {k F : Type u} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {x : F} (hx : x ≠ 0) {hxt : Transcendental k x} :
    homOfAlgHom hF hF hx hx hxt hxt (AlgHom.id k F) = CategoryTheory.CategoryStruct.id (twoChartModel hF hx)

    The identity of F induces the identity of twoChartModel hF hx.

    source
    theorem TauCeti.AlgebraicGeometry.twoChartModel.homOfAlgHom_comp {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} (φ : F →ₐ[k] F') {F'' : Type u} [Field F''] [Algebra k F''] (hF'' : IsFunctionField k F'') {x'' : F''} (hx'' : x'' ≠ 0) {hx''t : Transcendental k x''} (φ' : F' →ₐ[k] F'') :
    CategoryTheory.CategoryStruct.comp (homOfAlgHom hF' hF'' hx' hx'' hx't hx''t φ') (homOfAlgHom hF hF' hx hx' hxt hx't φ) = homOfAlgHom hF hF'' hx hx'' hxt hx''t (φ'.comp φ)

    k-embeddings F → F' → F'' induce the composite of the morphisms of two-chart models.

    source
    theorem TauCeti.AlgebraicGeometry.twoChartModel.homOfAlgHom_comp_assoc {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} (φ : F →ₐ[k] F') {F'' : Type u} [Field F''] [Algebra k F''] (hF'' : IsFunctionField k F'') {x'' : F''} (hx'' : x'' ≠ 0) {hx''t : Transcendental k x''} (φ' : F' →ₐ[k] F'') {Z : AlgebraicGeometry.Scheme} (h : twoChartModel hF hx ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (homOfAlgHom hF' hF'' hx' hx'' hx't hx''t φ') (CategoryTheory.CategoryStruct.comp (homOfAlgHom hF hF' hx hx' hxt hx't φ) h) = CategoryTheory.CategoryStruct.comp (homOfAlgHom hF hF'' hx hx'' hxt hx''t (φ'.comp φ)) h

    k-embeddings F → F' → F'' induce the composite of the morphisms of two-chart models.

    source
    noncomputable def TauCeti.AlgebraicGeometry.twoChartModel.isoOfAlgEquiv {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} (e : F ≃ₐ[k] F') :
    twoChartModel hF' hx' ≅ twoChartModel hF hx

    The isomorphism of two-chart models induced by a k-isomorphism e : F ≃ₐ[k] F' of function fields, for transcendental x ∈ F and x' ∈ F'. For F' = F and e the identity, this says that the two-chart model does not depend on the choice of the transcendental function.

    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.twoChartModel.isoOfAlgEquiv_hom {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} (e : F ≃ₐ[k] F') :
      (isoOfAlgEquiv hF hF' hx hx' e).hom = homOfAlgHom hF hF' hx hx' hxt hx't ↑e

      The forward morphism of isoOfAlgEquiv e is the morphism induced by e.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.twoChartModel.isoOfAlgEquiv_inv {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} (e : F ≃ₐ[k] F') :
      (isoOfAlgEquiv hF hF' hx hx' e).inv = homOfAlgHom hF' hF hx' hx hx't hxt ↑e.symm

      The inverse morphism of isoOfAlgEquiv e is the morphism induced by e.symm.

      Comparison with the morphism glued from the chart maps #

      source
      theorem TauCeti.AlgebraicGeometry.twoChartModel.map_eq_homOfAlgHom {k F F' : Type u} [Field k] [Field F] [Field F'] [Algebra k F] [Algebra k F'] (hF : IsFunctionField k F) (hF' : IsFunctionField k F') {x : F} (hx : x ≠ 0) {x' : F'} (hx' : x' ≠ 0) {hxt : Transcendental k x} {hx't : Transcendental k x'} [Algebra F F'] [IsScalarTower k F F'] [Algebra.IsIntegral F F'] (h : (algebraMap F F') x = x') :
      map hF hF' hx hx' h = homOfAlgHom hF hF' hx hx' hxt hx't (IsScalarTower.toAlgHom k F F')

      The morphism glued from the chart maps is homOfAlgHom of the algebra map: for an integral extension F' / F carrying x to x', the morphism map of two-chart models is the morphism induced by the k-embedding F → F'.