case intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal A
h : Ideal.FG I
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ FinitePresentation R (A ⧸ I)
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal A
h : Ideal.FG I
hfp : FinitePresentation R A
⊢ FinitePresentation R (A ⧸ I)
obtain ⟨n, f, hf⟩ := hfp
case intro.intro.refine'_1
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal A
h : Ideal.FG I
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Surjective ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f)

case intro.intro.refine'_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal A
h : Ideal.FG I
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Ideal.FG (RingHom.ker ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f))
case intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal A
h : Ideal.FG I
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ FinitePresentation R (A ⧸ I)
refine' ⟨n, (Ideal.Quotient.mkₐ R I).comp f, _, _⟩
no goals
case intro.intro.refine'_1
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal A
h : Ideal.FG I
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Surjective ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
exact (Ideal.Quotient.mkₐ_surjective R I).comp hf.1
case intro.intro.refine'_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal A
h : Ideal.FG I
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Ideal.FG (RingHom.ker ↑(Ideal.Quotient.mkₐ R I))
case intro.intro.refine'_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal A
h : Ideal.FG I
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Ideal.FG (RingHom.ker ↑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f))
refine' Ideal.fg_ker_comp _ _ hf.2 _ hf.1
no goals
case intro.intro.refine'_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
I : Ideal A
h : Ideal.FG I
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Ideal.FG (RingHom.ker ↑(Ideal.Quotient.mkₐ R I))
simp [h]