NYLL
Module

Correspondences.lean

Nyll.AlgebraicCurves.Divisors.Correspondences
39 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Transport of field structures, places, divisors, and degree-zero Picard groups along base-field algebra homomorphisms.

Imports2
Imported by146

Declarations

abbrev

algebraAlong

L32 ↗
AlgebraicCurve.algebraAlong
Documentation

The field-algebra structure induced by the given base-field algebra homomorphism.

Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
abbrev algebraAlong (φ : F →ₐ[K] F') : Algebra F F'
theorem

isScalarTower_along

L34 ↗
AlgebraicCurve.isScalarTower_along
Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · full declaration
theorem isScalarTower_along (φ : F →ₐ[K] F') :
    letI := algebraAlong φ; IsScalarTower K F F' :=
  letI := algebraAlong φ
  IsScalarTower.of_algebraMap_eq fun k => (φ.commutes k).symm
theorem

isIntegral_along

L39 ↗
AlgebraicCurve.isIntegral_along
Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · full declaration
theorem isIntegral_along (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) :
    letI := algebraAlong φ; Algebra.IsIntegral F F' :=
  letI := algebraAlong φ
  ⟨hφ⟩
def

FundamentalIdentityAlong

L47 ↗
AlgebraicCurve.FundamentalIdentityAlong
Documentation

The ramification and inertia fundamental identity for the field extension induced by the homomorphism.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (K) in
Lean source · statement
def FundamentalIdentityAlong (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    [HasPrincipalDivisors K F'] : Prop
def

FiniteAlong

L56 ↗
AlgebraicCurve.FiniteAlong
Documentation

The field extension induced by the homomorphism is finite as a module.

Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (K) in
variable (K) in
Lean source · statement
def FiniteAlong (φ : F →ₐ[K] F') : Prop
def

NormFormulaAlong

L63 ↗
AlgebraicCurve.NormFormulaAlong
Documentation

The divisor pushforward norm formula for the finite extension induced by the homomorphism.

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (K) in
variable (K) in
variable (K) in
Lean source · statement
def NormFormulaAlong (φ : F →ₐ[K] F') (hfin : FiniteAlong K φ) : Prop
def

finrankAlong

L71 ↗
AlgebraicCurve.finrankAlong
Documentation

The module finrank of the field extension induced by the homomorphism.

Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable (K) in
variable (K) in
variable (K) in
variable (K) in
Lean source · statement
def finrankAlong (φ : F →ₐ[K] F') : ℕ
def

pullbackAlong

L88 ↗
AlgebraicCurve.Divisor.pullbackAlong
Documentation

Divisor pullback along the integral base-field algebra homomorphism.

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Pullback
variable [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
def pullbackAlong : Divisor K F →+ Divisor K F'
theorem

isPrincipal_pullbackAlong

L94 ↗
AlgebraicCurve.Divisor.isPrincipal_pullbackAlong
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Pullback
variable [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem isPrincipal_pullbackAlong {D : Divisor K F} (hD : D.IsPrincipal) :
    (pullbackAlong φ hφ D).IsPrincipal
theorem

degree_pullbackAlong

L101 ↗
AlgebraicCurve.Divisor.degree_pullbackAlong
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Pullback
variable [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem degree_pullbackAlong (hFI : FundamentalIdentityAlong K φ hφ) (D : Divisor K F) :
    degree (pullbackAlong φ hφ D) = (finrankAlong K φ : ℤ) * degree D
theorem

pullbackAlong_mem_degZero

L109 ↗
AlgebraicCurve.Divisor.pullbackAlong_mem_degZero
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Pullback
variable [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem pullbackAlong_mem_degZero (hFI : FundamentalIdentityAlong K φ hφ) {D : Divisor K F}
    (hD : D ∈ degZero (K := K) (F := F)) :
    pullbackAlong φ hφ D ∈ degZero (K := K) (F := F')
def

pushforwardAlong

L121 ↗
AlgebraicCurve.Divisor.pushforwardAlong
Documentation

Divisor pushforward along the integral base-field algebra homomorphism.

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Pushforward
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
def pushforwardAlong : Divisor K F' →+ Divisor K F
theorem

degree_pushforwardAlong

L127 ↗
AlgebraicCurve.Divisor.degree_pushforwardAlong
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Pushforward
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem degree_pushforwardAlong (D : Divisor K F') :
    degree (pushforwardAlong φ hφ D) = degree D
theorem

pushforwardAlong_mem_degZero

L134 ↗
AlgebraicCurve.Divisor.pushforwardAlong_mem_degZero
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Pushforward
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem pushforwardAlong_mem_degZero {D : Divisor K F'}
    (hD : D ∈ degZero (K := K) (F := F')) :
    pushforwardAlong φ hφ D ∈ degZero (K := K) (F := F)
theorem

isPrincipal_pushforwardAlong

L139 ↗
AlgebraicCurve.Divisor.isPrincipal_pushforwardAlong
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section AlongHom
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
section Pushforward
variable (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
Lean source · statement
theorem isPrincipal_pushforwardAlong (hfin : FiniteAlong K φ)
    (hN : NormFormulaAlong K φ hfin) {D : Divisor K F'} (hD : D.IsPrincipal) :
    (pushforwardAlong φ hφ D).IsPrincipal
def

correspondence

L160 ↗
AlgebraicCurve.Divisor.correspondence
Documentation

The divisor endomorphism obtained by pullback along the first map and pushforward along the second.

Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section Correspondence
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
Lean source · statement
def correspondence : Divisor K F →+ Divisor K F
theorem

correspondence_apply

L163 ↗
AlgebraicCurve.Divisor.correspondence_apply
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section Correspondence
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
Lean source · statement
theorem correspondence_apply (D : Divisor K F) :
    correspondence φ ψ hφ hψ D = pushforwardAlong ψ hψ (pullbackAlong φ hφ D)
theorem

degree_correspondence

L167 ↗
AlgebraicCurve.Divisor.degree_correspondence
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section Correspondence
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
Lean source · statement
theorem degree_correspondence (hFI : FundamentalIdentityAlong K φ hφ) (D : Divisor K F) :
    Divisor.degree (correspondence φ ψ hφ hψ D) = (finrankAlong K φ : ℤ) * Divisor.degree D
theorem

correspondence_mem_degZero

L171 ↗
AlgebraicCurve.Divisor.correspondence_mem_degZero
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section Correspondence
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
Lean source · statement
theorem correspondence_mem_degZero (hFI : FundamentalIdentityAlong K φ hφ) {D : Divisor K F}
    (hD : D ∈ degZero (K := K) (F := F)) :
    correspondence φ ψ hφ hψ D ∈ degZero (K := K) (F := F)
theorem

correspondence_mem_principal

L176 ↗
AlgebraicCurve.Divisor.correspondence_mem_principal
Source context 7 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Divisor
section Correspondence
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
Lean source · statement
theorem correspondence_mem_principal (hfin : FiniteAlong K ψ)
    (hN : NormFormulaAlong K ψ hfin) {D : Divisor K F}
    (hD : D ∈ principal (K := K) (F := F)) :
    correspondence φ ψ hφ hψ D ∈ principal (K := K) (F := F)
def

degZeroCorrespondence

L195 ↗
AlgebraicCurve.Pic0.degZeroCorrespondence
Documentation

The divisor correspondence restricted to degree-zero divisors.

Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Pic0
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
variable (hFI : FundamentalIdentityAlong K φ hφ)
variable (hfin : FiniteAlong K ψ) (hN : NormFormulaAlong K ψ hfin)
Lean source · statement
def degZeroCorrespondence :
    Divisor.degZero (K := K) (F := F) →+ Divisor.degZero (K := K) (F := F)
theorem

coe_degZeroCorrespondence

L201 ↗
AlgebraicCurve.Pic0.coe_degZeroCorrespondence
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Pic0
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
variable (hFI : FundamentalIdentityAlong K φ hφ)
variable (hfin : FiniteAlong K ψ) (hN : NormFormulaAlong K ψ hfin)
Lean source · statement
theorem coe_degZeroCorrespondence (D : Divisor.degZero (K := K) (F := F)) :
    (degZeroCorrespondence φ ψ hφ hψ hFI D : Divisor K F) =
      Divisor.correspondence φ ψ hφ hψ (D : Divisor K F)
def

correspondence

L207 ↗
AlgebraicCurve.Pic0.correspondence
Documentation

The endomorphism induced by the divisor correspondence on the degree-zero Picard group.

Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Pic0
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
variable (hFI : FundamentalIdentityAlong K φ hφ)
variable (hfin : FiniteAlong K ψ) (hN : NormFormulaAlong K ψ hfin)
Lean source · statement
def correspondence : Pic0 K F →+ Pic0 K F
theorem

correspondence_mk

L213 ↗
AlgebraicCurve.Pic0.correspondence_mk
Source context 8 commands

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

noncomputable section
namespace AlgebraicCurve
namespace Pic0
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
variable [HasPrincipalDivisors K F']
variable (φ ψ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral)
variable (hFI : FundamentalIdentityAlong K φ hφ)
variable (hfin : FiniteAlong K ψ) (hN : NormFormulaAlong K ψ hfin)
Lean source · statement
theorem correspondence_mk (D : Divisor.degZero (K := K) (F := F)) :
    correspondence φ ψ hφ hψ hFI hfin hN (mk D) =
      mk (degZeroCorrespondence φ ψ hφ hψ hFI D)
def

restrictAlong

L229 ↗
AlgebraicCurve.Place.restrictAlong
Documentation

Restriction of a place along the integral base-field algebra homomorphism.

Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongPlaces
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
def Place.restrictAlong (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w : Place K F') :
    Place K F
def

ramificationIndexAlong

L238 ↗
AlgebraicCurve.Place.ramificationIndexAlong
Documentation

The ramification index of the place over the field structure induced by the homomorphism.

Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongPlaces
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
def Place.ramificationIndexAlong (φ : F →ₐ[K] F') (w : Place K F') : ℕ
def

inertiaDegAlong

L243 ↗
AlgebraicCurve.Place.inertiaDegAlong
Documentation

The inertia degree of the place over the induced integral field extension.

Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongPlaces
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
def Place.inertiaDegAlong (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (w : Place K F') :
    ℕ
theorem

ord_restrictAlong

L250 ↗
AlgebraicCurve.Place.ord_restrictAlong
Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongPlaces
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem Place.ord_restrictAlong (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w : Place K F') (f : F) :
    w.ord (φ f) = Place.ramificationIndexAlong φ w * (w.restrictAlong φ hφ).ord f
theorem

pullbackAlong_apply

L258 ↗
AlgebraicCurve.Divisor.pullbackAlong_apply
Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongPlaces
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem Divisor.pullbackAlong_apply [HasPrincipalDivisors K F'] (φ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (D : Divisor K F) (w : Place K F') :
    Divisor.pullbackAlong φ hφ D w
      = Place.ramificationIndexAlong φ w * D (w.restrictAlong φ hφ)
theorem

pushforwardAlong_single

L267 ↗
AlgebraicCurve.Divisor.pushforwardAlong_single
Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongPlaces
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem Divisor.pushforwardAlong_single (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (w : Place K F') (n : ℤ) :
    Divisor.pushforwardAlong φ hφ (Finsupp.single w n)
      = Finsupp.single (w.restrictAlong φ hφ) (n * w.inertiaDegAlong φ hφ)
theorem

restrictAlong_congr

L287 ↗
AlgebraicCurve.Place.restrictAlong_congr
Source context 4 commands

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

noncomputable section
namespace AlgebraicCurve
variable {K F F₁ Z : Type*} [Field K] [Field F] [Field F₁] [Field Z]
  [Algebra K F] [Algebra K F₁] [Algebra K Z]
namespace Place
Lean source · statement
theorem restrictAlong_congr {φ φ' : F →ₐ[K] F₁} (h : φ = φ')
    (hφ : φ.toRingHom.IsIntegral) (hφ' : φ'.toRingHom.IsIntegral) (w : Place K F₁) :
    w.restrictAlong φ hφ = w.restrictAlong φ' hφ'
def

fiberAlong

L299 ↗
AlgebraicCurve.Place.fiberAlong
Documentation

The finite fibre of places over the specified place along the integral algebra homomorphism.

Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
variable {K F F₁ Z : Type*} [Field K] [Field F] [Field F₁] [Field Z]
  [Algebra K F] [Algebra K F₁] [Algebra K Z]
namespace Place
section Fiber
variable [HasPrincipalDivisors K Z]
Lean source · statement
def fiberAlong (u : F₁ →ₐ[K] Z) (hu : u.toRingHom.IsIntegral) (w₁ : Place K F₁) :
    Finset (Place K Z)
theorem

mem_fiberAlong

L306 ↗
AlgebraicCurve.Place.mem_fiberAlong
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
variable {K F F₁ Z : Type*} [Field K] [Field F] [Field F₁] [Field Z]
  [Algebra K F] [Algebra K F₁] [Algebra K Z]
namespace Place
section Fiber
variable [HasPrincipalDivisors K Z]
Lean source · statement
theorem mem_fiberAlong {u : F₁ →ₐ[K] Z} {hu : u.toRingHom.IsIntegral} {w₁ : Place K F₁}
    {W : Place K Z} : W ∈ fiberAlong u hu w₁ ↔ W.restrictAlong u hu = w₁
theorem

pullbackAlong_single

L313 ↗
AlgebraicCurve.Divisor.pullbackAlong_single
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
variable {K F F₁ Z : Type*} [Field K] [Field F] [Field F₁] [Field Z]
  [Algebra K F] [Algebra K F₁] [Algebra K Z]
namespace Place
section Fiber
variable [HasPrincipalDivisors K Z]
Lean source · statement
theorem _root_.AlgebraicCurve.Divisor.pullbackAlong_single (u : F₁ →ₐ[K] Z)
    (hu : u.toRingHom.IsIntegral) (w₁ : Place K F₁) (n : ℤ) :
    Divisor.pullbackAlong u hu (Finsupp.single w₁ n)
      = ∑ W ∈ fiberAlong u hu w₁,
          Finsupp.single W (n * W.ramificationIndexAlong u)
def

SeparableAlong

L337 ↗
AlgebraicCurve.SeparableAlong
Documentation

The field extension induced by the algebra homomorphism is separable.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section AlongTransport
variable {K F F₁ : Type*} [Field K] [Field F] [Field F₁] [Algebra K F] [Algebra K F₁]
variable (K) in
Lean source · statement
def SeparableAlong (φ : F →ₐ[K] F₁) : Prop
def

IntertwinesAlong

L354 ↗
AlgebraicCurve.SemilinearAut.IntertwinesAlong
Documentation

The field homomorphism intertwines the two semilinear automorphisms.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace SemilinearAut
section Intertwines
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
def IntertwinesAlong (ι : F →+* F') (g : SemilinearAut K F) (g' : SemilinearAut K F') : Prop
theorem

inv

L357 ↗
AlgebraicCurve.SemilinearAut.IntertwinesAlong.inv
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace SemilinearAut
section Intertwines
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem IntertwinesAlong.inv {ι : F →+* F'} {g : SemilinearAut K F} {g' : SemilinearAut K F'}
    (h : IntertwinesAlong ι g g') : IntertwinesAlong ι g⁻¹ g'⁻¹
theorem

one

L363 ↗
AlgebraicCurve.SemilinearAut.IntertwinesAlong.one
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace SemilinearAut
section Intertwines
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem IntertwinesAlong.one (ι : F →+* F') :
    IntertwinesAlong ι (1 : SemilinearAut K F) (1 : SemilinearAut K F')
theorem

mul

L367 ↗
AlgebraicCurve.SemilinearAut.IntertwinesAlong.mul
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
namespace SemilinearAut
section Intertwines
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
Lean source · statement
theorem IntertwinesAlong.mul {ι : F →+* F'} {g₁ g₂ : SemilinearAut K F}
    {g₁' g₂' : SemilinearAut K F'} (h₁ : IntertwinesAlong ι g₁ g₁')
    (h₂ : IntertwinesAlong ι g₂ g₂') : IntertwinesAlong ι (g₁ * g₂) (g₁' * g₂')

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