NYLL
Module

BaseChange.lean

Nyll.JacobianVarieties.Pic0.BaseChange
9 declarations indexed from sourceView source ↗

Module documentation

Extension of constants on Picard groups

Extension of constants on divisors induces a homomorphism on degree-zero divisor classes.

Imports1
Imported by1

Declarations

theorem

algebraMap_inv_apply_of_forall_algebraMap_apply

L33 ↗
AlgebraicCurve.algebraMap_inv_apply_of_forall_algebraMap_apply
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section Equivariance
open scoped Pointwise
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra F F']
  {σ : F ≃ₐ[K] F} {σ' : F' ≃ₐ[K'] F'}
Lean source · statement
theorem algebraMap_inv_apply_of_forall_algebraMap_apply
    (hσ : ∀ f : F, algebraMap F F' (σ f) = σ' (algebraMap F F' f)) (f : F) :
    algebraMap F F' (σ⁻¹ f) = σ'⁻¹ (algebraMap F F' f)
theorem

restrictConstants_smul

L43 ↗
AlgebraicCurve.Place.restrictConstants_smul
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section Equivariance
open scoped Pointwise
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra F F']
  {σ : F ≃ₐ[K] F} {σ' : F' ≃ₐ[K'] F'}
variable [Algebra K K'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
Lean source · statement
theorem Place.restrictConstants_smul (hσ : ∀ f : F, algebraMap F F' (σ f) = σ' (algebraMap F F' f))
    (w : Place K' F') :
    Place.restrictConstants F (K := K) (σ' • w) = σ • Place.restrictConstants F (K := K) w
theorem

ramificationIndex_forgetConstants_smul

L56 ↗
AlgebraicCurve.Place.ramificationIndex_forgetConstants_smul
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section Equivariance
open scoped Pointwise
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra F F']
  {σ : F ≃ₐ[K] F} {σ' : F' ≃ₐ[K'] F'}
variable [Algebra K K'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
Lean source · statement
theorem Place.ramificationIndex_forgetConstants_smul
    (hσ : ∀ f : F, algebraMap F F' (σ f) = σ' (algebraMap F F' f)) (w : Place K' F') :
    Place.ramificationIndex (F := F) (Place.forgetConstants (K := K) (σ' • w)) =
      Place.ramificationIndex (F := F) (Place.forgetConstants (K := K) w)
theorem

pullbackConstants_smul

L72 ↗
AlgebraicCurve.Divisor.pullbackConstants_smul
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section Equivariance
open scoped Pointwise
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K F] [Algebra K' F'] [Algebra F F']
  {σ : F ≃ₐ[K] F} {σ' : F' ≃ₐ[K'] F'}
variable [Algebra K K'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F']
Lean source · statement
theorem Divisor.pullbackConstants_smul [HasPrincipalDivisors K' F']
    (hσ : ∀ f : F, algebraMap F F' (σ f) = σ' (algebraMap F F' f)) (D : Divisor K F) :
    Divisor.pullbackConstants K' F' (σ • D) = σ' • Divisor.pullbackConstants K' F' D
def

degZeroBaseChangeHom

L92 ↗
AlgebraicCurve.Pic0.degZeroBaseChangeHom
Documentation

Extend constants on degree-zero divisors.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section ClassGroup
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F'] [ConstantFieldDegreeFormula K K' F F']
variable (K K' F F') in
Lean source · statement
def Pic0.degZeroBaseChangeHom :
    Divisor.degZero (K := K) (F := F) →+ Divisor.degZero (K := K') (F := F')
theorem

coe_degZeroBaseChangeHom

L97 ↗
AlgebraicCurve.Pic0.coe_degZeroBaseChangeHom
Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve
section ClassGroup
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F'] [ConstantFieldDegreeFormula K K' F F']
variable (K K' F F') in
Lean source · statement
theorem Pic0.coe_degZeroBaseChangeHom (D : Divisor.degZero (K := K) (F := F)) :
    (degZeroBaseChangeHom K K' F F' D : Divisor K' F') =
      Divisor.pullbackConstants K' F' (D : Divisor K F)
def

baseChange

L104 ↗
AlgebraicCurve.Pic0.baseChange
Documentation

The homomorphism on degree-zero divisor classes induced by extending constants.

Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section ClassGroup
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F'] [ConstantFieldDegreeFormula K K' F F']
variable (K K' F F') in
variable (K K' F F') in
Lean source · statement
def Pic0.baseChange : Pic0 K F →+ Pic0 K' F'
theorem

baseChange_mk

L111 ↗
AlgebraicCurve.Pic0.baseChange_mk
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section ClassGroup
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F'] [ConstantFieldDegreeFormula K K' F F']
variable (K K' F F') in
variable (K K' F F') in
Lean source · statement
theorem Pic0.baseChange_mk (D : Divisor.degZero (K := K) (F := F)) :
    Pic0.baseChange K K' F F' (Pic0.mk D) =
      Pic0.mk ⟨Divisor.pullbackConstants K' F' (D : Divisor K F),
        Divisor.pullbackConstants_mem_degZero D.2⟩
theorem

baseChange_smul

L117 ↗
AlgebraicCurve.Pic0.baseChange_smul
Source context 6 commands

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

noncomputable section
namespace AlgebraicCurve
section ClassGroup
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
  [Algebra.IsIntegral F F'] [HasPrincipalDivisors K' F'] [ConstantFieldDegreeFormula K K' F F']
variable (K K' F F') in
variable (K K' F F') in
Lean source · statement
theorem Pic0.baseChange_smul {σ : F ≃ₐ[K] F} {σ' : F' ≃ₐ[K'] F'}
    (hσ : ∀ f : F, algebraMap F F' (σ f) = σ' (algebraMap F F' f)) (x : Pic0 K F) :
    Pic0.baseChange K K' F F' (σ • x) = σ' • Pic0.baseChange K K' F F' x

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