NYLL
Module

Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.lean

Nyll.AlgebraicCurves.Places.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
21 declarations indexed from sourceView source ↗

Module documentation

Exists placeEquiv ord eq and ell mapDomain eq

A base-field algebra equivalence transports places, preserves orders and residue degrees, and identifies the corresponding Riemann spaces.

Imports2
Imported by2

Declarations

abbrev

vsMap

L43 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.vsMap
Documentation

The valuation subring transported by comap along the inverse algebra equivalence.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
abbrev vsMap (σ : F ≃ₐ[K] F') (A : ValuationSubring F) : ValuationSubring F'
theorem

mem_vsMap_iff

L46 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.mem_vsMap_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem mem_vsMap_iff (σ : F ≃ₐ[K] F') (A : ValuationSubring F) (y : F') :
    y ∈ vsMap σ A ↔ σ.symm y ∈ A
def

vsEquiv

L52 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.vsEquiv
Documentation

The ring equivalence from the original valuation subring to its transported valuation subring.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · full declaration
def vsEquiv (σ : F ≃ₐ[K] F') (A : ValuationSubring F) : A ≃+* vsMap σ A where
  toFun x := ⟨σ x, by rw [mem_vsMap_iff, AlgEquiv.symm_apply_apply]; exact x.2⟩
  invFun y := ⟨σ.symm y, y.2⟩
  left_inv x := by ext; simp
  right_inv y := by ext; simp
  map_mul' x y := by ext; simp
  map_add' x y := by ext; simp
theorem

coe_vsEquiv_apply

L60 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.coe_vsEquiv_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem coe_vsEquiv_apply (σ : F ≃ₐ[K] F') (A : ValuationSubring F) (x : A) :
    ((vsEquiv σ A x : vsMap σ A) : F') = σ x
def

placeMap

L65 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.placeMap
Documentation

The place transported along the compatible base-field algebra equivalence.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · full declaration
def placeMap (σ : F ≃ₐ[K] F') (v : Place K F) : Place K F' where
  toValuationSubring := vsMap σ v.toValuationSubring
  algebraMap_mem' a := by
    rw [mem_vsMap_iff, AlgEquiv.commutes]
    exact v.algebraMap_mem' a
  ne_top' h := v.ne_top' <| by
    refine SetLike.ext fun x => ⟨fun _ => ValuationSubring.mem_top x, fun _ => ?_⟩
    have hx : σ x ∈ vsMap σ v.toValuationSubring := h ▸ ValuationSubring.mem_top (σ x)
    rwa [mem_vsMap_iff, AlgEquiv.symm_apply_apply] at hx
  isPrincipalIdealRing' :=
    IsPrincipalIdealRing.of_surjective (vsEquiv σ v.toValuationSubring : _ ≃+* _)
      (vsEquiv σ v.toValuationSubring).surjective
theorem

placeMap_toValuationSubring

L78 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.placeMap_toValuationSubring
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem placeMap_toValuationSubring (σ : F ≃ₐ[K] F') (v : Place K F) :
    (placeMap σ v).toValuationSubring = vsMap σ v.toValuationSubring
theorem

mem_placeMap_iff

L81 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.mem_placeMap_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem mem_placeMap_iff (σ : F ≃ₐ[K] F') (v : Place K F) (y : F') :
    y ∈ (placeMap σ v).toValuationSubring ↔ σ.symm y ∈ v.toValuationSubring
theorem

placeMap_symm_placeMap

L84 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.placeMap_symm_placeMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem placeMap_symm_placeMap (σ : F ≃ₐ[K] F') (v : Place K F) : placeMap σ.symm
  (placeMap σ v) = v
def

placeEquiv

L91 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.placeEquiv
Documentation

The equivalence between place sets induced by the base-field algebra equivalence.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · full declaration
def placeEquiv (σ : F ≃ₐ[K] F') : Place K F ≃ Place K F' where
  toFun := placeMap σ
  invFun := placeMap σ.symm
  left_inv v := placeMap_symm_placeMap σ v
  right_inv w := by simpa using placeMap_symm_placeMap σ.symm w
theorem

placeEquiv_apply

L97 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.placeEquiv_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem placeEquiv_apply (σ : F ≃ₐ[K] F') (v : Place K F) : placeEquiv σ v =
  placeMap σ v
theorem

placeEquiv_symm_apply

L99 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.placeEquiv_symm_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem placeEquiv_symm_apply (σ : F ≃ₐ[K] F') (w : Place K F') :
    (placeEquiv σ).symm w = placeMap σ.symm w
theorem

coe_placeMap

L102 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.coe_placeMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem coe_placeMap (σ : F ≃ₐ[K] F') (v : Place K F) :
    ((placeMap σ v).toValuationSubring : Set F') = σ '' (v.toValuationSubring : Set F)
theorem

ord_placeMap

L111 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.ord_placeMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem ord_placeMap (σ : F ≃ₐ[K] F') (v : Place K F) (f : F) : (placeMap σ v).ord (σ f) =
  v.ord f
def

residueAlgEquiv

L134 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.residueAlgEquiv
Documentation

The induced base-field algebra equivalence between the two residue fields.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
def residueAlgEquiv (σ : F ≃ₐ[K] F') (v : Place K F) : v.ResidueField ≃ₐ[K]
  (placeMap σ v).ResidueField
theorem

deg_placeMap

L158 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.deg_placeMap
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem deg_placeMap (σ : F ≃ₐ[K] F') (v : Place K F) : (placeMap σ v).deg = v.deg
theorem

mapDomain_placeEquiv_apply

L161 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.mapDomain_placeEquiv_apply
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem mapDomain_placeEquiv_apply (σ : F ≃ₐ[K] F') (D : Divisor K F) (w : Place K F') :
    (Finsupp.mapDomain (placeEquiv σ) D) w = D ((placeEquiv σ).symm w)
def

lSpaceEquiv

L167 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.lSpaceEquiv
Documentation

The linear equivalence of Riemann spaces induced by transport of the divisor and function.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · full declaration
def lSpaceEquiv (σ : F ≃ₐ[K] F') (D : Divisor K F) :
    LSpace D ≃ₗ[K] LSpace (Finsupp.mapDomain (placeEquiv σ) D) where
  toFun f := ⟨σ f, by
    rw [mem_riemannRochSpace_iff]
    intro w
    rcases eq_or_ne (f : F) 0 with h0 | h0
    · left; rw [h0, map_zero]
    right
    have hf := (mem_riemannRochSpace_iff.mp f.2) ((placeEquiv σ).symm w)
    rw [mapDomain_placeEquiv_apply]
    have hw : w = placeMap σ ((placeEquiv σ).symm w) := by
      rw [← placeEquiv_apply, Equiv.apply_symm_apply]
    rw [hw, ord_placeMap, ← hw]
    exact hf.resolve_left h0⟩
  invFun g := ⟨σ.symm g, by
    rw [mem_riemannRochSpace_iff]
    intro v
    rcases eq_or_ne (g : F') 0 with h0 | h0
    · left; rw [h0, map_zero]
    right
    have hg := (mem_riemannRochSpace_iff.mp g.2) (placeEquiv σ v)
    rw [mapDomain_placeEquiv_apply, Equiv.symm_apply_apply] at hg
    have h1 : (placeEquiv σ v).ord (g : F') = v.ord (σ.symm g) := by
      conv_lhs => rw [← σ.apply_symm_apply (g : F')]
      exact ord_placeMap σ v _
    rw [← h1]
    exact hg.resolve_left h0⟩
  left_inv f := by ext; simp
  right_inv g := by ext; simp
  map_add' f g := by ext; simp
  map_smul' c f := by ext; simp
theorem

ell_mapDomain

L199 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.ell_mapDomain
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem ell_mapDomain (σ : F ≃ₐ[K] F') (D : Divisor K F) : ell (Finsupp.mapDomain
  (placeEquiv σ) D) = ell D
theorem

degree_mapDomain

L203 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.degree_mapDomain
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem degree_mapDomain (σ : F ≃ₐ[K] F') (D : Divisor K F) :
    Divisor.degree (Finsupp.mapDomain (placeEquiv σ) D) = Divisor.degree D
theorem

isPrincipal_mapDomain_iff

L212 ↗
AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq.AlgebraicCurve.PlaceTransportGlue.isPrincipal_mapDomain_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace PlaceTransportGlue
open _root_.AlgebraicCurve
variable {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
  [Algebra K F']
Lean source · statement
theorem isPrincipal_mapDomain_iff (σ : F ≃ₐ[K] F') (D : Divisor K F) :
    Divisor.IsPrincipal (Finsupp.mapDomain (placeEquiv σ) D) ↔ Divisor.IsPrincipal D
theorem

exists_placeEquiv_ord_eq_and_ell_mapDomain_eq

L233 ↗
AlgebraicCurve.exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
universe u v w
noncomputable section
open _root_.AlgebraicCurve
open AlgebraicCurve.PlaceTransportGlue in
Lean source · statement
theorem _root_.AlgebraicCurve.exists_placeEquiv_ord_eq_and_ell_mapDomain_eq
    {K : Type u} [Field K] {F : Type v} [Field F] [Algebra K F] {F' : Type w} [Field F']
      [Algebra K F']
    (σ : F ≃ₐ[K] F') :
    ∃ π : Place K F ≃ Place K F',
      (∀ v : Place K F, ((π v).toValuationSubring : Set F') = σ '' (v.toValuationSubring : Set F)) ∧
      (∀ (v : Place K F) (f : F), (π v).ord (σ f) = v.ord f) ∧
      (∀ v : Place K F, (π v).deg = v.deg) ∧
      (∀ D : Divisor K F, ell (Finsupp.mapDomain π D) = ell D) ∧
      (∀ D : Divisor K F, Divisor.degree (Finsupp.mapDomain π D) = Divisor.degree D) ∧
      (∀ D : Divisor K F, Divisor.IsPrincipal (Finsupp.mapDomain π D) ↔ Divisor.IsPrincipal D)

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