module

public import Papers.OaiReconstructionMilnorTheory.Helpers.PDegreeMonomials
public import Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
public import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
public import Mathlib.RingTheory.AlgebraicIndependent.Basic
public import Mathlib.RingTheory.Localization.Module
public import Mathlib.RingTheory.MvPolynomial.Expand
public import Mathlib.FieldTheory.Relrank
public import Mathlib.LinearAlgebra.Dimension.Constructions

/-! # Residue monomials in rational function fields -/

public section

namespace Papers.OaiReconstructionMilnorTheory

open MvPolynomial
open scoped IntermediateField.algebraAdjoinAdjoin

variable {σ κ F : Type*} [Fintype σ]
  [Field κ] [Field F] [Algebra κ F]

-- @node: powerResidue_linearIndependent_algebraAdjoin
/-- If [p is positive](hyp:hp) and [the finite family t is algebraically independent
over κ](hyp:ht), then [the monomials in t with individual exponents between zero
and p minus one are linearly independent over the κ-algebra generated by the
p-th powers of t](goal). -/
lemma powerResidue_linearIndependent_algebraAdjoin {p : ℕ} (hp : 0 < p)
    (t : σ → F) (ht : AlgebraicIndependent κ t) :
    LinearIndependent (Algebra.adjoin κ (Set.range (fun i => t i ^ p)))
      (fun r : σ → Fin p => aeval t (monomial (powerResidueExponent r) (1 : κ))) := by
  classical
  rw [Fintype.linearIndependent_iffₛ]
  intro a b heq
  have hrep (a : (σ → Fin p) → Algebra.adjoin κ (Set.range (fun i => t i ^ p))) :
      ∀ r, ∃ f : MvPolynomial σ κ, aeval (fun i => t i ^ p) f = (a r : F) := by
    intro r
    have h : (a r : F) ∈ (aeval (fun i => t i ^ p) : MvPolynomial σ κ →ₐ[κ] F).range := by
      simpa only [Algebra.adjoin_range_eq_range_aeval] using (a r).property
    exact h
  choose f hf using hrep a
  choose g hg using hrep b
  have hpoly : (∑ r, expand p (f r) * monomial (powerResidueExponent r) 1) =
      ∑ r, expand p (g r) * monomial (powerResidueExponent r) 1 := by
    apply ht
    simp only [map_sum, map_mul, aeval_expand]
    change (∑ r, (a r : F) * aeval t (monomial (powerResidueExponent r) 1)) =
      ∑ r, (b r : F) * aeval t (monomial (powerResidueExponent r) 1) at heq
    change (∑ r, aeval (fun i => t i ^ p) (f r) *
      aeval t (monomial (powerResidueExponent r) 1)) =
      ∑ r, aeval (fun i => t i ^ p) (g r) *
        aeval t (monomial (powerResidueExponent r) 1)
    simpa only [hf, hg] using heq
  have hfg := powerResidue_polynomial_decomposition_unique hp f g hpoly
  intro r
  apply Subtype.ext
  rw [← hf r, ← hg r, hfg]

-- @node: powerResidue_linearIndependent_intermediateField
/-- If [p is positive](hyp:hp) and [the finite family t is algebraically independent
over κ](hyp:ht), then [the monomials in t with individual exponents between zero
and p minus one are linearly independent over the field generated by κ and the
p-th powers of t](goal). -/
lemma powerResidue_linearIndependent_intermediateField {p : ℕ} (hp : 0 < p)
    (t : σ → F) (ht : AlgebraicIndependent κ t) :
    LinearIndependent (IntermediateField.adjoin κ (Set.range (fun i => t i ^ p)))
      (fun r : σ → Fin p => aeval t (monomial (powerResidueExponent r) (1 : κ))) := by
  classical
  exact (LinearIndependent.iff_fractionRing
    (Algebra.adjoin κ (Set.range (fun i => t i ^ p)))
    (IntermediateField.adjoin κ (Set.range (fun i => t i ^ p)))).mp
    (powerResidue_linearIndependent_algebraAdjoin hp t ht)

-- @node: powerResidue_aeval_mem_adjoin
/-- [Evaluating any polynomial f with coefficients in κ at the family t gives
an element of the field generated by κ and t](goal). -/
lemma powerResidue_aeval_mem_adjoin (t : σ → F) (f : MvPolynomial σ κ) :
    aeval t f ∈ IntermediateField.adjoin κ (Set.range t) := by
  apply IntermediateField.algebra_adjoin_le_adjoin
  rw [Algebra.adjoin_range_eq_range_aeval]
  exact ⟨f, rfl⟩

-- @node: powerResidue_aeval_mem_span
/-- If [p is positive](hyp:hp), then [every polynomial in the finite family t with
coefficients in κ lies in the linear span of the monomials with individual
exponents between zero and p minus one, over the field generated by κ and the
p-th powers of t](goal). -/
lemma powerResidue_aeval_mem_span {p : ℕ} (hp : 0 < p)
    (t : σ → F) (f : MvPolynomial σ κ) :
    aeval t f ∈ Submodule.span
      (IntermediateField.adjoin κ (Set.range (fun i => t i ^ p)))
      (Set.range (fun r : σ → Fin p =>
        aeval t (monomial (powerResidueExponent r) (1 : κ)))) := by
  classical
  obtain ⟨g, hg⟩ := powerResidue_polynomial_decomposition hp f
  rw [hg, map_sum]
  apply Submodule.sum_mem
  intro r hr
  rw [map_mul, aeval_expand]
  let c : IntermediateField.adjoin κ (Set.range (fun i => t i ^ p)) :=
    ⟨aeval (fun i => t i ^ p) (g r), powerResidue_aeval_mem_adjoin _ _⟩
  exact Submodule.smul_mem _ c (Submodule.subset_span ⟨r, rfl⟩)

-- @node: powerResidue_denominator_pow_mem
/-- In prime characteristic p, [the p-th power of any polynomial b evaluated at
t belongs to the field generated by κ and the p-th powers of t](goal). -/
lemma powerResidue_denominator_pow_mem {p : ℕ} [Fact p.Prime] [CharP κ p]
    (t : σ → F) (b : MvPolynomial σ κ) :
    (aeval t b) ^ p ∈ IntermediateField.adjoin κ (Set.range (fun i => t i ^ p)) := by
  rw [← map_pow, ← MvPolynomial.map_frobenius_expand p, MvPolynomial.map_expand,
    aeval_expand]
  exact powerResidue_aeval_mem_adjoin _ _

-- @node: powerResidue_rational_mem_span
/-- In prime characteristic p, if [x belongs to the field generated by κ and
the finite family t](hyp:hx), then [x lies in the linear span of the monomials
in t with individual exponents between zero and p minus one, over the field
generated by κ and the p-th powers of t](goal). -/
lemma powerResidue_rational_mem_span {p : ℕ} [Fact p.Prime] [CharP κ p]
    (t : σ → F) {x : F} (hx : x ∈ IntermediateField.adjoin κ (Set.range t)) :
    x ∈ Submodule.span
      (IntermediateField.adjoin κ (Set.range (fun i => t i ^ p)))
      (Set.range (fun r : σ → Fin p =>
        aeval t (monomial (powerResidueExponent r) (1 : κ)))) := by
  classical
  have hp : 0 < p := (Fact.out : p.Prime).pos
  obtain ⟨a, b, rfl⟩ := (IntermediateField.mem_adjoin_range_iff κ t x).mp hx
  by_cases hb : aeval t b = 0
  · simp only [hb, div_zero]
    exact Submodule.zero_mem _
  let c : IntermediateField.adjoin κ (Set.range (fun i => t i ^ p)) :=
    ⟨aeval t b ^ p, powerResidue_denominator_pow_mem t b⟩
  have h := Submodule.smul_mem
    (Submodule.span (IntermediateField.adjoin κ (Set.range (fun i => t i ^ p)))
      (Set.range (fun r : σ → Fin p =>
        aeval t (monomial (powerResidueExponent r) (1 : κ))))) c⁻¹
    (powerResidue_aeval_mem_span hp t (a * b ^ (p - 1)))
  change (aeval t b ^ p)⁻¹ * aeval t (a * b ^ (p - 1)) ∈ _ at h
  have heq : (aeval t b ^ p)⁻¹ * aeval t (a * b ^ (p - 1)) =
      aeval t a / aeval t b := by
    rw [map_mul, map_pow]
    field_simp [hb]
    rw [mul_assoc, ← pow_succ, Nat.sub_add_cancel hp, mul_comm]
  rwa [heq] at h

-- @node: powerResidue_relfinrank_adjoin
/-- In prime characteristic p, if [the finite family t is algebraically
independent over κ](hyp:ht), then [the degree of the field generated by κ and t
over the field generated by κ and the p-th powers of t equals p raised to the
number of members of t](goal). -/
lemma powerResidue_relfinrank_adjoin {p : ℕ} [Fact p.Prime] [CharP κ p]
    (t : σ → F) (ht : AlgebraicIndependent κ t) :
    Subfield.relfinrank
      (IntermediateField.adjoin κ (Set.range (fun i => t i ^ p))).toSubfield
      (IntermediateField.adjoin κ (Set.range t)).toSubfield = p ^ Fintype.card σ := by
  classical
  let B := IntermediateField.adjoin κ (Set.range (fun i => t i ^ p))
  let K := IntermediateField.adjoin κ (Set.range t)
  have hBK : B.toSubfield ≤ K.toSubfield := by
    apply IntermediateField.adjoin_le_iff.mpr
    rintro _ ⟨i, rfl⟩
    exact K.toSubfield.pow_mem (IntermediateField.subset_adjoin κ _ ⟨i, rfl⟩) p
  let E := Subfield.extendScalars hBK
  have hspan : Submodule.span B
      (Set.range (fun r : σ → Fin p =>
        aeval t (monomial (powerResidueExponent r) (1 : κ)))) =
      E.toSubalgebra.toSubmodule := by
    apply le_antisymm
    · apply Submodule.span_le.mpr
      rintro _ ⟨r, rfl⟩
      exact powerResidue_aeval_mem_adjoin t _
    · intro x hx
      exact powerResidue_rational_mem_span t hx
  rw [Subfield.relfinrank_eq_finrank_of_le hBK]
  change Module.finrank B E.toSubalgebra.toSubmodule = _
  rw [← hspan, finrank_span_eq_card
    (powerResidue_linearIndependent_intermediateField (Fact.out : p.Prime).pos t ht),
    powerResidue_card]

end Papers.OaiReconstructionMilnorTheory