GeneratorReduction.lean

theorem adjoin_linearTailCoordinatesFirst_le
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (c : Fin n → K) (x : Fin (n + 1) → A) :
    Algebra.adjoin K (Set.range (linearTailCoordinatesFirst c x)) ≤
      Algebra.adjoin K (Set.range x)

theorem adjoin_range_eq_adjoin_linearTailCoordinatesFirst_union
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (c : Fin n → K) (x : Fin (n + 1) → A) :
    Algebra.adjoin K (Set.range x) =
      Algebra.adjoin K
        (Set.range (linearTailCoordinatesFirst c x) ∪ {x 0})

theorem isIntegral_of_mem_adjoin_range_of_first
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (c : Fin n → K) (x : Fin (n + 1) → A)
    (hfirst :
      IsIntegral
        (Algebra.adjoin K (Set.range (linearTailCoordinatesFirst c x))) (x 0)) :
    ∀ y ∈ Algebra.adjoin K (Set.range x),
      IsIntegral
        (Algebra.adjoin K (Set.range (linearTailCoordinatesFirst c x))) y

theorem isIntegral_of_mem_adjoin_range_self
    {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (x : Fin n → A) :
    ∀ y ∈ Algebra.adjoin K (Set.range x),
      IsIntegral (Algebra.adjoin K (Set.range x)) y

theorem exists_generatorReducing_linearTail
    [Infinite K] {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (x : Fin (n + 1) → A) {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F ≠ 0) (hrel : aeval x F = 0) :
    ∃ c : Fin n → K,
      let t : Fin n → A := linearTailCoordinatesFirst c x
      Algebra.adjoin K (Set.range t) ≤ Algebra.adjoin K (Set.range x) ∧
        Algebra.adjoin K (Set.range x) =
          Algebra.adjoin K (Set.range t ∪ {x 0}) ∧
        ∀ y ∈ Algebra.adjoin K (Set.range x),
          IsIntegral (Algebra.adjoin K (Set.range t)) y := by
  obtain ⟨c, hc⟩ := exists_linearCoordinatesFirst_isIntegral x hF hrel
  refine ⟨c, ?_, ?_, ?_⟩
  · exact adjoin_linearTailCoordinatesFirst_le c x
  · exact adjoin_range_eq_adjoin_linearTailCoordinatesFirst_union c x
  · exact isIntegral_of_mem_adjoin_range_of_first c x hc

theorem exists_linearTail_isIntegral_of_adjoin_eq_top
    [Infinite K] {A : Type*} [CommRing A] [Algebra K A] {n : ℕ}
    (x : Fin (n + 1) → A)
    (hx : Algebra.adjoin K (Set.range x) = ⊤)
    {F : MvPolynomial (Fin (n + 1)) K}
    (hF : F ≠ 0) (hrel : aeval x F = 0) :
    ∃ c : Fin n → K,
      Algebra.IsIntegral
        (Algebra.adjoin K (Set.range (linearTailCoordinatesFirst c x))) A

theorem exists_linearNormalization_span_integral
    [Infinite K] {A : Type*} [CommRing A] [Nontrivial A] [Algebra K A] :
    ∀ {n : ℕ} (x : Fin n → A),
      ∃ r : ℕ, r ≤ n ∧
        ∃ t : Fin r → A,
          (∀ i, t i ∈ Submodule.span K (Set.range x)) ∧
            AlgebraicIndependent K t ∧
              ∀ y ∈ Algebra.adjoin K (Set.range x),
                IsIntegral (Algebra.adjoin K (Set.range t)) y
  | 0, x => by
      refine ⟨0, le_rfl, x, ?_, algebraicIndependent_empty_type, ?_⟩
      · exact fun i => Fin.elim0 i
      · exact isIntegral_of_mem_adjoin_range_self x
  | n + 1, x => by
      by_cases hx : AlgebraicIndependent K x
      · refine ⟨n + 1, le_rfl, x, ?_, hx, ?_⟩
        · intro i
          exact Submodule.subset_span ⟨i, rfl⟩
        · exact isIntegral_of_mem_adjoin_range_self x
      · have hnotinj :
            ¬ Function.Injective
              (aeval x : MvPolynomial (Fin (n + 1)) K →ₐ[K] A) := by
          intro hinj
          exact hx (algebraicIndependent_iff_injective_aeval.mpr hinj)
        obtain ⟨P, Q, hPQ, hne⟩ := Function.not_injective_iff.mp hnotinj
        let F : MvPolynomial (Fin (n + 1)) K := P - Q
        have hF : F ≠ 0 := sub_ne_zero.mpr hne
        have hrel : aeval x F = 0 := by
          dsimp only [F]
          rw [map_sub, hPQ, sub_self]
        obtain ⟨c, htail_le, -, hstep⟩ :=
          exists_generatorReducing_linearTail x hF hrel
        let tail : Fin n → A := linearTailCoordinatesFirst c x
        obtain ⟨r, hr, t, htspan, htind, htail_integral⟩ :=
          exists_linearNormalization_span_integral tail
        refine ⟨r, hr.trans (Nat.le_succ n), t, ?_, htind, ?_⟩
        · have htail_span :
              ∀ i, tail i ∈ Submodule.span K (Set.range x) := by
            intro i
            have hxi :
                x i.succ ∈ Submodule.span K (Set.range x) :=
              Submodule.subset_span ⟨i.succ, rfl⟩
            have hx₀ :
                x 0 ∈ Submodule.span K (Set.range x) :=
              Submodule.subset_span ⟨0, rfl⟩
            simpa only [tail, linearTailCoordinatesFirst, Algebra.smul_def] using
              Submodule.sub_mem (Submodule.span K (Set.range x)) hxi
                (Submodule.smul_mem (Submodule.span K (Set.range x)) (c i) hx₀)
          have hspan_le :
              Submodule.span K (Set.range tail) ≤
                Submodule.span K (Set.range x) := by
            rw [Submodule.span_le]
            rintro y ⟨i, rfl⟩
            exact htail_span i
          exact fun i => hspan_le (htspan i)
        · let B : Subalgebra K A := Algebra.adjoin K (Set.range t)
          let S : Subalgebra K A := Algebra.adjoin K (Set.range tail)
          have ht_mem_S : ∀ i, t i ∈ S := by
            intro i
            change t i ∈ S.toSubmodule
            exact
              (Submodule.span_le.mpr
                (fun y hy => Algebra.subset_adjoin hy) :
                  Submodule.span K (Set.range tail) ≤ S.toSubmodule) (htspan i)
          have hBS : B ≤ S := by
            rw [Algebra.adjoin_le_iff]
            rintro y ⟨i, rfl⟩
            exact ht_mem_S i
          let : Algebra B S := (Subalgebra.inclusion hBS).toAlgebra
          have : IsScalarTower B S A :=
            IsScalarTower.of_algebraMap_eq fun _ => rfl
          let : Algebra.IsIntegral B S :=
            ⟨fun z =>
              (isIntegral_algebraMap_iff (R := B) (A := S) (B := A)).mp
                (htail_integral z z.property)⟩
          intro y hy
          exact isIntegral_trans y (hstep y hy)