module

public import Papers.OaiReconstructionMilnorTheory.Basic
public import Mathlib.FieldTheory.Relrank
public import Mathlib.Algebra.CharP.Frobenius

/-! # Frobenius transport and cancellation in the power-degree towers -/

public section

namespace Papers.OaiReconstructionMilnorTheory

variable (p : ℕ) (F : Type*) [Field F] [Fact p.Prime] [CharP F p]

-- @node: powSubfield_eq_frobenius_fieldRange
/-- In prime characteristic p, [the subfield generated by p-th powers in F equals
the image of the p-th-power map on F](goal). -/
lemma powSubfield_eq_frobenius_fieldRange :
    powSubfield p F = (frobenius F p).fieldRange := by
  apply le_antisymm
  · exact Subfield.closure_le.2 (fun _ ⟨x, hx⟩ => ⟨x, hx⟩)
  · rintro _ ⟨x, rfl⟩
    exact Subfield.subset_closure ⟨x, rfl⟩

-- @node: frobenius_map_top_eq_powSubfield
/-- In prime characteristic p, [the image of the whole field F under the
p-th-power map equals its subfield generated by p-th powers](goal). -/
lemma frobenius_map_top_eq_powSubfield :
    (⊤ : Subfield F).map (frobenius F p) = powSubfield p F := by
  rw [powSubfield_eq_frobenius_fieldRange, RingHom.fieldRange_eq_map]

-- @node: frobenius_subfield_le_self
/-- In prime characteristic p, [the p-th-power image of every subfield K of F is
contained in K](goal). -/
lemma frobenius_subfield_le_self (K : Subfield F) :
    K.map (frobenius F p) ≤ K := by
  rintro _ ⟨x, hx, rfl⟩
  exact K.pow_mem hx p

-- @node: frobenius_subfield_extension_degree
/-- In prime characteristic p, [the degree of the p-th-power subfield of F over
the p-th-power image of K equals the degree of F over K](goal).

Degrees here are vector-space dimensions recorded as natural numbers, with zero
representing infinite dimension. -/
lemma frobenius_subfield_extension_degree (K : Subfield F) :
    Subfield.relfinrank (K.map (frobenius F p)) (powSubfield p F) =
      Module.finrank K F := by
  rw [← frobenius_map_top_eq_powSubfield]
  exact (Subfield.relfinrank_map_map K ⊤ (frobenius F p)).trans
    (Subfield.relfinrank_top_right K)

-- @node: power_degree_eq_of_finite_extension
/-- For a finite extension F of K in prime characteristic p, [the degree of F
over its p-th-power subfield equals the degree of K over its own p-th-power
image, viewed inside F](goal).

Degrees are recorded as natural numbers, with zero representing infinite dimension. -/
lemma power_degree_eq_of_finite_extension (K : Subfield F) [FiniteDimensional K F] :
    Module.finrank ↥(powSubfield p F) F =
      Subfield.relfinrank (K.map (frobenius F p)) K := by
  have hK := frobenius_subfield_le_self p F K
  have hC : K.map (frobenius F p) ≤ powSubfield p F := by
    rw [← frobenius_map_top_eq_powSubfield]
    rintro _ ⟨x, _, rfl⟩
    exact ⟨x, trivial, rfl⟩
  have h₁ := Subfield.relfinrank_mul_finrank_top hK
  have h₂ := Subfield.relfinrank_mul_finrank_top hC
  rw [frobenius_subfield_extension_degree] at h₂
  apply Nat.eq_of_mul_eq_mul_left (Module.finrank_pos (R := K) (M := F))
  calc
    Module.finrank K F * Module.finrank ↥(powSubfield p F) F =
        Module.finrank ↥(K.map (frobenius F p)) F := h₂
    _ = Module.finrank K F * Subfield.relfinrank (K.map (frobenius F p)) K := by
      rw [mul_comm]
      exact h₁.symm

end Papers.OaiReconstructionMilnorTheory