FiniteType.lean

theorem algebraTensorAlgEquiv_comp_includeRight :
    ((MvPolynomial.algebraTensorAlgEquiv (σ := Fin n) R₀ A :
        A ⊗[R₀] MvPolynomial (Fin n) R₀ ≃ₐ[A] MvPolynomial (Fin n) A) :
        A ⊗[R₀] MvPolynomial (Fin n) R₀ →+* MvPolynomial (Fin n) A).comp
      (Algebra.TensorProduct.includeRight (R := R₀) (A := A) (B := MvPolynomial (Fin n) R₀) :
        MvPolynomial (Fin n) R₀ →+* A ⊗[R₀] MvPolynomial (Fin n) R₀)
      = MvPolynomial.map (algebraMap R₀ A)

theorem ker_eq_map_map (hJ : J₀.map (MvPolynomial.map (algebraMap R₀ A)) = RingHom.ker f) :
    RingHom.ker f = (J₀.map (Algebra.TensorProduct.includeRight (R := R₀) (A := A))).map
      ((MvPolynomial.algebraTensorAlgEquiv (σ := Fin n) R₀ A :
        A ⊗[R₀] MvPolynomial (Fin n) R₀ ≃ₐ[A] MvPolynomial (Fin n) A) :
        A ⊗[R₀] MvPolynomial (Fin n) R₀ →+* MvPolynomial (Fin n) A)

def modelEquiv (hf : Function.Surjective f)
    (hJ : J₀.map (MvPolynomial.map (algebraMap R₀ A)) = RingHom.ker f) :
    A ⊗[R₀] (MvPolynomial (Fin n) R₀ ⧸ J₀) ≃ₐ[A] B

theorem modelEquiv_tmul_mk (hf : Function.Surjective f)
    (hJ : J₀.map (MvPolynomial.map (algebraMap R₀ A)) = RingHom.ker f)
    (a : A) (g₀ : MvPolynomial (Fin n) R₀) :
    modelEquiv J₀ f hf hJ (a ⊗ₜ Ideal.Quotient.mk J₀ g₀)
      = algebraMap A B a * f (MvPolynomial.map (algebraMap R₀ A) g₀)

theorem modelEquiv_one_tmul_mk (hf : Function.Surjective f)
    (hJ : J₀.map (MvPolynomial.map (algebraMap R₀ A)) = RingHom.ker f)
    (g₀ : MvPolynomial (Fin n) R₀) :
    modelEquiv J₀ f hf hJ (1 ⊗ₜ Ideal.Quotient.mk J₀ g₀)
      = f (MvPolynomial.map (algebraMap R₀ A) g₀)

theorem mem_range_comap_of_comap_mem (h : S →ₐ[R₀] S') (𝔮' : PrimeSpectrum S')
    (h𝔮 : PrimeSpectrum.comap (h : S →+* S') 𝔮' ∈
      Set.range (PrimeSpectrum.comap (algebraMap S (S ⊗[R₀] C)))) :
    𝔮' ∈ Set.range (PrimeSpectrum.comap (algebraMap S' (S' ⊗[R₀] C)))

theorem eq_top_of_faithfullyFlat_of_surjective (E : Subalgebra R₀ A) (C : Type*) [CommRing C]
    [Algebra E C] [Module.FaithfullyFlat E C]
    (hs : Function.Surjective (fun c : C => (1 : A) ⊗ₜ[E] c)) : E = ⊤ := by
  have hsurj : Function.Surjective ((Algebra.linearMap E A).lTensor C) := by
    intro z
    obtain ⟨c, hc⟩ := hs (TensorProduct.comm E C A z)
    refine ⟨c ⊗ₜ (1 : E), ?_⟩
    apply (TensorProduct.comm E C A).injective
    rw [LinearMap.lTensor_tmul, Algebra.linearMap_apply, map_one, TensorProduct.comm_tmul]
    exact hc
  rw [Module.FaithfullyFlat.lTensor_surjective_iff_surjective] at hsurj
  refine eq_top_iff.mpr fun x _ => ?_
  obtain ⟨e, rfl⟩ := hsurj x
  exact e.2

def toTop (E : Subalgebra R₀ A) : E ⊗[R₀] Bq →ₐ[R₀] A ⊗[R₀] Bq

theorem toTop_tmul (E : Subalgebra R₀ A) (e : E) (b : Bq) :
    toTop Bq E (e ⊗ₜ b) = (e : A) ⊗ₜ b

theorem toTop_comp_algebraMap (E : Subalgebra R₀ A) :
    (toTop Bq E : E ⊗[R₀] Bq →+* A ⊗[R₀] Bq).comp (algebraMap E (E ⊗[R₀] Bq))
      = (algebraMap A (A ⊗[R₀] Bq)).comp (algebraMap E A)

theorem toTop_surjective
    (hgen : Function.Surjective
      (Algebra.TensorProduct.includeRight : Bq →ₐ[R₀] A ⊗[R₀] Bq))
    (E : Subalgebra R₀ A) : Function.Surjective (toTop Bq E)

theorem one_tmul_surjective
    (hgen : Function.Surjective
      (Algebra.TensorProduct.includeRight : Bq →ₐ[R₀] A ⊗[R₀] Bq))
    (E : Subalgebra R₀ A) :
    Function.Surjective (fun c : E ⊗[R₀] Bq => (1 : A) ⊗ₜ[E] c) := by
  intro z
  let ψ := Algebra.TensorProduct.cancelBaseChange R₀ E E A Bq
  have hψ : ∀ c : E ⊗[R₀] Bq, ψ ((1 : A) ⊗ₜ[E] c) = toTop Bq E c := by
    intro c
    induction c using TensorProduct.inductionOn with
    | tmul e b =>
      rw [toTop_tmul, Algebra.TensorProduct.cancelBaseChange_tmul, Algebra.smul_def, mul_one]
      rfl
    | add x y hx hy => rw [TensorProduct.tmul_add, map_add, hx, hy, map_add]
  obtain ⟨c, hc⟩ := toTop_surjective Bq hgen E (ψ z)
  refine ⟨c, ψ.injective ?_⟩
  change ψ ((1 : A) ⊗ₜ[E] c) = ψ z
  rw [hψ, hc]

theorem isOpen_range_comap (E : Subalgebra R₀ A) [Module.Flat E (E ⊗[R₀] Bq)] :
    IsOpen (Set.range (PrimeSpectrum.comap (algebraMap E (E ⊗[R₀] Bq))))

theorem fg_top_of_faithfullyFlat [Module.FaithfullyFlat A (A ⊗[R₀] Bq)]
    (hgen : Function.Surjective
      (Algebra.TensorProduct.includeRight : Bq →ₐ[R₀] A ⊗[R₀] Bq)) :
    (⊤ : Subalgebra R₀ A).FG

theorem map_span_range_lift {n : ℕ} (tk : Finset (MvPolynomial (Fin n) A))
    (g₀ : tk → MvPolynomial (Fin n) R₀)
    (hg₀ : ∀ g, MvPolynomial.map (algebraMap R₀ A) (g₀ g) = g) :
    (Ideal.span (Set.range g₀)).map (MvPolynomial.map (algebraMap R₀ A))
      = Ideal.span (↑tk : Set (MvPolynomial (Fin n) A))

theorem finiteType_of_lifts [Module.FaithfullyFlat A B] [Algebra.FiniteType R R₀]
    {n : ℕ} (f : MvPolynomial (Fin n) A →ₐ[A] B) (hf : Function.Surjective f)
    (tk : Finset (MvPolynomial (Fin n) A))
    (htk : Ideal.span (↑tk : Set (MvPolynomial (Fin n) A)) = RingHom.ker f)
    (g₀ : tk → MvPolynomial (Fin n) R₀)
    (hg₀ : ∀ g, MvPolynomial.map (algebraMap R₀ A) (g₀ g) = g)
    (sB : Finset B) (hsB : Algebra.adjoin R (↑sB : Set B) = ⊤)
    (P₀ : sB → MvPolynomial (Fin n) R₀)
    (hP₀ : ∀ b, f (MvPolynomial.map (algebraMap R₀ A) (P₀ b)) = b) :
    Algebra.FiniteType R A

theorem finiteType_of_faithfullyFlat_of_finitePresentation
    (R : Type u) (A : Type v) (B : Type w) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
    [Module.FaithfullyFlat A B] [Algebra.FinitePresentation A B] [Algebra.FiniteType R B] :
    Algebra.FiniteType R A

theorem Algebra.FiniteType.of_faithfullyFlat_of_finitePresentation
    (R : Type u) (A : Type v) (B : Type w) [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] [Algebra A B] [IsScalarTower R A B]
    [Module.FaithfullyFlat A B] [Algebra.FinitePresentation A B] [Algebra.FiniteType R B] :
    Algebra.FiniteType R A