Module

Maps.lean

Nyll.AlgebraicCurves.Differentials.Maps

8 declarations indexed from sourceView source ↗

Module documentation

Differentials, residues, and divisor correspondences

Pullback, trace, and correspondence maps for Kähler differentials along base-field algebra homomorphisms.

Imports2

Nyll.AlgebraicCurves.Divisors.Correspondences
Mathlib.RingTheory.Etale.Field

Imported by24

def

pullbackAlong

L34 ↗

AlgebraicCurve.Differential.pullbackAlong

Documentation

Pullback of Kähler differentials along a base-field algebra homomorphism.

Source context 5 commands

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

noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
namespace Differential
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

def pullbackAlong (φ : F →ₐ[K] F') : Ω[F⁄K] →ₗ[K] Ω[F'⁄K]

theorem

pullbackAlong_D

L39 ↗

AlgebraicCurve.Differential.pullbackAlong_D

Source context 5 commands

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

noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
namespace Differential
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem pullbackAlong_D (φ : F →ₐ[K] F') (f : F) :
    pullbackAlong φ (D K F f) = D K F' (φ f)

theorem

pullbackAlong_smul

L45 ↗

AlgebraicCurve.Differential.pullbackAlong_smul

Source context 5 commands

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

noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
namespace Differential
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem pullbackAlong_smul (φ : F →ₐ[K] F') (f : F) (ω : Ω[F⁄K]) :
    pullbackAlong φ (f • ω) = φ f • pullbackAlong φ ω

def

traceAlong

L56 ↗

AlgebraicCurve.Differential.traceAlong

Documentation

Trace of differentials through the formally étale tensor equivalence when the induced extension is separable, and zero otherwise.

Source context 6 commands

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

noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
namespace Differential
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
open Classical in

Lean source · statement

def traceAlong (φ : F →ₐ[K] F') : Ω[F'⁄K] →ₗ[K] Ω[F⁄K]

theorem

traceAlong_smul_pullbackAlong

L68 ↗

AlgebraicCurve.Differential.traceAlong_smul_pullbackAlong

Source context 5 commands

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

noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
namespace Differential
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · full declaration

theorem traceAlong_smul_pullbackAlong (φ : F →ₐ[K] F') (h : SeparableAlong K φ) (u : F')
    (ω : Ω[F⁄K]) :
    traceAlong φ (u • pullbackAlong φ ω) =
      (letI := algebraAlong φ; Algebra.trace F F' u) • ω := by
  let := algebraAlong φ
  have := isScalarTower_along φ
  have : Algebra.IsSeparable F F' := h
  have : Algebra.FormallyEtale F F' := Algebra.FormallyEtale.of_isSeparable F F'
  rw [traceAlong, dite_eq_left h]
  simp only [LinearMap.coe_restrictScalars, LinearMap.coe_comp, LinearEquiv.coe_coe,
    Function.comp_apply]
  have hsymm : (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale K F F').symm
      (u • pullbackAlong φ ω) = u ⊗ₜ ω := by
    rw [LinearEquiv.symm_apply_eq, KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale_apply,
      KaehlerDifferential.mapBaseChange_tmul]
    rfl
  rw [hsymm, LinearMap.rTensor_tmul, TensorProduct.lid_tmul]

theorem

traceAlong_of_not

L86 ↗

AlgebraicCurve.Differential.traceAlong_of_not

Source context 5 commands

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

noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
namespace Differential
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem traceAlong_of_not (φ : F →ₐ[K] F') (h : ¬ SeparableAlong K φ) : traceAlong φ = 0

def

correspondence

L91 ↗

AlgebraicCurve.Differential.correspondence

Documentation

The differential correspondence formed by pullback along the second map and trace along the first.

Source context 5 commands

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

noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
namespace Differential
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

def correspondence (φ ψ : F →ₐ[K] F') : Ω[F⁄K] →ₗ[K] Ω[F⁄K]

theorem

correspondence_apply

L94 ↗

AlgebraicCurve.Differential.correspondence_apply

Source context 5 commands

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

noncomputable section
open KaehlerDifferential TensorProduct
namespace AlgebraicCurve
namespace Differential
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']

Lean source · statement

theorem correspondence_apply (φ ψ : F →ₐ[K] F') (ω : Ω[F⁄K]) :
    correspondence φ ψ ω = traceAlong φ (pullbackAlong ψ ω)

Module documentation

Differentials, residues, and divisor correspondences

Declarations