FinitePresentation.lean

lemma ker_includeRight_le_map (h : Function.Surjective (algebraMap A' A)) :
    RingHom.ker (Algebra.TensorProduct.includeRight : B' →ₐ[A'] A ⊗[A'] B').toRingHom ≤
      (RingHom.ker (algebraMap A' A)).map (algebraMap A' B')

lemma exists_fg_le_of_le_map {S : Type*} [CommRing S] (φ : A' →+* S) (I : Ideal A') (N : Ideal S)
    (hN : N.FG) (h : N ≤ I.map φ) : ∃ I₀ : Ideal A', I₀ ≤ I ∧ I₀.FG ∧ N ≤ I₀.map φ

def θ (J : Ideal A') (hJ : J ≤ RingHom.ker (algebraMap A' A)) :
    (A' ⧸ J) ⊗[A'] B' →ₐ[A'] A ⊗[A'] B'

lemma θ_tmul (J : Ideal A') (hJ : J ≤ RingHom.ker (algebraMap A' A)) (a : A') (b : B') :
    θ A B' J hJ (Ideal.Quotient.mk J a ⊗ₜ b) = algebraMap A' A a ⊗ₜ b

lemma θ_includeRight (J : Ideal A') (hJ : J ≤ RingHom.ker (algebraMap A' A)) (b : B') :
    θ A B' J hJ (Algebra.TensorProduct.includeRight b) = (1 : A) ⊗ₜ b

lemma θ_injective (J : Ideal A')
    (hJ : J ≤ RingHom.ker (algebraMap A' A))
    (hker : RingHom.ker (Algebra.TensorProduct.includeRight : B' →ₐ[A'] A ⊗[A'] B').toRingHom ≤
      J.map (algebraMap A' B')) :
    Function.Injective (θ A B' J hJ)

lemma θ_smul_eq_zero (J : Ideal A') (hJ : J ≤ RingHom.ker (algebraMap A' A)) (a : A')
    (ha : algebraMap A' A a = 0) (x : (A' ⧸ J) ⊗[A'] B') :
    θ A B' J hJ (Ideal.Quotient.mk J a • x) = 0

theorem ker_fg_of_faithfullyFlat_baseChange (h : Function.Surjective (algebraMap A' A))
    [Module.Flat A' B'] [Algebra.FinitePresentation A' B']
    [Module.FaithfullyFlat A (A ⊗[A'] B')] [Algebra.FinitePresentation A' (A ⊗[A'] B')] :
    (RingHom.ker (algebraMap A' A)).FG

theorem ker_fg_of_descent (P : Type*) (A : Type*) (B : Type*) [CommRing P] [CommRing A] [CommRing B]
    [Algebra P A] [Algebra A B] [Algebra P B] [IsScalarTower P A B]
    (hπ : Function.Surjective (algebraMap P A))
    [Module.FaithfullyFlat A B] [Algebra.FinitePresentation P B]
    (A₁ : Type*) [CommRing A₁] [Algebra A₁ A] (B₁ : Type*) [CommRing B₁] [Algebra A₁ B₁]
    [Module.Flat A₁ B₁] [Algebra.FinitePresentation A₁ B₁]
    (e : A ⊗[A₁] B₁ ≃ₐ[A] B)
    (R₁ : Type*) [CommRing R₁] [Algebra R₁ P] [Algebra R₁ A₁] [IsNoetherianRing R₁]
    (hρ : Function.Surjective (algebraMap R₁ A₁))
    (hcompat : ∀ r : R₁, algebraMap A₁ A (algebraMap R₁ A₁ r) =
      algebraMap P A (algebraMap R₁ P r)) :
    (RingHom.ker (algebraMap P A)).FG

theorem ker_fg_of_model (P : Type*) (A : Type*) (B : Type*) [CommRing P] [CommRing A] [CommRing B]
    [Algebra P A] [Algebra A B] [Algebra P B] [IsScalarTower P A B]
    (hπ : Function.Surjective (algebraMap P A))
    [Module.FaithfullyFlat A B] [Algebra.FinitePresentation P B]
    (R₀ : Type*) [CommRing R₀] [Algebra R₀ P] [Algebra R₀ A]
    [IsScalarTower R₀ P A] [IsNoetherianRing R₀]
    (Bq : Type*) [CommRing Bq] [Algebra R₀ Bq] [Algebra.FinitePresentation R₀ Bq]
    (Φ : A ⊗[R₀] Bq ≃ₐ[A] B) :
    (RingHom.ker (algebraMap P A)).FG

theorem ker_fg_of_lifts (P : Type*) (A : Type*) (B : Type*) [CommRing P] [CommRing A] [CommRing B]
    [Algebra P A] [Algebra A B] [Algebra P B] [IsScalarTower P A B]
    (hπ : Function.Surjective (algebraMap P A))
    [Module.FaithfullyFlat A B] [Algebra.FinitePresentation P B]
    (R₀ : Type*) [CommRing R₀] [Algebra R₀ P] [Algebra R₀ A]
    [IsScalarTower R₀ P A] [IsNoetherianRing R₀]
    {k : ℕ} (ψ : MvPolynomial (Fin k) A →ₐ[A] B) (hψ : Function.Surjective ψ)
    (tk : Finset (MvPolynomial (Fin k) A))
    (htk : Ideal.span (↑tk : Set (MvPolynomial (Fin k) A)) = RingHom.ker ψ)
    (g₀ : tk → MvPolynomial (Fin k) R₀) (hg₀ : ∀ g, MvPolynomial.map (algebraMap R₀ A) (g₀ g) = g) :
    (RingHom.ker (algebraMap P A)).FG

theorem ker_fg_of_surjective (P : Type*) (A : Type*) (B : Type*)
    [CommRing P] [CommRing A] [CommRing B]
    [Algebra P A] [Algebra A B] [Algebra P B] [IsScalarTower P A B]
    (hπ : Function.Surjective (algebraMap P A))
    [Module.FaithfullyFlat A B] [Algebra.FinitePresentation A B] [Algebra.FinitePresentation P B] :
    (RingHom.ker (algebraMap P A)).FG

theorem main (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.FinitePresentation R B] :
    Algebra.FinitePresentation R A

theorem Algebra.FinitePresentation.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.FinitePresentation R B] :
    Algebra.FinitePresentation R A