NYLL
Module

Pic0_forall_isPrincipal_of_ringEquiv.lean

Nyll.JacobianVarieties.Pic0.Pic0_forall_isPrincipal_of_ringEquiv
16 declarations indexed from sourceView source ↗

Module documentation

Transport of principal degree-zero divisors

A field ring equivalence respecting the constant field transports places, orders, and residue degrees. These comparisons carry a principal representative of a transported divisor back to the original divisor.

Imports1
Imported by1

Declarations

def

comapSymmRingEquiv

L42 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.comapSymmRingEquiv
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
Lean source · full declaration
def comapSymmRingEquiv (V : ValuationSubring F) :
    V ≃+* (V.comap (e.symm : F' →+* F)) where
  toFun x := ⟨e x, by
    rw [ValuationSubring.mem_comap]
    change e.symm (e x) ∈ V
    rw [e.symm_apply_apply]
    exact x.2⟩
  invFun y := ⟨e.symm y, y.2⟩
  left_inv x := by
    ext
    exact e.symm_apply_apply x
  right_inv y := by
    ext
    exact e.apply_symm_apply y
  map_mul' x y := by
    ext
    exact e.map_mul x y
  map_add' x y := by
    ext
    exact e.map_add x y
theorem

coe_comapSymmRingEquiv_apply

L64 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
Lean source · statement
theorem coe_comapSymmRingEquiv_apply (V : ValuationSubring F) (x : V) :
    ((comapSymmRingEquiv e V x : (V.comap (e.symm : F' →+* F))) : F') = e x
theorem

symm_algebraMap_comm

L70 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.symm_algebraMap_comm
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he
Lean source · statement
theorem symm_algebraMap_comm (a : K) : e.symm (algebraMap K F' a) = algebraMap K F a
def

congrRingEquiv

L73 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.congrRingEquiv
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he
Lean source · full declaration
def congrRingEquiv (v : Place K F) : Place K F' where
  toValuationSubring := v.toValuationSubring.comap (e.symm : F' →+* F)
  algebraMap_mem' a := by
    rw [ValuationSubring.mem_comap]
    change e.symm (algebraMap K F' a) ∈ v.toValuationSubring
    rw [symm_algebraMap_comm e he a]
    exact v.algebraMap_mem' a
  ne_top' := fun h =>
    v.ne_top' (SetLike.ext fun x =>
      ⟨fun _ => ValuationSubring.mem_top x, fun _ => by
        have hx : e x ∈ v.toValuationSubring.comap (e.symm : F' →+* F) := by
          rw [h]
          exact ValuationSubring.mem_top _
        rw [ValuationSubring.mem_comap] at hx
        have : e.symm (e x) ∈ v.toValuationSubring := hx
        rwa [e.symm_apply_apply] at this⟩)
  isPrincipalIdealRing' :=
    IsPrincipalIdealRing.of_surjective
      (comapSymmRingEquiv e v.toValuationSubring : _ ≃+* _)
      (comapSymmRingEquiv e v.toValuationSubring).surjective
theorem

congrRingEquiv_toValuationSubring

L95 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.congrRingEquiv_toValuationSubring
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he
Lean source · statement
theorem congrRingEquiv_toValuationSubring (v : Place K F) :
    (congrRingEquiv e he v).toValuationSubring
      = v.toValuationSubring.comap (e.symm : F' →+* F)
theorem

ord_congrRingEquiv

L99 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.ord_congrRingEquiv
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he
Lean source · statement
theorem ord_congrRingEquiv (v : Place K F) (f : F) :
    (congrRingEquiv e he v).ord (e f) = v.ord f
def

congrResidueAlgEquiv

L119 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.congrResidueAlgEquiv
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he
Lean source · statement
def congrResidueAlgEquiv (v : Place K F) :
    v.ResidueField ≃ₐ[K] (congrRingEquiv e he v).ResidueField
theorem

deg_congrRingEquiv

L135 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.deg_congrRingEquiv
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he
Lean source · statement
theorem deg_congrRingEquiv (v : Place K F) : (congrRingEquiv e he v).deg = v.deg
def

congrEquiv

L138 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.congrEquiv
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he
Lean source · full declaration
def congrEquiv : Place K F ≃ Place K F' where
  toFun := congrRingEquiv e he
  invFun := congrRingEquiv e.symm (symm_algebraMap_comm e he)
  left_inv v := by
    ext1
    refine SetLike.ext fun x => ?_
    change e.symm (e.symm.symm x) ∈ v.toValuationSubring ↔ x ∈ v.toValuationSubring
    rw [RingEquiv.symm_symm, e.symm_apply_apply]
  right_inv v := by
    ext1
    refine SetLike.ext fun x => ?_
    change e.symm.symm (e.symm x) ∈ v.toValuationSubring ↔ x ∈ v.toValuationSubring
    rw [RingEquiv.symm_symm, e.apply_symm_apply]
theorem

congrEquiv_apply

L153 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.congrEquiv_apply
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he
Lean source · statement
theorem congrEquiv_apply (v : Place K F) : congrEquiv e he v = congrRingEquiv e he v
theorem

congrEquiv_symm_apply

L156 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Place.congrEquiv_symm_apply
Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
section Congr
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F')
variable (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include he
Lean source · statement
theorem congrEquiv_symm_apply (v : Place K F') :
    (congrEquiv e he).symm v = congrRingEquiv e.symm (symm_algebraMap_comm e he) v
theorem

subsingleton_iff

L169 ↗
AlgebraicCurve.Pic0.subsingleton_iff
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
section SubsingletonCriterion
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
namespace Pic0
open scoped _root_.AlgebraicCurve.Pic0 in
Lean source · statement
theorem _root_.AlgebraicCurve.Pic0.subsingleton_iff :
    Subsingleton (Pic0 K F) ↔
      Divisor.degZero (K := K) (F := F) ≤ Divisor.principal (K := K) (F := F)
theorem

subsingleton_of_forall_isPrincipal

L177 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Pic0.subsingleton_of_forall_isPrincipal
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
section SubsingletonCriterion
variable (K F : Type*) [Field K] [Field F] [Algebra K F]
open _root_.AlgebraicCurve
open scoped _root_.AlgebraicCurve.Pic0 in
Lean source · statement
theorem Pic0.subsingleton_of_forall_isPrincipal
    (h : ∀ D : Divisor K F, Divisor.degree D = 0 → D.IsPrincipal) :
    Subsingleton (Pic0 K F)
theorem

forall_isPrincipal_of_ringEquiv

L191 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Pic0.forall_isPrincipal_of_ringEquiv
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Pic0
open _root_.AlgebraicCurve.Pic0
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F') (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include e he
Lean source · statement
theorem forall_isPrincipal_of_ringEquiv
    (h : ∀ D : Divisor K F, Divisor.degree D = 0 → D.IsPrincipal)
    (D' : Divisor K F') (hD' : Divisor.degree D' = 0) : D'.IsPrincipal
theorem

subsingleton_of_ringEquiv

L222 ↗
JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Pic0.subsingleton_of_ringEquiv
Source context 11 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Pic0
open _root_.AlgebraicCurve.Pic0
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (e : F ≃+* F') (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
include e he
Lean source · statement
theorem subsingleton_of_ringEquiv (h : Subsingleton (Pic0 K F)) :
    Subsingleton (Pic0 K F')
theorem

forall_isPrincipal_of_ringEquiv

L237 ↗
AlgebraicCurve.Pic0.forall_isPrincipal_of_ringEquiv
Source context 5 commands

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

section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.PrincipalTransport
open IsDedekindDomain WithZero IsLocalRing
open _root_.AlgebraicCurve in
open JacobianVarieties.Pic0.Proofs.PrincipalTransport.AlgebraicCurve.Pic0 renaming
  forall_isPrincipal_of_ringEquiv → transportPrincipal in
Lean source · statement
theorem _root_.AlgebraicCurve.Pic0.forall_isPrincipal_of_ringEquiv {K F F' : Type*} [Field K]
    [Field F] [Field F'] [Algebra K F] [Algebra K F']
    (e : F ≃+* F') (he : ∀ a : K, e (algebraMap K F a) = algebraMap K F' a)
    (h : ∀ D : Divisor K F, Divisor.degree D = 0 → D.IsPrincipal)
    (D' : Divisor K F') (hD' : Divisor.degree D' = 0) :
    D'.IsPrincipal

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