NYLL
Module

Transport.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.Transport
19 declarations indexed from sourceView source ↗

Module documentation

Transport of prime divisors across function-field equivalences

A K-algebra equivalence of function fields transports valuation subrings, discrete K-valuations, residue fields, and hence Fried--Jarden prime divisors. This is the model-independent bridge needed to replace a plane equation by an isomorphic monic representative.

Imports1
Imported by2

Declarations

def

mapEquiv

L34 ↗
FieldArithmetic.Chapter06.ValuationSubring.mapEquiv
Documentation

The image of a valuation subring under a field isomorphism.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace ValuationSubring
Lean source · full declaration
def mapEquiv (e : F ≃+* G) (V : ValuationSubring F) :
    ValuationSubring G where
  toSubring := V.toSubring.map e.toRingHom
  mem_or_inv_mem' x := by
    rcases V.mem_or_inv_mem (e.symm x) with hx | hx
    · left
      exact Subring.mem_map_equiv.mpr hx
    · right
      change x⁻¹ ∈ V.toSubring.map e.toRingHom
      apply
        (Subring.mem_map_equiv
          (f := e) (K := V.toSubring) (x := x⁻¹)).mpr
      simpa using hx
theorem

mem_mapEquiv_iff

L49 ↗
FieldArithmetic.Chapter06.ValuationSubring.mem_mapEquiv_iff
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace ValuationSubring
Lean source · statement
theorem mem_mapEquiv_iff
    (e : F ≃+* G) (V : ValuationSubring F) (x : G) :
    x ∈ mapEquiv e V ↔ e.symm x ∈ V
def

equivMapEquiv

L55 ↗
FieldArithmetic.Chapter06.ValuationSubring.equivMapEquiv
Documentation

The source valuation ring is ring-isomorphic to its transported image.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace ValuationSubring
Lean source · statement
def equivMapEquiv (e : F ≃+* G) (V : ValuationSubring F) :
    V ≃+* mapEquiv e V
theorem

coe_equivMapEquiv

L60 ↗
FieldArithmetic.Chapter06.ValuationSubring.coe_equivMapEquiv
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace ValuationSubring
Lean source · statement
theorem coe_equivMapEquiv
    (e : F ≃+* G) (V : ValuationSubring F) (x : V) :
    ((equivMapEquiv e V x : mapEquiv e V) : G) = e x
theorem

mapEquiv_symm_mapEquiv

L66 ↗
FieldArithmetic.Chapter06.ValuationSubring.mapEquiv_symm_mapEquiv
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace ValuationSubring
Lean source · statement
theorem mapEquiv_symm_mapEquiv
    (e : F ≃+* G) (V : ValuationSubring F) :
    mapEquiv e.symm (mapEquiv e V) = V
theorem

ext

L77 ↗
FieldArithmetic.Chapter06.DiscreteKValuation.ext
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace DiscreteKValuation
Lean source · statement
theorem ext
    {v w : DiscreteKValuation K F}
    (h : v.valuationSubring = w.valuationSubring) :
    v = w
def

map

L87 ↗
FieldArithmetic.Chapter06.DiscreteKValuation.map
Documentation

Transport a discrete K-valuation across a K-field equivalence.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace DiscreteKValuation
Lean source · full declaration
def map (e : F ≃ₐ[K] G) (v : DiscreteKValuation K F) :
    DiscreteKValuation K G where
  valuationSubring := ValuationSubring.mapEquiv e.toRingEquiv v.valuationSubring
  isDiscreteValuationRing := by
    let : IsDiscreteValuationRing v.valuationSubring :=
      v.isDiscreteValuationRing
    exact
      IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing
        (ValuationSubring.equivMapEquiv
          e.toRingEquiv v.valuationSubring)
  algebraMap_mem x := by
    rw [ValuationSubring.mem_mapEquiv_iff]
    simpa using v.algebraMap_mem x
def

valuationSubringAlgEquiv

L102 ↗
FieldArithmetic.Chapter06.DiscreteKValuation.valuationSubringAlgEquiv
Documentation

The valuation rings before and after transport are K-algebra equivalent.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace DiscreteKValuation
Lean source · full declaration
def valuationSubringAlgEquiv
    (e : F ≃ₐ[K] G) (v : DiscreteKValuation K F) :
    v.valuationSubring ≃ₐ[K] (map e v).valuationSubring where
  __ :=
    ValuationSubring.equivMapEquiv e.toRingEquiv v.valuationSubring
  commutes' x := by
    apply Subtype.ext
    exact e.commutes x
def

residueFieldAlgEquiv

L112 ↗
FieldArithmetic.Chapter06.DiscreteKValuation.residueFieldAlgEquiv
Documentation

Transport induces a K-algebra equivalence of residue fields.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace DiscreteKValuation
Lean source · statement
def residueFieldAlgEquiv
    (e : F ≃ₐ[K] G) (v : DiscreteKValuation K F) :
    v.ResidueField ≃ₐ[K] (map e v).ResidueField
theorem

map_symm_map

L119 ↗
FieldArithmetic.Chapter06.DiscreteKValuation.map_symm_map
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace DiscreteKValuation
Lean source · statement
theorem map_symm_map
    (e : F ≃ₐ[K] G) (v : DiscreteKValuation K F) :
    map e.symm (map e v) = v
theorem

ext

L132 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.ext
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace FunctionFieldPrimeDivisor
Lean source · statement
theorem ext
    {v w : FunctionFieldPrimeDivisor K F}
    (h : v.toDiscreteKValuation = w.toDiscreteKValuation) :
    v = w
def

map

L142 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.map
Documentation

Transport a Fried--Jarden prime divisor across a K-field equivalence.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace FunctionFieldPrimeDivisor
Lean source · full declaration
def map (e : F ≃ₐ[K] G) (v : FunctionFieldPrimeDivisor K F) :
    FunctionFieldPrimeDivisor K G where
  toDiscreteKValuation := v.toDiscreteKValuation.map e
  residueFinite := by
    exact
      Module.Finite.of_surjective
        (DiscreteKValuation.residueFieldAlgEquiv
          e v.toDiscreteKValuation).toLinearMap
        (DiscreteKValuation.residueFieldAlgEquiv
          e v.toDiscreteKValuation).surjective
def

valuationSubringAlgEquiv

L154 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.valuationSubringAlgEquiv
Documentation

The valuation-ring equivalence underlying transport of a prime divisor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace FunctionFieldPrimeDivisor
Lean source · statement
def valuationSubringAlgEquiv
    (e : F ≃ₐ[K] G) (v : FunctionFieldPrimeDivisor K F) :
    v.valuationSubring ≃ₐ[K] (map e v).valuationSubring
theorem

degree_map

L160 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.degree_map
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace FunctionFieldPrimeDivisor
Lean source · statement
theorem degree_map
    (e : F ≃ₐ[K] G) (v : FunctionFieldPrimeDivisor K F) :
    (map e v).degree = v.degree
theorem

map_symm_map

L168 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.map_symm_map
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace FunctionFieldPrimeDivisor
Lean source · statement
theorem map_symm_map
    (e : F ≃ₐ[K] G) (v : FunctionFieldPrimeDivisor K F) :
    map e.symm (map e v) = v
def

equivOfAlgEquiv

L175 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.equivOfAlgEquiv
Documentation

Prime divisors are invariant under K-equivalence of function fields.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace FunctionFieldPrimeDivisor
Lean source · full declaration
def equivOfAlgEquiv (e : F ≃ₐ[K] G) :
    FunctionFieldPrimeDivisor K F ≃ FunctionFieldPrimeDivisor K G where
  toFun := map e
  invFun := map e.symm
  left_inv := map_symm_map e
  right_inv v := by
    simpa using map_symm_map e.symm v
theorem

finiteAlong_map

L183 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteAlong_map
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace FunctionFieldPrimeDivisor
Lean source · statement
theorem finiteAlong_map
    {A : Type*} [CommRing A] [Algebra K A]
    (e : F ≃ₐ[K] G) (v : FunctionFieldPrimeDivisor K F)
    (ι : A →ₐ[K] F) (h : v.FiniteAlong ι) :
    (map e v).FiniteAlong (e.toAlgHom.comp ι)
theorem

finiteAlong_map_iff

L195 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.finiteAlong_map_iff
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace FunctionFieldPrimeDivisor
Lean source · statement
theorem finiteAlong_map_iff
    {A : Type*} [CommRing A] [Algebra K A]
    (e : F ≃ₐ[K] G) (v : FunctionFieldPrimeDivisor K F)
    (ι : A →ₐ[K] F) :
    (map e v).FiniteAlong (e.toAlgHom.comp ι) ↔
      v.FiniteAlong ι
theorem

centerAlong_map

L212 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.centerAlong_map
Documentation

Centers are preserved by simultaneous transport of the field and model map.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
open IsLocalRing
universe uK uF uG
variable {K : Type uK} {F : Type uF} {G : Type uG}
  [Field K] [Field F] [Field G]
  [Algebra K F] [Algebra K G]
namespace FunctionFieldPrimeDivisor
Lean source · statement
theorem centerAlong_map
    {A : Type*} [CommRing A] [Algebra K A]
    (e : F ≃ₐ[K] G) (v : FunctionFieldPrimeDivisor K F)
    (ι : A →ₐ[K] F) (h : v.FiniteAlong ι) :
    (map e v).centerAlong (e.toAlgHom.comp ι)
        (finiteAlong_map e v ι h) =
      v.centerAlong ι h

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.