Algebra_exists_finitePresentation_tensorProduct_algEquiv_of_isDirectLimit.lean

theorem range_mono {ι : Type u} [Preorder ι]
    {G : ι → Type v} [∀ i, CommRing (G i)] (f : ∀ i j : ι, i ≤ j → G i →+* G j)
    [DirectedSystem G fun i j h => ⇑(f i j h)]
    {R : Type w} [CommRing R] [∀ i, Algebra (G i) R]
    (hR : IsDirectLimit (fun i j h => ⇑(f i j h)) fun i => ⇑(algebraMap (G i) R))
    {i j : ι} (hij : i ≤ j) :
    Set.range (algebraMap (G i) R) ⊆ Set.range (algebraMap (G j) R) := by
  rintro _ ⟨x, rfl⟩
  exact ⟨f i j hij x, hR.compatibility i j hij x⟩

theorem exists_subset_range_of_finite {ι : Type u} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
    {G : ι → Type v} [∀ i, CommRing (G i)] (f : ∀ i j : ι, i ≤ j → G i →+* G j)
    [DirectedSystem G fun i j h => ⇑(f i j h)]
    {R : Type w} [CommRing R] [∀ i, Algebra (G i) R]
    (hR : IsDirectLimit (fun i j h => ⇑(f i j h)) fun i => ⇑(algebraMap (G i) R))
    {s : Set R} (hs : s.Finite) :
    ∃ i : ι, s ⊆ Set.range (algebraMap (G i) R) := by
  classical
  let idx : R → ι := fun r => (hR.surj r).choose
  have hidx : ∀ r : R, r ∈ Set.range (algebraMap (G (idx r)) R) := fun r =>
    let ⟨x, hx⟩ := (hR.surj r).choose_spec
    ⟨x, hx⟩
  obtain ⟨M, hM⟩ := Finset.exists_le (hs.toFinset.image idx)
  refine ⟨M, fun r hr => ?_⟩
  have hle : idx r ≤ M := hM _ (Finset.mem_image_of_mem idx (hs.mem_toFinset.mpr hr))
  exact range_mono f hR hle (hidx r)

theorem _root_.Algebra.exists_finitePresentation_tensorProduct_algEquiv_of_isDirectLimit
    {ι : Type u} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
    (G : ι → Type v) [∀ i, CommRing (G i)] (f : ∀ i j : ι, i ≤ j → G i →+* G j)
    [DirectedSystem G fun i j h => ⇑(f i j h)]
    (R : Type w) [CommRing R] [∀ i, Algebra (G i) R]
    (hR : IsDirectLimit (fun i j h => ⇑(f i j h)) fun i => ⇑(algebraMap (G i) R))
    (A : Type w') [CommRing A] [Algebra R A] [Algebra.FinitePresentation R A] :
    ∃ (i : ι) (A₀ : Type v) (_ : CommRing A₀) (_ : Algebra (G i) A₀)
      (_ : Algebra.FinitePresentation (G i) A₀), Nonempty ((R ⊗[G i] A₀) ≃ₐ[R] A) := by
  classical
  let P := Algebra.Presentation.ofFinitePresentation R A
  obtain ⟨i, hi⟩ := exists_subset_range_of_finite f hR (s := P.coeffs)
    Algebra.Presentation.finite_coeffs
  let : Algebra (G i) A := ((algebraMap R A).comp (algebraMap (G i) R)).toAlgebra
  have : IsScalarTower (G i) R A := IsScalarTower.of_algebraMap_eq (fun _ => rfl)
  have : P.HasCoeffs (G i) := ⟨hi⟩
  exact ⟨i, P.ModelOfHasCoeffs (G i), inferInstance, inferInstance, inferInstance,
    ⟨P.tensorModelOfHasCoeffsEquiv (G i)⟩⟩