FinrankAlong_eq_and_trace_eq_of_constantFieldExtension.lean

theorem exists_finset_adjoin_eq_top
    (hfg : ∃ x : F', Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F') :
    ∃ G : Finset F', IntermediateField.adjoin K (G : Set F') = ⊤

theorem finiteAlong_of_isIntegral_of_adjoin_eq_top (φ : F →ₐ[K] F')
    (hφ : φ.toRingHom.IsIntegral) (T : Finset F')
    (hT : IntermediateField.adjoin K (T : Set F') = ⊤) : FiniteAlong K φ

theorem finiteAlong_of_hfg (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (hfg : ∃ x : F', Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F')) F') : FiniteAlong K φ

def spanEF : Submodule E FE

theorem mul_mem_spanEF {a b : FE} (ha : a ∈ spanEF F E FE) (hb : b ∈ spanEF F E FE) :
    a * b ∈ spanEF F E FE

theorem one_mem_spanEF : (1 : FE) ∈ spanEF F E FE

theorem algebraMap_E_mem_spanEF (e : E) : algebraMap E FE e ∈ spanEF F E FE

theorem prod_mem_spanEF {ι : Type*} (s : Finset ι) (q : ι → FE) (hq : ∀ i ∈ s, q i ∈ spanEF F E FE)
  :
    ∏ i ∈ s, q i ∈ spanEF F E FE

def spanEFRing : Subring FE where
  carrier := spanEF F E FE
  mul_mem' ha hb := mul_mem_spanEF ha hb
  one_mem' := one_mem_spanEF
  add_mem' ha hb := Submodule.add_mem _ ha hb
  zero_mem' := Submodule.zero_mem _
  neg_mem' ha := Submodule.neg_mem _ ha

theorem exists_div_of_adjoin_eq_top
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤) (z : FE) :
    ∃ p q : FE, p ∈ spanEF F E FE ∧ q ∈ spanEF F E FE ∧ q ≠ 0 ∧ z = p / q

theorem exists_linearIndependent_repr {d : ℕ} (c : Fin d → FE) (hc : ∀ j, c j ∈ spanEF F E FE) :
    ∃ (r : ℕ) (u : Fin r → F), LinearIndependent K u ∧
      ∀ j, ∃ e : Fin r → E, c j = ∑ m, e m • algebraMap F FE (u m)

theorem linearIndependent_along_baseChange
    (φ : F →ₐ[K] F') (φE : FE →ₐ[E] F'E)
    (hφcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (hli : ∀ {ι : Type} [Fintype ι] (g : ι → F'), LinearIndependent K g →
      LinearIndependent E (fun i => algebraMap F' F'E (g i)))
    {d : ℕ} (b : Fin d → F') (hb : letI := algebraAlong φ; LinearIndependent F b) :
    letI := algebraAlong φE
    LinearIndependent FE (fun j => algebraMap F' F'E (b j)) := by
  classical
  let : Algebra F F' := algebraAlong φ
  let : Algebra FE F'E := algebraAlong φE
  have hsmulF : ∀ (s : F) (y : F'), s • y = φ s * y := fun s y => rfl
  have hsmulFE : ∀ (s : FE) (y : F'E), s • y = φE s * y := fun s y => rfl
  have hcore : ∀ c : Fin d → FE, (∀ j, c j ∈ spanEF F E FE) →
      ∑ j, c j • algebraMap F' F'E (b j) = 0 → ∀ j, c j = 0 := by
    intro c hc hrel
    obtain ⟨r, u, hu, he⟩ := exists_linearIndependent_repr (K := K) c hc
    choose e he using he
    have hG : LinearIndependent K (fun mj : Fin r × Fin d => φ (u mj.1) * b mj.2) := by
      rw [Fintype.linearIndependent_iff]
      intro a ha
      have hsum : ∑ j, (∑ m, a (m, j) • u m) • b j = 0 := by
        have : ∑ mj : Fin r × Fin d, a mj • (φ (u mj.1) * b mj.2) =
            ∑ j, (∑ m, a (m, j) • u m) • b j := by
          rw [Fintype.sum_prod_type, Finset.sum_comm]
          refine Finset.sum_congr rfl fun j _ => ?_
          rw [hsmulF, map_sum, Finset.sum_mul]
          refine Finset.sum_congr rfl fun m _ => ?_
          rw [map_smul, Algebra.smul_def, Algebra.smul_def, mul_assoc]
        rw [← this]; exact ha
      have h1 := Fintype.linearIndependent_iff.1 hb (fun j => ∑ m, a (m, j) • u m) hsum
      intro mj
      have h2 := Fintype.linearIndependent_iff.1 hu (fun m => a (m, mj.2)) (h1 mj.2) mj.1
      exact h2
    have hG' := hli _ hG
    have hrel' : ∑ mj : Fin r × Fin d,
        e mj.2 mj.1 • algebraMap F' F'E (φ (u mj.1) * b mj.2) = 0 := by
      have : ∑ mj : Fin r × Fin d, e mj.2 mj.1 • algebraMap F' F'E (φ (u mj.1) * b mj.2) =
          ∑ j, c j • algebraMap F' F'E (b j) := by
        rw [Fintype.sum_prod_type, Finset.sum_comm]
        refine Finset.sum_congr rfl fun j _ => ?_
        rw [hsmulFE, he j, map_sum, Finset.sum_mul]
        refine Finset.sum_congr rfl fun m _ => ?_
        rw [map_smul, hφcomm, map_mul, Algebra.smul_def, Algebra.smul_def, mul_assoc]
      rw [this]; exact hrel
    have h0 := Fintype.linearIndependent_iff.1 hG' (fun mj => e mj.2 mj.1) hrel'
    intro j
    rw [he j]
    refine Finset.sum_eq_zero fun m _ => ?_
    have h0' : e j m = 0 := h0 (m, j)
    rw [h0', zero_smul]
  rw [Fintype.linearIndependent_iff]
  intro c hrel
  choose p q hp hq hq0 hcpq using fun j => exists_div_of_adjoin_eq_top hgen (c j)
  set Q : FE := ∏ j, q j with hQ
  have hQ0 : Q ≠ 0 := Finset.prod_ne_zero_iff.2 fun j _ => hq0 j
  have hc' : ∀ j, c j * Q ∈ spanEF F E FE := by
    intro j
    have : c j * Q = p j * ∏ k ∈ Finset.univ.erase j, q k := by
      have hqj : q j ≠ 0 := hq0 j
      rw [hcpq j, hQ, ← Finset.prod_erase_mul Finset.univ q (Finset.mem_univ j)]
      field_simp
    rw [this]
    exact mul_mem_spanEF (hp j) (prod_mem_spanEF _ q fun k _ => hq k)
  have hrel' : ∑ j, (c j * Q) • algebraMap F' F'E (b j) = 0 := by
    have : ∑ j, (c j * Q) • algebraMap F' F'E (b j) = φE Q * ∑ j, c j • algebraMap F' F'E (b j) :=
      by
      rw [Finset.mul_sum]
      refine Finset.sum_congr rfl fun j _ => ?_
      rw [hsmulFE, hsmulFE, map_mul]; ring
    rw [this, hrel, mul_zero]
  intro j
  have := hcore (fun j => c j * Q) hc' hrel' j
  exact (mul_eq_zero.1 this).resolve_right hQ0

theorem _root_.AlgebraicCurve.finrankAlong_eq_and_trace_eq_of_constantFieldExtension
    (K F : Type*) [Field K] [Field F] [Algebra K F] [IsAlgClosed K] [CharZero K] [IsCurveOver K F]
    (_hfg : ∃ x : F, Transcendental K x ∧
      FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F)
    (F' : Type*) [Field F'] [Algebra K F'] [IsCurveOver K F']
    (hfg' : ∃ x' : F', Transcendental K x' ∧
      FiniteDimensional (IntermediateField.adjoin K ({x'} : Set F')) F')
    (φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral)
    (E FE : Type*) [Field E] [Field FE] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
    [IsScalarTower K E FE] [IsScalarTower K F FE] [IsAlgClosed E] [IsCurveOver E FE]
    (_hfgE : ∃ x : FE, Transcendental E x ∧
      FiniteDimensional (IntermediateField.adjoin E ({x} : Set FE)) FE)
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤)
    (F'E : Type*) [Field F'E] [Algebra E F'E] [Algebra F' F'E] [Algebra K F'E]
    [IsScalarTower K E F'E] [IsScalarTower K F' F'E] [IsCurveOver E F'E]
    (hfgE' : ∃ x' : F'E, Transcendental E x' ∧
      FiniteDimensional (IntermediateField.adjoin E ({x'} : Set F'E)) F'E)
    (hgen' : IntermediateField.adjoin E (Set.range (algebraMap F' F'E)) = ⊤)
    (φE : FE →ₐ[E] F'E)
    (hφcomm : ∀ f : F, φE (algebraMap F FE f) = algebraMap F' F'E (φ f))
    (hφE : φE.toRingHom.IsIntegral) :
    FiniteAlong K φ ∧ FiniteAlong E φE ∧ finrankAlong E φE = finrankAlong K φ ∧
    ∀ u : F',
      (letI := algebraAlong φE; Algebra.trace FE F'E (algebraMap F' F'E u)) =
        algebraMap F FE (letI := algebraAlong φ; Algebra.trace F F' u) := by
  classical
  have hfinφ : FiniteAlong K φ := finiteAlong_of_hfg φ hφ hfg'
  have hfinφE : FiniteAlong E φE := finiteAlong_of_hfg φE hφE hfgE'
  let : Algebra F F' := algebraAlong φ
  have : IsScalarTower K F F' := isScalarTower_along φ
  have : Module.Finite F F' := hfinφ
  let : Algebra FE F'E := algebraAlong φE
  have : IsScalarTower E FE F'E := isScalarTower_along φE
  have : Module.Finite FE F'E := hfinφE
  have hsmulFE : ∀ (s : FE) (y : F'E), s • y = φE s * y := fun s y => rfl
  set b := Module.finBasis F F' with hb
  set d := Module.finrank F F' with hd
  have hli : LinearIndependent FE (fun j => algebraMap F' F'E (b j)) := by
    refine linearIndependent_along_baseChange (K := K) φ φE hφcomm hgen ?_ b b.linearIndependent
    intro ι _ g hg
    exact AlgebraicCurve.linearIndependent_of_constantFieldExtension K F' E F'E hfg' hfgE' hgen' hg
  have hspan : ⊤ ≤ Submodule.span FE (Set.range fun j => algebraMap F' F'E (b j)) := by
    have hF' : ∀ u : F', algebraMap F' F'E u ∈
        Submodule.span FE (Set.range fun j => algebraMap F' F'E (b j)) := by
      intro u
      have hu : u = ∑ j, b.repr u j • b j := (b.sum_repr u).symm
      rw [hu, map_sum]
      refine Submodule.sum_mem _ fun j _ => ?_
      have : algebraMap F' F'E (b.repr u j • b j) =
          (algebraMap F FE (b.repr u j)) • algebraMap F' F'E (b j) := by
        rw [hsmulFE, hφcomm, Algebra.smul_def, map_mul]; rfl
      rw [this]
      exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨j, rfl⟩)
    have : Algebra.IsIntegral FE F'E := ⟨fun z => hφE z⟩
    have : Algebra.IsAlgebraic FE F'E := Algebra.IsIntegral.isAlgebraic
    set A : Subalgebra FE F'E := Algebra.adjoin FE (Set.range (algebraMap F' F'E)) with hA
    have hAfield : IsField A := Subalgebra.isField_of_algebraic A
    have hAinv : ∀ z ∈ A, z⁻¹ ∈ A := by
      intro z hz
      by_cases hz0 : z = 0
      · rw [hz0, inv_zero]; exact A.zero_mem
      · obtain ⟨w, hw⟩ := hAfield.mul_inv_cancel (a := ⟨z, hz⟩) (fun h => hz0 (congrArg Subtype.val
          h))
        have hw' : z * (w : F'E) = 1 := congrArg Subtype.val hw
        have : (w : F'E) = z⁻¹ :=
          (mul_eq_one_iff_eq_inv₀ hz0).1 (by rw [mul_comm]; exact hw')
        rw [← this]; exact w.2
    set A' : IntermediateField E F'E := (A.restrictScalars E).toIntermediateField
      (fun z hz => hAinv z hz) with hA'
    have hA'top : (⊤ : IntermediateField E F'E) ≤ A' := by
      rw [← hgen', IntermediateField.adjoin_le_iff]
      rintro _ ⟨u, rfl⟩
      change algebraMap F' F'E u ∈ A
      exact Algebra.subset_adjoin ⟨u, rfl⟩
    have hAtop : ∀ z : F'E, z ∈ A := fun z => hA'top (IntermediateField.mem_top (x := z))
    intro z _
    have hz : z ∈ Subalgebra.toSubmodule A := hAtop z
    rw [hA, Algebra.adjoin_eq_span] at hz
    have hclos : (Submonoid.closure (Set.range (algebraMap F' F'E)) : Set F'E) ⊆
        Set.range (algebraMap F' F'E) := by
      intro y hy
      have hle : Submonoid.closure (Set.range (algebraMap F' F'E)) ≤
          MonoidHom.mrange ((algebraMap F' F'E : F' →+* F'E) : F' →* F'E) :=
        Submonoid.closure_le.2 (by rintro _ ⟨u, rfl⟩; exact ⟨u, rfl⟩)
      obtain ⟨u, hu⟩ := hle hy
      exact ⟨u, hu⟩
    refine (Submodule.span_le.2 ?_) (Submodule.span_mono hclos hz)
    rintro _ ⟨u, rfl⟩
    exact hF' u
  set bE : Module.Basis (Fin d) FE F'E := Module.Basis.mk hli hspan with hbE
  have hbE_apply : ∀ j, bE j = algebraMap F' F'E (b j) := fun j => by
    rw [hbE, Module.Basis.mk_apply]
  have hdeg : finrankAlong E φE = finrankAlong K φ := by
    change Module.finrank FE F'E = Module.finrank F F'
    rw [Module.finrank_eq_card_basis bE, Fintype.card_fin]
  refine ⟨hfinφ, hfinφE, hdeg, fun u => ?_⟩
  change Algebra.trace FE F'E (algebraMap F' F'E u) = algebraMap F FE (Algebra.trace F F' u)
  rw [Algebra.trace_eq_matrix_trace bE, Algebra.trace_eq_matrix_trace b, Matrix.trace, Matrix.trace,
    map_sum]
  refine Finset.sum_congr rfl fun i _ => ?_
  rw [Matrix.diag_apply, Matrix.diag_apply, Algebra.leftMulMatrix_eq_repr_mul,
    Algebra.leftMulMatrix_eq_repr_mul]
  have hexp : algebraMap F' F'E u * bE i =
      ∑ k, algebraMap F FE (b.repr (u * b i) k) • bE k := by
    rw [hbE_apply, ← map_mul]
    conv_lhs => rw [← b.sum_repr (u * b i)]
    rw [map_sum]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [hbE_apply, hsmulFE, hφcomm, Algebra.smul_def, map_mul]
    rfl
  rw [hexp, Module.Basis.repr_sum_self]