module

public import Papers.OaiReconstructionMilnorTheory.Basic
public import Papers.OaiReconstructionMilnorTheory.Helpers.PDegreeFrobenius
public import Papers.OaiReconstructionMilnorTheory.Helpers.PDegreeRational
public import Mathlib.FieldTheory.SeparablyGenerated
public import Mathlib.FieldTheory.FinTrdeg
public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
public import Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra

/-! # Degree over the power subfield -/

public section

namespace Papers.OaiReconstructionMilnorTheory

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

-- @node: geometricField_constant_power_root
/-- If [κ is algebraically closed and F is a finitely generated extension of κ of
characteristic p](hyp:hF) and [n is positive](hyp:hn), then [every constant a from κ
has an n-th root in κ whose image in F has n-th power equal to the image of a](goal). -/
lemma geometricField_constant_power_root (hF : GeometricField p κ F)
    (a : κ) {n : ℕ} (hn : 0 < n) :
    ∃ b : κ, (algebraMap κ F b) ^ n = algebraMap κ F a := by
  let : IsAlgClosed κ := hF.1
  obtain ⟨b, hb⟩ := IsAlgClosed.exists_pow_nat_eq a hn
  exact ⟨b, by rw [← map_pow, hb]⟩

-- @node: geometricField_constant_mem_powSubfield
/-- If [p is prime](hyp:hp) and [κ is algebraically closed and F is a finitely
generated extension of κ of characteristic p](hyp:hF), then [the image in F of
every constant a from κ belongs to the subfield generated by p-th powers](goal). -/
lemma geometricField_constant_mem_powSubfield (hp : PrimeChar p)
    (hF : GeometricField p κ F) (a : κ) :
    algebraMap κ F a ∈ powSubfield p F := by
  obtain ⟨b, hb⟩ := geometricField_constant_power_root p κ F hF a hp.pos
  exact Subfield.subset_closure ⟨algebraMap κ F b, hb⟩

-- @node: geometricField_frobenius_adjoin
/-- If [κ is algebraically closed and F is a finitely generated extension of κ of
characteristic p](hyp:hF), then [the p-th-power image of the field generated by κ
and a set s equals the field generated by κ and the p-th powers of elements of s](goal). -/
lemma geometricField_frobenius_adjoin [Fact p.Prime] [CharP F p]
    (hF : GeometricField p κ F) (s : Set F) :
    (IntermediateField.adjoin κ s).toSubfield.map (frobenius F p) =
      (IntermediateField.adjoin κ ((fun x : F => x ^ p) '' s)).toSubfield := by
  have hconstants : (frobenius F p) '' Set.range (algebraMap κ F) =
      Set.range (algebraMap κ F) := by
    ext x
    constructor
    · rintro ⟨_, ⟨a, rfl⟩, rfl⟩
      exact ⟨a ^ p, map_pow (algebraMap κ F) a p⟩
    · rintro ⟨a, rfl⟩
      obtain ⟨b, hb⟩ := geometricField_constant_power_root p κ F hF a
        (Fact.out : p.Prime).pos
      exact ⟨algebraMap κ F b, ⟨b, rfl⟩, hb⟩
  rw [IntermediateField.adjoin_toSubfield, RingHom.map_field_closure,
    Set.image_union, hconstants, IntermediateField.adjoin_toSubfield]
  rfl

-- @node: geometricField_finiteDimensional_powSubfield
/-- If [p is prime](hyp:hp) and [κ is algebraically closed and F is a finitely
generated extension of κ of characteristic p](hyp:hF), then [F has finite dimension
over its subfield generated by p-th powers](goal). -/
lemma geometricField_finiteDimensional_powSubfield (hp : PrimeChar p)
    (hF : GeometricField p κ F) : FiniteDimensional ↥(powSubfield p F) F := by
  let C : IntermediateField κ F :=
    { powSubfield p F with
      algebraMap_mem' := geometricField_constant_mem_powSubfield p κ F hp hF }
  let : Algebra.EssFiniteType κ F := IntermediateField.fg_top_iff.mp hF.2.2
  let : Algebra.EssFiniteType C F := Algebra.EssFiniteType.of_comp κ C F
  let : Algebra.IsAlgebraic C F := ⟨fun s => by
    have hsp : s ^ p ∈ C := Subfield.subset_closure ⟨s, rfl⟩
    apply IsIntegral.isAlgebraic
    refine ⟨Polynomial.X ^ p - Polynomial.C (⟨s ^ p, hsp⟩ : C),
      Polynomial.monic_X_pow_sub_C _ hp.ne_zero, ?_⟩
    simp⟩
  exact Algebra.finite_of_essFiniteType_of_isAlgebraic (F := C) (E := F)

-- @node: geometricField_finiteDimensional_transcendenceBasis
/-- If [κ is algebraically closed and F is a finitely generated extension of κ of
characteristic p](hyp:hF) and [the finite set s is a transcendence basis of F over
κ](hyp:hs), then [F has finite dimension over the field generated by κ and s](goal). -/
lemma geometricField_finiteDimensional_transcendenceBasis (hF : GeometricField p κ F)
    (s : Finset F) (hs : IsTranscendenceBasis κ ((↑) : s → F)) :
    FiniteDimensional ↥(IntermediateField.adjoin κ (s : Set F)) F := by
  let K := IntermediateField.adjoin κ (s : Set F)
  let : Algebra.EssFiniteType κ F := IntermediateField.fg_top_iff.mp hF.2.2
  let : Algebra.EssFiniteType K F := Algebra.EssFiniteType.of_comp κ K F
  let : Algebra.IsAlgebraic K F := by
    have hr : Set.range ((↑) : s → F) = (s : Set F) := by
      ext x
      exact ⟨fun ⟨a, ha⟩ => ha ▸ a.property, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩
    have halg := hs.isAlgebraic_field
    rw [hr] at halg
    exact halg
  exact Algebra.finite_of_essFiniteType_of_isAlgebraic (F := K) (E := F)

-- @node: geometricField_exists_finite_transcendenceBasis
/-- If [κ is algebraically closed and F is a finitely generated extension of κ of
characteristic p](hyp:hF), then [F has a finite transcendence basis over κ whose
size equals the transcendence degree of F over κ](goal). -/
lemma geometricField_exists_finite_transcendenceBasis (hF : GeometricField p κ F) :
    ∃ s : Finset F, IsTranscendenceBasis κ ((↑) : s → F) ∧
      s.card = (Algebra.trdeg κ F).toNat := by
  let : Algebra.EssFiniteType κ F := IntermediateField.fg_top_iff.mp hF.2.2
  obtain ⟨s, hs⟩ := exists_finset_isTranscendenceBasis κ F
  refine ⟨s, hs, ?_⟩
  simpa using congrArg Cardinal.toNat hs.cardinalMk_eq_trdeg

-- @node: lem:p-degree
/-- If [p is prime](hyp:hp) and [κ is algebraically closed and F is a finitely
generated extension of κ of characteristic p](hyp:hF), then [F has finite dimension
over its subfield generated by p-th powers, and that dimension is p raised to the
transcendence degree of F over κ](goal). -/
lemma finrank_powSubfield_eq_pow_trdeg (hp : PrimeChar p) (hF : GeometricField p κ F) :
    FiniteDimensional ↥(powerDegreeSetup p κ F).1 F ∧
    Module.finrank ↥(powerDegreeSetup p κ F).1 F = p ^ (powerDegreeSetup p κ F).2 := by
  refine ⟨geometricField_finiteDimensional_powSubfield p κ F hp hF, ?_⟩
  let : Fact p.Prime := ⟨hp⟩
  let : CharP F p := hF.2.1
  let : CharP κ p := (algebraMap κ F).charP (algebraMap κ F).injective p
  classical
  obtain ⟨s, hs, hcard⟩ := geometricField_exists_finite_transcendenceBasis p κ F hF
  let K := IntermediateField.adjoin κ (s : Set F)
  let : FiniteDimensional K F :=
    geometricField_finiteDimensional_transcendenceBasis p κ F hF s hs
  have hmonomials : Subfield.relfinrank (K.toSubfield.map (frobenius F p)) K.toSubfield =
      p ^ s.card := by
    change Subfield.relfinrank
      ((IntermediateField.adjoin κ (s : Set F)).toSubfield.map (frobenius F p))
      (IntermediateField.adjoin κ (s : Set F)).toSubfield = p ^ s.card
    rw [geometricField_frobenius_adjoin p κ F hF]
    have himage : (fun x : F => x ^ p) '' (s : Set F) =
        Set.range (fun i : s => (i : F) ^ p) := by
      ext x
      exact ⟨fun ⟨a, ha, hx⟩ => ⟨⟨a, ha⟩, hx⟩,
        fun ⟨a, hx⟩ => ⟨a, a.property, hx⟩⟩
    have hrange : Set.range ((↑) : s → F) = (s : Set F) := by
      ext x
      exact ⟨fun ⟨a, ha⟩ => ha ▸ a.property, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩
    rw [himage]
    simpa only [hrange, Fintype.card_coe] using
      powerResidue_relfinrank_adjoin ((↑) : s → F) hs.1
  change Module.finrank ↥(powSubfield p F) F = p ^ (Algebra.trdeg κ F).toNat
  rw [power_degree_eq_of_finite_extension p F K.toSubfield, hmonomials, hcard]

end Papers.OaiReconstructionMilnorTheory