NYLL
Module

Pic0Congr.lean

Nyll.AlgebraicCurves.Divisors.Pic0Congr
15 declarations indexed from sourceView source ↗

Module documentation

Pic0 Congr

Imports1
Imported by4

Declarations

def

congr

L31 ↗
AlgebraicCurve.Divisor.congr
Documentation

The additive equivalence of divisor groups induced by the equivalence of places.

Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
def congr : Divisor K F ≃+ Divisor K F'
theorem

congr_single

L34 ↗
AlgebraicCurve.Divisor.congr_single
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
theorem congr_single (v : Place K F) (n : ℤ) :
    congr e he (Finsupp.single v n) = Finsupp.single (Place.congrRingEquiv e he v) n
theorem

congr_apply_place_congr

L38 ↗
AlgebraicCurve.Divisor.congr_apply_place_congr
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
theorem congr_apply_place_congr (D : Divisor K F) (v : Place K F) :
    congr e he D (Place.congrRingEquiv e he v) = D v
theorem

congr_symm_apply_place

L44 ↗
AlgebraicCurve.Divisor.congr_symm_apply_place
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
theorem congr_symm_apply_place (D : Divisor K F') (v : Place K F) :
    (congr e he).symm D v = D (Place.congrRingEquiv e he v)
theorem

degree_congr

L50 ↗
AlgebraicCurve.Divisor.degree_congr
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
theorem degree_congr (D : Divisor K F) : degree (congr e he D) = degree D
theorem

degree_congr_symm

L57 ↗
AlgebraicCurve.Divisor.degree_congr_symm
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
theorem degree_congr_symm (D : Divisor K F') : degree ((congr e he).symm D) = degree D
theorem

congr_mem_degZero

L61 ↗
AlgebraicCurve.Divisor.congr_mem_degZero
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
theorem congr_mem_degZero {D : Divisor K F}
    (hD : D ∈ degZero (K := K) (F := F)) : congr e he D ∈ degZero (K := K) (F := F')
theorem

congr_symm_mem_degZero

L65 ↗
AlgebraicCurve.Divisor.congr_symm_mem_degZero
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
theorem congr_symm_mem_degZero {D : Divisor K F'}
    (hD : D ∈ degZero (K := K) (F := F')) :
    (congr e he).symm D ∈ degZero (K := K) (F := F)
theorem

congr_mem_principal

L70 ↗
AlgebraicCurve.Divisor.congr_mem_principal
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
theorem congr_mem_principal {D : Divisor K F}
    (hD : D ∈ principal (K := K) (F := F)) :
    congr e he D ∈ principal (K := K) (F := F')
theorem

congr_symm_mem_principal

L80 ↗
AlgebraicCurve.Divisor.congr_symm_mem_principal
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace Divisor
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)
Lean source · statement
theorem congr_symm_mem_principal {D : Divisor K F'}
    (hD : D ∈ principal (K := K) (F := F')) :
    (congr e he).symm D ∈ principal (K := K) (F := F)
def

degZeroCongr

L97 ↗
AlgebraicCurve.Pic0.degZeroCongr
Documentation

The induced additive equivalence of the subgroups of degree-zero divisors.

Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace 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)
Lean source · full declaration
def degZeroCongr :
    Divisor.degZero (K := K) (F := F) ≃+ Divisor.degZero (K := K) (F := F') where
  toFun D := ⟨Divisor.congr e he D, Divisor.congr_mem_degZero e he D.2⟩
  invFun D := ⟨(Divisor.congr e he).symm D, Divisor.congr_symm_mem_degZero e he D.2⟩
  left_inv D := Subtype.ext ((Divisor.congr e he).symm_apply_apply D)
  right_inv D := Subtype.ext ((Divisor.congr e he).apply_symm_apply D)
  map_add' D E := Subtype.ext (map_add (Divisor.congr e he) (D : Divisor K F) (E : Divisor K F))
theorem

coe_degZeroCongr

L105 ↗
AlgebraicCurve.Pic0.coe_degZeroCongr
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace 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)
Lean source · statement
theorem coe_degZeroCongr (D : Divisor.degZero (K := K) (F := F)) :
    (degZeroCongr e he D : Divisor K F') = Divisor.congr e he (D : Divisor K F)
theorem

coe_degZeroCongr_symm

L108 ↗
AlgebraicCurve.Pic0.coe_degZeroCongr_symm
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace 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)
Lean source · statement
theorem coe_degZeroCongr_symm (D : Divisor.degZero (K := K) (F := F')) :
    ((degZeroCongr e he).symm D : Divisor K F)
      = (Divisor.congr e he).symm (D : Divisor K F')
theorem

map_principal_degZeroCongr

L112 ↗
AlgebraicCurve.Pic0.map_principal_degZeroCongr
Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace 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)
Lean source · statement
theorem map_principal_degZeroCongr :
    ((Divisor.principal (K := K) (F := F)).addSubgroupOf
        (Divisor.degZero (K := K) (F := F))).map (degZeroCongr e he).toAddMonoidHom
      = (Divisor.principal (K := K) (F := F')).addSubgroupOf
          (Divisor.degZero (K := K) (F := F'))
def

congr

L128 ↗
AlgebraicCurve.Pic0.congr
Documentation

The additive equivalence of degree-zero divisor class groups induced by field transport.

Source context 6 commands

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

noncomputable section
open AlgebraicCurve
namespace AlgebraicCurve
namespace 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)
Lean source · statement
def congr : Pic0 K F ≃+ Pic0 K F'

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