Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicCurve_DifferentialPushPull.lean

definition module

Pull-back, trace and correspondence maps on Kähler differentials

Throughout, K, F, F' are fields with F, F' algebras over K, and the maps considered are K-algebra homomorphisms \varphi:F\to F'; no Algebra F F' instance is fixed globally, so that two embeddings of the same pair of fields can be used simultaneously. Each \varphi determines an F-algebra structure on F' (algebraAlong, the algebra given by \varphi viewed as a ring homomorphism) together with the tower K\subseteq F\subseteq F', and the constructions here are made relative to that structure. pullbackAlong φ is the K-linear map \Omega_{F/K}\to\Omega_{F'/K} obtained from Mathlib's functoriality of Kähler differentials; it is characterised by D_{F/K}f\mapsto D_{F'/K}(\varphi f) and satisfies \varphi^*(f\cdot\omega)=\varphi(f)\cdot\varphi^*\omega. traceAlong φ is the K-linear map \Omega_{F'/K}\to\Omega_{F/K} defined by a case distinction on the predicate SeparableAlong K φ, which says that F' is a separable F-algebra for the structure induced by \varphi: in that case F' is formally étale over F, so the canonical base-change map identifies F'\otimes_F\Omega_{F/K} with \Omega_{F'/K}, and traceAlong φ is the composite of the inverse of this identification with \mathrm{Tr}_{F'/F}\otimes\mathrm{id} and the identification F\otimes_F\Omega_{F/K}\cong\Omega_{F/K}; otherwise it is the zero map. Its characteristic property is recorded as \operatorname{tr}_\varphi(u\cdot\varphi^*\omega)=\mathrm{Tr}_{F'/F}(u)\cdot\omega for u\in F' and \omega\in\Omega_{F/K}, under the separability hypothesis. Finally, for two K-algebra homomorphisms \varphi,\psi:F\to F', correspondence φ ψ is the K-endomorphism \operatorname{tr}_\varphi\circ\psi^* of \Omega_{F/K}, with the pull-back taken along \psi and the trace along \varphi; a companion lemma states this pointwise. No further properties (invariance of regular differentials, compatibility with composition) are asserted here.

Relation to Mathlib

The pull-back is Mathlib's KaehlerDifferential.map, and the separable case of the trace uses Mathlib's KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale together with Algebra.trace; what is new is the packaging along a K-algebra homomorphism rather than a registered Algebra F F' instance, and the resulting trace map on differentials, which Mathlib does not provide.

Where it is used

These maps supply the action on differentials of a correspondence between curves whose function-field legs are \varphi and \psi, matching in argument order the divisor- and \mathrm{Pic}^0-level correspondence \psi_*\varphi^* defined for the same pair of embeddings.

References

  1. R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977, ch. II §8 and ch. IV
  2. H. Matsumura, Commutative Ring Theory, Cambridge Studies in Advanced Mathematics 8, Cambridge University Press, 1986, ch. 10

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_AlgebraicCurve_DifferentialPushPull.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicCurve_Correspondence

set_option autoImplicit false

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']

def pullbackAlong (φ : F →ₐ[K] F') : Ω[F⁄K] →ₗ[K] Ω[F'⁄K] :=
  letI := algebraAlong φ
  haveI := isScalarTower_along φ
  (KaehlerDifferential.map K K F F').restrictScalars K

theorem pullbackAlong_D (φ : F →ₐ[K] F') (f : F) :
    pullbackAlong φ (D K F f) = D K F' (φ f) := by
  letI := algebraAlong φ
  haveI := isScalarTower_along φ
  exact KaehlerDifferential.map_D K K F F' f

theorem pullbackAlong_smul (φ : F →ₐ[K] F') (f : F) (ω : Ω[F⁄K]) :
    pullbackAlong φ (f • ω) = φ f • pullbackAlong φ ω := by
  letI := algebraAlong φ
  haveI := isScalarTower_along φ
  show KaehlerDifferential.map K K F F' (f • ω) = _
  rw [LinearMap.map_smul_of_tower]
  rfl

open Classical in

def traceAlong (φ : F →ₐ[K] F') : Ω[F'⁄K] →ₗ[K] Ω[F⁄K] :=
  if h : SeparableAlong K φ then
    letI := algebraAlong φ
    haveI := isScalarTower_along φ
    haveI : Algebra.IsSeparable F F' := h
    haveI : Algebra.FormallyEtale F F' := Algebra.FormallyEtale.of_isSeparable F F'
    ((TensorProduct.lid F Ω[F⁄K]).toLinearMap ∘ₗ
      (Algebra.trace F F').rTensor Ω[F⁄K] ∘ₗ
      (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale K F F').symm.toLinearMap).restrictScalars K
  else 0

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
  letI := algebraAlong φ
  haveI := isScalarTower_along φ
  haveI : Algebra.IsSeparable F F' := h
  haveI : Algebra.FormallyEtale F F' := Algebra.FormallyEtale.of_isSeparable F F'
  rw [traceAlong, dif_pos 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 (φ : F →ₐ[K] F') (h : ¬ SeparableAlong K φ) : traceAlong φ = 0 := by
  rw [traceAlong, dif_neg h]

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

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

end Differential

end AlgebraicCurve

end

Statements phrased using this module (44)