LinearIndependent_of_constantFieldExtension_of_isAlgClosed.lean

def genericPoly (d N : ℕ) (v : Fin d → Fin N → R) : R[X][X]

theorem genericPoly_map (d N : ℕ) (v : Fin d → Fin N → R) (φ : R →+* S) :
    (genericPoly d N v).map (mapRingHom φ) = genericPoly d N (fun j n => φ (v j n)) := by
  simp [genericPoly, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow]

theorem genericPoly_monic [Nontrivial R] (d N : ℕ) (v : Fin d → Fin N → R) :
    (genericPoly d N v).Monic

theorem genericPoly_natDegree [Nontrivial R] (d N : ℕ) (v : Fin d → Fin N → R) :
    (genericPoly d N v).natDegree = d

theorem genericPoly_coeff_eq (g : R[X][X]) (hg : g.Monic) (N : ℕ)
    (hN : ∀ j : ℕ, j < g.natDegree → (g.coeff j).natDegree < N) :
    genericPoly g.natDegree N (fun j n => (g.coeff j).coeff n) = g := by
  have inner : ∀ j : Fin g.natDegree,
      (∑ n : Fin N, C ((g.coeff j).coeff n) * X ^ (n : ℕ)) = g.coeff j := by
    intro j
    rw [Fin.sum_univ_eq_sum_range (fun n => C ((g.coeff (j : ℕ)).coeff n) * X ^ n) N]
    exact (as_sum_range_C_mul_X_pow' _ (hN j j.2)).symm
  unfold genericPoly
  simp_rw [inner]
  rw [Fin.sum_univ_eq_sum_range (fun j => C (g.coeff j) * X ^ j) g.natDegree]
  exact hg.as_sum.symm

theorem exists_factorisation_of_factorisation_map (m : K[X][X])
    (g h : K'[X][X]) (hg : g.Monic) (hh : h.Monic)
    (hfac : m.map (mapRingHom (algebraMap K K')) = g * h) :
    ∃ g₀ h₀ : K[X][X], g₀.Monic ∧ h₀.Monic ∧ g₀.natDegree = g.natDegree ∧
      h₀.natDegree = h.natDegree ∧ m = g₀ * h₀

theorem irreducible_map_of_isAlgClosed (m : K[X][X]) (hm : m.Monic) (hirr : Irreducible m) :
    Irreducible (m.map (mapRingHom (algebraMap K K')))

theorem algebraMap_comp_aeval_gen (x : F) :
    (algebraMap K⟮x⟯ F).comp (aeval (AdjoinSimple.gen K x) : K[X] →ₐ[K] K⟮x⟯).toRingHom =
      (aeval x : K[X] →ₐ[K] F).toRingHom

theorem aeval_gen_injective {x : F} (hx : Transcendental K x) :
    Function.Injective (aeval (AdjoinSimple.gen K x) : K[X] →ₐ[K] K⟮x⟯)

theorem exists_common_denom {x : F} (hx : Transcendental K x) {T : Type*} [Finite T]
    (r : T → K⟮x⟯) : ∃ q : K[X], q ≠ 0 ∧ ∀ t, ∃ p : K[X],
      aeval (AdjoinSimple.gen K x) q * r t = aeval (AdjoinSimple.gen K x) p

theorem exists_primitive_integral {x : F} (hx : Transcendental K x)
    [FiniteDimensional K⟮x⟯ F] [Algebra.IsSeparable K⟮x⟯ F] :
    ∃ (y : F) (m : K[X][X]) (d : ℕ), m.Monic ∧ Irreducible m ∧ m.natDegree = d ∧
      m.eval₂ (aeval x : K[X] →ₐ[K] F).toRingHom y = 0 ∧
      ∀ f : F, ∃ r : Fin d → K⟮x⟯, f = ∑ j, algebraMap K⟮x⟯ F (r j) * y ^ (j : ℕ)

theorem algebraMap_mem_adjoin (x : F) (z : K⟮x⟯) :
    algebraMap F F' (z : F) ∈ K'⟮algebraMap F F' x⟯

theorem exists_ringHom_adjoin (x : F) : ∃ ρ : K⟮x⟯ →+* K'⟮algebraMap F F' x⟯,
    ∀ z, algebraMap K'⟮algebraMap F F' x⟯ F' (ρ z) = algebraMap F F' (algebraMap K⟮x⟯ F z)

theorem isIntegral_algebraMap (x : F) [FiniteDimensional K⟮x⟯ F] (f : F) :
    IsIntegral K'⟮algebraMap F F' x⟯ (algebraMap F F' f)

theorem transcendental_algebraMap {x : F} [FiniteDimensional K⟮x⟯ F]
    (hfg' : ∃ x' : F', Transcendental K' x' ∧ FiniteDimensional K'⟮x'⟯ F')
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤) :
    Transcendental K' (algebraMap F F' x)

theorem linearIndependent_pow_algebraMap [IsAlgClosed K] {x : F}
    (hx₁ : Transcendental K' (algebraMap F F' x))
    {y : F} {m : K[X][X]} (hm : m.Monic) (hirr : Irreducible m)
    (hroot : m.eval₂ (aeval x : K[X] →ₐ[K] F).toRingHom y = 0) :
    LinearIndependent K'⟮algebraMap F F' x⟯
      (fun j : Fin m.natDegree => algebraMap F F' y ^ (j : ℕ)) := by
  classical
  set x₁ := algebraMap F F' x with hx₁def
  set y₁ := algebraMap F F' y with hy₁def
  let ψ : K[X] →+* K'⟮x₁⟯ :=
    (aeval (AdjoinSimple.gen K' x₁) : K'[X] →ₐ[K'] K'⟮x₁⟯).toRingHom.comp
      (mapRingHom (algebraMap K K'))
  set M : K'⟮x₁⟯[X] := m.map ψ with hM
  have hMmonic : M.Monic := hm.map ψ
  have hcomp : (algebraMap K'⟮x₁⟯ F').comp ψ = (algebraMap F F').comp (aeval x).toRingHom := by
    refine Polynomial.ringHom_ext (fun a => ?_) ?_
    · simp only [ψ, RingHom.coe_comp, Function.comp_apply, coe_mapRingHom, map_C,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_C]
      rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
        ← IsScalarTower.algebraMap_apply]
    · simp only [ψ, RingHom.coe_comp, Function.comp_apply, coe_mapRingHom, map_X,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_X]
      rfl
  have hMroot : aeval y₁ M = 0 := by
    rw [aeval_def, hM, eval₂_map, hcomp, hy₁def, ← hom_eval₂, hroot, map_zero]
  have hMirr : Irreducible M := by
    have h0 : Irreducible (m.map (mapRingHom (algebraMap K K'))) :=
      irreducible_map_of_isAlgClosed m hm hirr
    have h1 : Irreducible ((m.map (mapRingHom (algebraMap K K'))).map
        (algebraMap K'[X] (RatFunc K'))) :=
      ((hm.map _).irreducible_iff_irreducible_map_fraction_map).mp h0
    let e := RatFunc.algEquivOfTranscendental x₁ hx₁
    have h2 := h1.map (mapEquiv (e : RatFunc K' ≃+* K'⟮x₁⟯))
    have h3 : mapEquiv (e : RatFunc K' ≃+* K'⟮x₁⟯)
        ((m.map (mapRingHom (algebraMap K K'))).map (algebraMap K'[X] (RatFunc K'))) = M := by
      rw [mapEquiv_apply, Polynomial.map_map, Polynomial.map_map, hM]
      congr 1
      refine RingHom.ext fun g => ?_
      simp only [ψ, RingHom.coe_comp, Function.comp_apply, coe_mapRingHom, RingHom.coe_coe,
        AlgHom.toRingHom_eq_coe]
      exact RatFunc.algEquivOfTranscendental_algebraMap x₁ hx₁ _
    rw [h3] at h2
    exact h2
  have hMeq : M = minpoly K'⟮x₁⟯ y₁ := minpoly.eq_of_irreducible_of_monic hMirr hMroot hMmonic
  have hdeg : (minpoly K'⟮x₁⟯ y₁).natDegree = m.natDegree := by
    rw [← hMeq, hM]; exact hm.natDegree_map ψ
  have hli := linearIndependent_pow (K := K'⟮x₁⟯) y₁
  rw [hdeg] at hli
  exact hli

theorem eq_zero_of_sum_C_mul_map {κ : Type*} [Fintype κ] {c : κ → K'}
    (hc : LinearIndependent K c) (p : κ → K[X])
    (h : ∑ k, C (c k) * (p k).map (algebraMap K K') = 0) : ∀ k, p k = 0

theorem eq_zero_of_sum_aeval {x₁ : F'} (hx₁ : Transcendental K' x₁) {κ : Type*} [Fintype κ]
    {c : κ → K'} (hc : LinearIndependent K c) (p : κ → K[X])
    (h : ∑ k, algebraMap K' K'⟮x₁⟯ (c k) *
      aeval (AdjoinSimple.gen K' x₁) ((p k).map (algebraMap K K')) = 0) : ∀ k, p k = 0

theorem eq_zero_of_sum_mul_algebraMap [IsAlgClosed K] {x : F}
    (hx : Transcendental K x) [FiniteDimensional K⟮x⟯ F] [Algebra.IsSeparable K⟮x⟯ F]
    (hx₁ : Transcendental K' (algebraMap F F' x))
    {κ : Type*} [Fintype κ] {c : κ → K'} (hc : LinearIndependent K c) (f : κ → F)
    (hrel : ∑ k, algebraMap F F' (f k) * algebraMap K' F' (c k) = 0) : ∀ k, f k = 0

theorem linearIndependent_algebraMap_of_fintype [IsAlgClosed K] {x : F}
    (hx : Transcendental K x) [FiniteDimensional K⟮x⟯ F] [Algebra.IsSeparable K⟮x⟯ F]
    (hx₁ : Transcendental K' (algebraMap F F' x))
    {κ : Type*} [Finite κ] {b : κ → F} (hb : LinearIndependent K b) :
    LinearIndependent K' (fun i => algebraMap F F' (b i)) := by
  classical
  let := Fintype.ofFinite κ
  rw [Fintype.linearIndependent_iff]
  intro a hrel i₀
  let W : Submodule K K' := Submodule.span K (Set.range a)
  have : Module.Finite K W := Module.Finite.span_of_finite K (Set.finite_range a)
  let bW := Module.finBasis K W
  let c : Fin (Module.finrank K W) → K' := fun k => (bW k : K')
  have hc : LinearIndependent K c :=
    bW.linearIndependent.map' W.subtype (Submodule.ker_subtype W)
  have ha : ∀ i, a i ∈ W := fun i => Submodule.subset_span ⟨i, rfl⟩
  let μ : κ → Fin (Module.finrank K W) → K := fun i k => bW.repr ⟨a i, ha i⟩ k
  have hai : ∀ i, a i = ∑ k, μ i k • c k := by
    intro i
    have h1 := congrArg (Submodule.subtype W) (bW.sum_repr ⟨a i, ha i⟩)
    rw [map_sum] at h1
    simp only [map_smul, Submodule.subtype_apply] at h1
    exact h1.symm
  let f : Fin (Module.finrank K W) → F := fun k => ∑ i, μ i k • b i
  have hf : ∀ k, f k = 0 := by
    apply eq_zero_of_sum_mul_algebraMap hx hx₁ hc f
    have lhs : ∑ k, algebraMap F F' (f k) * algebraMap K' F' (c k) =
        ∑ k, ∑ i, algebraMap K F' (μ i k) * algebraMap F F' (b i) * algebraMap K' F' (c k) := by
      refine Finset.sum_congr rfl fun k _ => ?_
      simp only [f, map_sum, Finset.sum_mul]
      refine Finset.sum_congr rfl fun i _ => ?_
      rw [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply]
    have rhs : ∑ i, a i • algebraMap F F' (b i) =
        ∑ i, ∑ k, algebraMap K F' (μ i k) * algebraMap F F' (b i) * algebraMap K' F' (c k) := by
      refine Finset.sum_congr rfl fun i _ => ?_
      rw [hai i, Algebra.smul_def, map_sum, Finset.sum_mul]
      refine Finset.sum_congr rfl fun k _ => ?_
      rw [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply]
      ring
    rw [lhs, Finset.sum_comm, ← rhs, hrel]
  have hμ : ∀ k i, μ i k = 0 := fun k =>
    Fintype.linearIndependent_iff.mp hb (fun i => μ i k) (hf k)
  rw [hai i₀]
  simp [hμ]

theorem _root_.AlgebraicCurve.linearIndependent_of_constantFieldExtension_of_isAlgClosed (K F K' F'
  : Type*)
    [Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
    [Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
    [IsAlgClosed K]
    (hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      F)) F)
    (hfg' : ∃ x : F', Transcendental K' x ∧
      FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
    (hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
    {ι : Type*} {b : ι → F} (hb : LinearIndependent K b) :
    LinearIndependent K' (fun i => algebraMap F F' (b i)) := by
  obtain ⟨x₀, hx₀, hfin₀⟩ := hfg
  obtain ⟨x, hx, hfin, hsep⟩ :=
    AlgebraicCurve.exists_separating_transcendental_of_perfectField hx₀ hfin₀
  have := hfin
  have := hsep
  have hx₁ : Transcendental K' (algebraMap F F' x) :=
    transcendental_algebraMap (K := K) (x := x) hfg' hgen
  rw [linearIndependent_iff_finset_linearIndependent]
  intro s
  exact linearIndependent_algebraMap_of_fintype hx hx₁ (hb.comp ((↑) : s → ι) Subtype.val_injective)