module

public import Papers.OaiReconstructionMilnorTheory.Helpers.PDegree
public import Papers.OaiReconstructionMilnorTheory.Helpers.PBasis
public import Papers.OaiReconstructionMilnorTheory.Helpers.SymbolPairing

/-! # Coordinate derivations and vanishing Milnor symbols -/

@[expose] public section

namespace Papers.OaiReconstructionMilnorTheory

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

-- @node: ass:pin-3
/-- For [an exponent p](hyp:p), [a finite family b in F](hyp:b), [coordinates
j and k](hyp:j,k), [elements s and t of F](hyp:s,t), and [derivations Ds](hyp:Ds)
and [Dt](hyp:Dt) over the subfield generated by p-th powers, the
[coordinate Euler condition](goal) requires [b to be a p-basis](step:1),
[j and k to be distinct](step:2), [the j-th entry to equal s](step:3),
[the k-th entry to equal t](step:4), [Ds to send the j-th basis element to
itself and every other basis element to zero](step:5), and [Dt to send the
k-th basis element to itself and every other basis element to zero](step:6). -/
def IsCoordEulerDerivation {e : ℕ} (b : Fin e → F) (j k : Fin e)
    (s t : F)
    (Ds : Derivation ↥(powSubfield p F) F F) -- @realizes D_s(C-linear derivation)
    (Dt : Derivation ↥(powSubfield p F) F F) : Prop := -- @realizes D_t(C-linear derivation)
  IsPBasis p F b ∧ -- @realizes s_j(the fixed common p-basis of F/C)
  j ≠ k ∧
  b j = s ∧ -- @realizes s(the j-th entry of the chosen extending p-basis)
  b k = t ∧ -- @realizes t(the distinct k-th entry of the same extending p-basis)
  (∀ i, Ds (b i) = if i = j then b j else 0) ∧ -- @realizes D_s(Euler values on that p-basis)
  (∀ i, Dt (b i) = if i = k then b k else 0) -- @realizes D_t(Euler values on the same p-basis)

-- @node: def:pair-derivations
/-- For [an exponent p](hyp:p), [a number e of coordinates](hyp:e),
[a family b of e elements of F](hyp:b), [coordinates j and k](hyp:j,k),
[elements s and t](hyp:s,t), and [derivations Ds](hyp:Ds) and [Dt](hyp:Dt)
over the subfield generated by p-th powers, the [pair derivation condition](goal)
says that b is a p-basis with distinct entries s and t at j and k, and that
Ds and Dt each fix their own coordinate basis element and kill all the others. -/
def IsPairDerivations (e : ℕ)
    (b : Fin e → F) -- @realizes s_j(fixed basis; constrained below)
    (j k : Fin e) (s t : F)
    (Ds : Derivation ↥(powSubfield p F) F F) -- @realizes D_s(C-linear derivation)
    (Dt : Derivation ↥(powSubfield p F) F F) : Prop := -- @realizes D_t(C-linear derivation)
  IsCoordEulerDerivation p b j k s t Ds Dt

-- @node: ass:zero-symbol-inputs
/-- For [elements s and t of F](hyp:s,t), the [nonzero symbol input condition](goal)
requires [s to be nonzero](step:1) and [t to be nonzero](step:2). -/
def ZeroSymbolInputs (s t : F) : Prop := -- @realizes s(carrier F) @realizes t(carrier F)
  s ≠ 0 ∧ -- @realizes s(nonzero input of the zero-symbol lemma)
  t ≠ 0 -- @realizes t(nonzero input of the zero-symbol lemma)

-- @node: ass:zero-symbol-antecedent
/-- For [a modulus p](hyp:p), [elements s and t of F](hyp:s,t), and
[their nonzero input condition](hyp:hst), the [zero-symbol antecedent](goal)
requires [s to lie outside the subfield generated by p-th powers](step:1)
and [the Milnor symbol of s and t modulo p to vanish](step:2). -/
def ZeroSymbolAntecedent (s t : F) (hst : ZeroSymbolInputs s t) : Prop :=
  s ∉ powSubfield p F ∧ -- @realizes s(outside C)
  milnorSymbol p s t hst.1 hst.2 = 0

-- @node: ass:pin-1
/-- For [an exponent p](hyp:p), [a field F](hyp:F), and [an element d of F](hyp:d),
the [affine slope condition](goal) requires [d to belong to the subfield
generated by p-th powers](step:1) and [d to be nonzero](step:2). -/
def AffineCoeffPin (F : Type*) [Field F] (d : F) : Prop := -- @realizes d(carrier F)
  d ∈ powSubfield p F ∧ d ≠ 0 -- @realizes d(locally bound nonzero affine coefficient in C)

-- @node: ass:affine-symbol-inputs
/-- For [an exponent p](hyp:p) and [elements c, d, and t of F](hyp:c,d,t),
the [affine symbol input condition](goal) requires [c to be a nonzero element
of the subfield generated by p-th powers](step:1), [d to be a nonzero element
of that subfield](step:2), [t to be nonzero](step:3), and [c + d times t to
be nonzero](step:4). -/
def AffineSymbolInputs (c d t : F) : Prop := -- @realizes c(carrier F) @realizes d(carrier F)
  (c ∈ powSubfield p F ∧ c ≠ 0) ∧ -- @realizes c(nonzero affine constant in C)
  AffineCoeffPin p F d ∧ -- @realizes d(nonzero affine slope in C)
  t ≠ 0 ∧ -- @realizes t(nonzero affine input)
  c + d * t ≠ 0

-- @node: cls_eq_zero_of_mem_powSubfield
/-- If [p is prime](hyp:hp), [F has characteristic p](hyp:hF), [a belongs
to the subfield generated by p-th powers](hyp:ha), and [a is nonzero](hyp:ha0),
then [the degree-one Milnor class of a modulo p is zero](goal). -/
lemma cls_eq_zero_of_mem_powSubfield (hp : PrimeChar p) (hF : CharP F p)
    {a : F} (ha : a ∈ powSubfield p F) (ha0 : a ≠ 0) : cls p a = 0 := by
  let : Fact p.Prime := ⟨hp⟩
  let : CharP F p := hF
  have hle : powSubfield p F ≤ (frobenius F p).fieldRange :=
    Subfield.closure_le.2 (by
      rintro _ ⟨x, rfl⟩
      exact ⟨x, rfl⟩)
  obtain ⟨x, hx⟩ := hle ha
  have hxpow : x ^ p = a := hx
  have hx0 : x ≠ 0 := by
    intro h
    apply ha0
    rw [← hxpow, h, zero_pow hp.ne_zero]
  unfold cls MilnorOne
  rw [dif_neg ha0]
  change (QuotientGroup.mk (Units.mk0 a ha0) :
    Fˣ ⧸ (powMonoidHom p : Fˣ →* Fˣ).range) = 1
  apply (QuotientGroup.eq_one_iff _).2
  refine ⟨Units.mk0 x hx0, ?_⟩
  ext
  exact hxpow

variable (κ : Type*) [Field κ] [Algebra κ F]

-- @node: lem:zero-symbol
/-- If [p is prime](hyp:hp), [F is a finitely generated characteristic-p
extension of the algebraically closed field κ](hyp:hF), [s and t are
nonzero](hyp:hst), and [s lies outside the subfield generated by p-th powers
while the Milnor symbol of s and t vanishes](hyp:hzero), then [t lies in
the field obtained by adjoining s to that subfield](goal). -/
lemma mem_adjoin_of_milnorSymbol_eq_zero (s t : F)
    (hp : PrimeChar p) (hF : GeometricField p κ F)
    (hst : ZeroSymbolInputs s t) (hzero : ZeroSymbolAntecedent p s t hst) :
    t ∈ IntermediateField.adjoin ↥(powSubfield p F) {s} := by
  let : CharP F p := hF.2.1
  by_contra ht
  have hpair := symbol_pair_independent p hp hzero.1 ht
  have hnonzero := symbol_independent_ne_zero p hp
    (geometricField_finiteDimensional_powSubfield p κ F hp hF) hst.1 hst.2 hpair
  exact hnonzero hzero.2

-- @node: lem:affine-symbol
/-- If [p is prime](hyp:hp), [F is a finitely generated characteristic-p
extension of the algebraically closed field κ](hyp:hF), and [c and d are
nonzero elements of the subfield generated by p-th powers, with both t and
c + d times t nonzero](hyp:hinputs), then [the Milnor symbol of t and
c + d times t modulo p vanishes](goal). -/
lemma milnorSymbol_affine_eq_zero (c d t : F)
    (hp : PrimeChar p) (hF : GeometricField p κ F) (hinputs : AffineSymbolInputs p c d t) :
    milnorSymbol p t (c + d * t) hinputs.2.2.1 hinputs.2.2.2 = 0 := by
  obtain ⟨⟨hc, hc0⟩, ⟨hd, hd0⟩, ht0, hsum0⟩ := hinputs
  let a : F := -d / c
  let b : F := 1 / c
  let q : F := a * t
  have ha0 : a ≠ 0 := div_ne_zero (neg_ne_zero.mpr hd0) hc0
  have hb0 : b ≠ 0 := div_ne_zero one_ne_zero hc0
  have hq0 : q ≠ 0 := mul_ne_zero ha0 ht0
  have ha : a ∈ powSubfield p F := (powSubfield p F).div_mem
    ((powSubfield p F).neg_mem hd) hc
  have hb : b ∈ powSubfield p F := (powSubfield p F).div_mem
    (powSubfield p F).one_mem hc
  have hsub : 1 - q = b * (c + d * t) := by
    dsimp [q, a, b]
    field_simp
    ring
  have hq1 : q ≠ 1 := by
    intro h
    have hz : 1 - q = 0 := by rw [h, sub_self]
    rw [hsub] at hz
    exact (mul_ne_zero hb0 hsum0) hz
  have hclsq : cls p q = cls p t := by
    rw [cls_mul p a t ha0 ht0, cls_eq_zero_of_mem_powSubfield p hp hF.2.1 ha ha0,
      zero_add]
  have hclssub : cls p (1 - q) = cls p (c + d * t) := by
    rw [hsub, cls_mul p b (c + d * t) hb0 hsum0,
      cls_eq_zero_of_mem_powSubfield p hp hF.2.1 hb hb0, zero_add]
  unfold milnorSymbol
  rw [← hclsq, ← hclssub]
  apply (Submodule.Quotient.mk_eq_zero (steinbergRel p F)).2
  apply Submodule.subset_span
  exact ⟨q, hq0, hq1, rfl⟩

end Papers.OaiReconstructionMilnorTheory