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