Place_exists_gram_denominator_of_mulTable.lean

theorem mwALGM_exists_mulMatrix_chi {j : F} (hj : Transcendental k j)
    (n : ℕ) (b : Fin n → F)
    (hbsp : ∀ x : F, ∃ (q : Polynomial k) (c : Fin n → Polynomial k), q ≠ 0 ∧
      x * Polynomial.aeval j q = ∑ i : Fin n, Polynomial.aeval j (c i) * b i)
    (d : Polynomial K₀) (hd : d ≠ 0) (A : Fin n → Matrix (Fin n) (Fin n) (Polynomial K₀))
    (hmul : ∀ i i' : Fin n, b i * b i' * Polynomial.aeval j (d.map (algebraMap K₀ k))
      = ∑ i'' : Fin n, Polynomial.aeval j ((A i i'' i').map (algebraMap K₀ k)) * b i'')
    (c₀ : Polynomial K₀) (cc : Fin n → Polynomial K₀) :
    ∃ (M : Matrix (Fin n) (Fin n) (Polynomial K₀)) (χ : Polynomial (Polynomial K₀)),
      χ.Monic ∧
      (∀ (m : ℕ) (i : Fin n),
        (Polynomial.aeval j (c₀.map (algebraMap K₀ k))
            + ∑ i' : Fin n, Polynomial.aeval j ((cc i' * d).map (algebraMap K₀ k)) * b i') ^ m
          * (Polynomial.aeval j (d.map (algebraMap K₀ k)) * b i)
        = ∑ i' : Fin n, Polynomial.aeval j (((M ^ m) i' i).map (algebraMap K₀ k))
            * (Polynomial.aeval j (d.map (algebraMap K₀ k)) * b i')) ∧
      Polynomial.eval₂
        ((Polynomial.aeval j).toRingHom.comp (Polynomial.mapRingHom (algebraMap K₀ k)))
        (Polynomial.aeval j (c₀.map (algebraMap K₀ k))
          + ∑ i' : Fin n, Polynomial.aeval j ((cc i' * d).map (algebraMap K₀ k)) * b i') χ
      = 0

theorem mwALGM_isIntegral_form {j : F} (hj : Transcendental k j)
    (n : ℕ) (b : Fin n → F)
    (hbsp : ∀ x : F, ∃ (q : Polynomial k) (c : Fin n → Polynomial k), q ≠ 0 ∧
      x * Polynomial.aeval j q = ∑ i : Fin n, Polynomial.aeval j (c i) * b i)
    (d : Polynomial K₀) (hd : d ≠ 0) (A : Fin n → Matrix (Fin n) (Fin n) (Polynomial K₀))
    (hmul : ∀ i i' : Fin n, b i * b i' * Polynomial.aeval j (d.map (algebraMap K₀ k))
      = ∑ i'' : Fin n, Polynomial.aeval j ((A i i'' i').map (algebraMap K₀ k)) * b i'')
    (c₀ : Polynomial K₀) (cc : Fin n → Polynomial K₀) :
    IsIntegral (Algebra.adjoin k ({j} : Set F))
      (Polynomial.aeval j (c₀.map (algebraMap K₀ k))
        + ∑ i' : Fin n, Polynomial.aeval j ((cc i' * d).map (algebraMap K₀ k)) * b i')

theorem mwALGM_isIntegral_j {j : F} :
    IsIntegral (Algebra.adjoin k ({j} : Set F)) j

theorem mwALGM_isIntegral_db {j : F} (hj : Transcendental k j)
    (n : ℕ) (b : Fin n → F)
    (hbsp : ∀ x : F, ∃ (q : Polynomial k) (c : Fin n → Polynomial k), q ≠ 0 ∧
      x * Polynomial.aeval j q = ∑ i : Fin n, Polynomial.aeval j (c i) * b i)
    (d : Polynomial K₀) (hd : d ≠ 0) (A : Fin n → Matrix (Fin n) (Fin n) (Polynomial K₀))
    (hmul : ∀ i i' : Fin n, b i * b i' * Polynomial.aeval j (d.map (algebraMap K₀ k))
      = ∑ i'' : Fin n, Polynomial.aeval j ((A i i'' i').map (algebraMap K₀ k)) * b i'') :
    ∀ i : Fin n, IsIntegral (Algebra.adjoin k ({j} : Set F))
      (Polynomial.aeval j (d.map (algebraMap K₀ k)) * b i)

theorem mwALGM_isPrincipalIdealRing_adjoin (j : F) :
    IsPrincipalIdealRing (Algebra.adjoin k ({j} : Set F))

theorem mwALGM_exists_aeval_eq_trace_of_isIntegral {j : F}
    [FiniteDimensional (IntermediateField.adjoin k ({j} : Set F)) F]
    [Algebra.IsSeparable (IntermediateField.adjoin k ({j} : Set F)) F]
    {x : F} (hint : IsIntegral (Algebra.adjoin k ({j} : Set F)) x) :
    ∃ p : Polynomial k, Polynomial.aeval j p =
      ((Algebra.trace (IntermediateField.adjoin k ({j} : Set F)) F x :
        IntermediateField.adjoin k ({j} : Set F)) : F)

theorem mwALGM_exists_basis {j : F} (hj : Transcendental k j) (n : ℕ) (b : Fin n → F)
    (hbli : ∀ c : Fin n → Polynomial k,
      (∑ i : Fin n, Polynomial.aeval j (c i) * b i) = 0 → ∀ i, c i = 0)
    (hbsp : ∀ x : F, ∃ (q : Polynomial k) (c : Fin n → Polynomial k), q ≠ 0 ∧
      x * Polynomial.aeval j q = ∑ i : Fin n, Polynomial.aeval j (c i) * b i) :
    ∃ bE : Module.Basis (Fin n) (IntermediateField.adjoin k ({j} : Set F)) F, ⇑bE = b

theorem mwALGM_gram_denom {j : F} (hj : Transcendental k j)
    [FiniteDimensional (IntermediateField.adjoin k ({j} : Set F)) F]
    [Algebra.IsSeparable (IntermediateField.adjoin k ({j} : Set F)) F]
    (n : ℕ) (b : Fin n → F)
    (hbli : ∀ c : Fin n → Polynomial k,
      (∑ i : Fin n, Polynomial.aeval j (c i) * b i) = 0 → ∀ i, c i = 0)
    (hbsp : ∀ x : F, ∃ (q : Polynomial k) (c : Fin n → Polynomial k), q ≠ 0 ∧
      x * Polynomial.aeval j q = ∑ i : Fin n, Polynomial.aeval j (c i) * b i)
    (d : Polynomial K₀) (hd : d ≠ 0) (A : Fin n → Matrix (Fin n) (Fin n) (Polynomial K₀))
    (hmul : ∀ i i' : Fin n, b i * b i' * Polynomial.aeval j (d.map (algebraMap K₀ k))
      = ∑ i'' : Fin n, Polynomial.aeval j ((A i i'' i').map (algebraMap K₀ k)) * b i'') :
    ∃ Δ : Polynomial K₀, Δ ≠ 0 ∧ ∀ x : F, IsIntegral (Algebra.adjoin k ({j} : Set F)) x →
      ∃ c : Fin n → Polynomial k,
        Polynomial.aeval j (Δ.map (algebraMap K₀ k)) * x
          = ∑ i : Fin n, Polynomial.aeval j (c i)
              * (Polynomial.aeval j (d.map (algebraMap K₀ k)) * b i)

theorem _root_.AlgebraicCurve.Place.exists_gram_denominator_of_mulTable
    {K₀ k F : Type*} [Field K₀] [Field k] [Field F] [Algebra K₀ k] [Algebra k F]
    {j : F} (hj : Transcendental k j)
    [FiniteDimensional (IntermediateField.adjoin k ({j} : Set F)) F]
    [Algebra.IsSeparable (IntermediateField.adjoin k ({j} : Set F)) F]
    (n : ℕ) (b : Fin n → F)
    (hbli : ∀ c : Fin n → Polynomial k,
      (∑ i : Fin n, Polynomial.aeval j (c i) * b i) = 0 → ∀ i, c i = 0)
    (hbsp : ∀ x : F, ∃ (q : Polynomial k) (c : Fin n → Polynomial k), q ≠ 0 ∧
      x * Polynomial.aeval j q = ∑ i : Fin n, Polynomial.aeval j (c i) * b i)
    (d : Polynomial K₀) (hd : d ≠ 0) (A : Fin n → Matrix (Fin n) (Fin n) (Polynomial K₀))
    (hmul : ∀ i i' : Fin n, b i * b i' * Polynomial.aeval j (d.map (algebraMap K₀ k))
      = ∑ i'' : Fin n, Polynomial.aeval j ((A i i'' i').map (algebraMap K₀ k)) * b i'') :
    ∃ Δ : Polynomial K₀, Δ ≠ 0 ∧ ∀ x : F, IsIntegral (Algebra.adjoin k ({j} : Set F)) x →
      ∃ c : Fin n → Polynomial k,
        Polynomial.aeval j (Δ.map (algebraMap K₀ k)) * x
          = ∑ i : Fin n, Polynomial.aeval j (c i)
              * (Polynomial.aeval j (d.map (algebraMap K₀ k)) * b i)