module

public import Papers.OaiReconstructionMilnorTheory.Helpers.PBasis
public import Mathlib.LinearAlgebra.BilinearMap
public import Mathlib.Algebra.Algebra.ZMod

/-! # Logarithmic derivations detect independent Milnor symbols -/

@[expose] public section

namespace Papers.OaiReconstructionMilnorTheory

open scoped TensorProduct

variable (p : ℕ) {F : Type*} [Field F] [CharP F p]

-- @node: symbolCoeffAlgebra
/-- For [a modulus p](hyp:p), the [coefficient algebra structure on F](goal)
lets residues modulo p act on F through the canonical map into this
characteristic-p field. -/
local instance symbolCoeffAlgebra : Algebra (Coeff p) F := ZMod.algebra F p

-- @node: symbolLogUnits
/-- For [a modulus p](hyp:p) and [a derivation D that is linear over the
subfield generated by p-th powers](hyp:D), the [logarithmic derivative on
nonzero elements of F](goal) sends u to D applied to u divided by u,
converting multiplication of inputs into addition of outputs. -/
noncomputable def symbolLogUnits (D : Derivation ↥(powSubfield p F) F F) :
    Fˣ →* Multiplicative F where
  toFun u := Multiplicative.ofAdd (D (u : F) / (u : F))
  map_one' := by change D 1 / 1 = 0; simp
  map_mul' u v := by
    change D ((u : F) * (v : F)) / ((u : F) * (v : F)) =
      D (u : F) / (u : F) + D (v : F) / (v : F)
    rw [D.leibniz]
    simp only [smul_eq_mul]
    field_simp
    <;> ring

-- @node: symbolLog
/-- For [a modulus p](hyp:p) and [a derivation D linear over the subfield
generated by p-th powers](hyp:D), the [linear logarithmic derivative on
degree-one Milnor classes](goal) is formed by [descending the map u to D
applied to u divided by u to classes modulo p-th powers](step:1) and
[regarding this additive map as linear over residues modulo p](step:2). -/
noncomputable def symbolLog (D : Derivation ↥(powSubfield p F) F F) :
    MilnorOne F p →ₗ[Coeff p] F :=
  let A : MilnorOne F p →+ F := (QuotientGroup.lift (powMonoidHom p : Fˣ →* Fˣ).range (symbolLogUnits p D) (by
    rintro u ⟨v, rfl⟩
    change D ((v : F) ^ p) / ((v : F) ^ p) = 0
    have h := D.map_algebraMap
      (⟨(v : F) ^ p, Subfield.subset_closure ⟨(v : F), rfl⟩⟩ : powSubfield p F)
    change D ((v : F) ^ p) = 0 at h
    rw [h, zero_div])).toAdditiveLeft
  A.toZModLinearMap p

-- @node: symbolLog_cls
/-- If [f is nonzero](hyp:hf), then [the logarithmic derivative associated
with D sends the degree-one Milnor class of f to D applied to f divided by f](goal). -/
lemma symbolLog_cls (D : Derivation ↥(powSubfield p F) F F)
    (f : F) (hf : f ≠ 0) : symbolLog p D (cls p f) = D f / f := by
  unfold cls MilnorOne
  rw [dif_neg hf]
  rfl

-- @node: symbolPairing
/-- For [a modulus p](hyp:p) and [two derivations Ds and Dt linear over the
subfield generated by p-th powers](hyp:Ds,Dt), the [alternating logarithmic
pairing](goal) is the linear map on pairs of degree-one Milnor classes that
multiplies their Ds and Dt logarithmic derivatives and subtracts the product
with the derivations interchanged. -/
noncomputable def symbolPairing (Ds Dt : Derivation ↥(powSubfield p F) F F) :
    MilnorOne F p ⊗[Coeff p] MilnorOne F p →ₗ[Coeff p] F :=
  TensorProduct.lift
    ((LinearMap.mul (Coeff p) F).compl₁₂ (symbolLog p Ds) (symbolLog p Dt) -
      (LinearMap.mul (Coeff p) F).compl₁₂ (symbolLog p Dt) (symbolLog p Ds))

-- @node: symbolPairing_tmul
/-- If [f is nonzero](hyp:hf) and [g is nonzero](hyp:hg), then [the alternating
pairing on the tensor of their Milnor classes equals the logarithmic Ds
derivative of f times the logarithmic Dt derivative of g, minus the
logarithmic Dt derivative of f times the logarithmic Ds derivative of g](goal). -/
lemma symbolPairing_tmul (Ds Dt : Derivation ↥(powSubfield p F) F F)
    (f g : F) (hf : f ≠ 0) (hg : g ≠ 0) :
    symbolPairing p Ds Dt (cls p f ⊗ₜ[Coeff p] cls p g) =
      Ds f / f * (Dt g / g) - Dt f / f * (Ds g / g) := by
  simp [symbolPairing, symbolLog_cls, hf, hg]

-- @node: symbolPairing_steinberg
/-- [Every Steinberg relation is annihilated by the alternating logarithmic
pairing associated with Ds and Dt](goal). -/
lemma symbolPairing_steinberg (Ds Dt : Derivation ↥(powSubfield p F) F F) :
    steinbergRel p F ≤ LinearMap.ker (symbolPairing p Ds Dt) := by
  apply Submodule.span_le.mpr
  rintro _ ⟨f, hf, hf1, rfl⟩
  change symbolPairing p Ds Dt (cls p f ⊗ₜ[Coeff p] cls p (1 - f)) = 0
  rw [symbolPairing_tmul p Ds Dt f (1 - f) hf
    (sub_ne_zero.mpr (Ne.symm hf1))]
  simp only [map_sub, Derivation.map_one_eq_zero, zero_sub]
  ring

-- @node: symbolFunctional
/-- For [a modulus p](hyp:p) and [two derivations Ds and Dt linear over the
subfield generated by p-th powers](hyp:Ds,Dt), the [logarithmic functional
on degree-two Milnor classes](goal) is the alternating logarithmic pairing
descended through the Steinberg relations. -/
noncomputable def symbolFunctional (Ds Dt : Derivation ↥(powSubfield p F) F F) :
    MilnorTwo p F →ₗ[Coeff p] F :=
  (steinbergRel p F).liftQ (symbolPairing p Ds Dt) (symbolPairing_steinberg p Ds Dt)

-- @node: symbolFunctional_symbol
/-- If [f is nonzero](hyp:hf) and [g is nonzero](hyp:hg), then [the logarithmic
functional on their Milnor symbol equals the logarithmic Ds derivative of f
times the logarithmic Dt derivative of g, minus the logarithmic Dt derivative
of f times the logarithmic Ds derivative of g](goal). -/
lemma symbolFunctional_symbol (Ds Dt : Derivation ↥(powSubfield p F) F F)
    (f g : F) (hf : f ≠ 0) (hg : g ≠ 0) :
    symbolFunctional p Ds Dt (milnorSymbol p f g hf hg) =
      Ds f / f * (Dt g / g) - Dt f / f * (Ds g / g) := by
  exact symbolPairing_tmul p Ds Dt f g hf hg

-- @node: symbol_euler_generator
/-- If [p is prime](hyp:hp) and [each derivation D at coordinate j multiplies
every p-monomial in b by its exponent at j](hyp:hD), then [D at coordinate j
sends the k-th generator to itself when j equals k and to zero otherwise](goal). -/
lemma symbol_euler_generator (hp : PrimeChar p) {e : ℕ} (b : Fin e → F)
    (D : Fin e → Derivation ↥(powSubfield p F) F F)
    (hD : ∀ j i, D j (pMonomial p b i) =
      (((i j : ℕ) : ↥(powSubfield p F))) • pMonomial p b i) (j k : Fin e) :
    D j (b k) = if j = k then b k else 0 := by
  classical
  let : NeZero p := ⟨hp.ne_zero⟩
  let i : Fin e → Fin p := Function.update 0 k ⟨1, hp.one_lt⟩
  have haxis : pMonomial p b i = b k := by
    simpa [i] using pMonomial_axis p b k i (by intro l hl; simp [i, hl])
  have h := hD j i
  rw [haxis] at h
  by_cases hjk : j = k
  · simpa [i, hjk] using h
  · simpa [i, hjk] using h

-- @node: symbol_pair_derivations
/-- If [p is prime](hyp:hp), [F is finite dimensional over the subfield
generated by p-th powers](hyp:hfin), and [s and t are p-independent](hyp:hpair),
then [there are two derivations over that subfield: Ds sends s to s and t to
zero, while Dt sends t to t and s to zero](goal). -/
lemma symbol_pair_derivations (hp : PrimeChar p)
    (hfin : FiniteDimensional ↥(powSubfield p F) F) {s t : F}
    (hpair : IsPIndependent p F ![s, t]) :
    ∃ Ds Dt : Derivation ↥(powSubfield p F) F F,
      Ds s = s ∧ Dt t = t ∧ Ds t = 0 ∧ Dt s = 0 := by
  obtain ⟨e, he, b, hb, hinit⟩ :=
    pIndependent_extends_to_pBasis p hp (inferInstance : CharP F p) hfin ![s, t] hpair
  obtain ⟨D, _, hEuler⟩ := pBasis_euler_operators p hp (inferInstance : CharP F p) b hb
  let js : Fin e := Fin.castLE he (0 : Fin 2)
  let jt : Fin e := Fin.castLE he (1 : Fin 2)
  have hbs : b js = s := by simpa [js] using hinit 0
  have hbt : b jt = t := by simpa [jt] using hinit 1
  have hne : js ≠ jt := by intro h; have := congrArg Fin.val h; simp [js, jt] at this
  refine ⟨D js, D jt, ?_, ?_, ?_, ?_⟩
  · simpa [hbs] using symbol_euler_generator p hp b D hEuler js js
  · simpa [hbt] using symbol_euler_generator p hp b D hEuler jt jt
  · simpa [hbt, hne] using symbol_euler_generator p hp b D hEuler js jt
  · simpa [hbs, Ne.symm hne] using symbol_euler_generator p hp b D hEuler jt js

-- @node: symbol_pair_independent
/-- If [p is prime](hyp:hp), [s lies outside the subfield generated by p-th
powers](hyp:hs), and [t lies outside the field obtained by adjoining s to
that subfield](hyp:ht), then [s and t are p-independent](goal). -/
lemma symbol_pair_independent (hp : PrimeChar p) {s t : F}
    (hs : s ∉ powSubfield p F)
    (ht : t ∉ IntermediateField.adjoin ↥(powSubfield p F) {s}) :
    IsPIndependent p F ![s, t] := by
  have hempty : IsPIndependent p F (Fin.elim0 : Fin 0 → F) := by
    constructor
    simp [PIndependentDegree]
  have hs' : s ∉ IntermediateField.adjoin ↥(powSubfield p F)
      (Set.range (Fin.elim0 : Fin 0 → F)) := by
    rw [Set.range_eq_empty, IntermediateField.adjoin_empty, IntermediateField.mem_bot]
    rintro ⟨c, rfl⟩
    exact hs c.property
  have hsingle := pIndependent_snoc p hp (inferInstance : CharP F p)
    (Fin.elim0 : Fin 0 → F) hempty s hs'
  have ht' : t ∉ IntermediateField.adjoin ↥(powSubfield p F)
      (Set.range (Fin.snoc (Fin.elim0 : Fin 0 → F) s)) := by
    simpa [Fin.range_snoc] using ht
  have hpair := pIndependent_snoc p hp (inferInstance : CharP F p)
    (Fin.snoc (Fin.elim0 : Fin 0 → F) s) hsingle t ht'
  have heq : Fin.snoc (Fin.snoc (Fin.elim0 : Fin 0 → F) s) t = ![s, t] := by
    funext i
    fin_cases i <;> rfl
  rw [heq] at hpair
  exact hpair

-- @node: symbol_independent_ne_zero
/-- If [p is prime](hyp:hp), [F is finite dimensional over the subfield
generated by p-th powers](hyp:hfin), [s is nonzero](hyp:hs0), [t is nonzero](hyp:ht0),
and [s and t are p-independent](hyp:hpair), then [their degree-two Milnor
symbol modulo p is nonzero](goal). -/
lemma symbol_independent_ne_zero (hp : PrimeChar p)
    (hfin : FiniteDimensional ↥(powSubfield p F) F) {s t : F}
    (hs0 : s ≠ 0) (ht0 : t ≠ 0) (hpair : IsPIndependent p F ![s, t]) :
    milnorSymbol p s t hs0 ht0 ≠ 0 := by
  obtain ⟨Ds, Dt, hss, htt, hst, hts⟩ := symbol_pair_derivations p hp hfin hpair
  have hone : symbolFunctional p Ds Dt (milnorSymbol p s t hs0 ht0) = 1 := by
    rw [symbolFunctional_symbol, hss, htt, hst, hts]
    simp [hs0, ht0]
  intro hz
  rw [hz, map_zero] at hone
  exact zero_ne_one hone

end Papers.OaiReconstructionMilnorTheory