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
inst✝ : IsNoetherianRing R
h : FiniteType R A
⊢ FinitePresentation R A
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
inst✝ : IsNoetherianRing R
⊢ FiniteType R A ↔ FinitePresentation R A
refine' ⟨fun h => _, Algebra.FiniteType.of_finitePresentation⟩
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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
⊢ FinitePresentation R A
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
inst✝ : IsNoetherianRing R
h : FiniteType R A
⊢ FinitePresentation R A
obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.1 h
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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
⊢ Ideal.FG (RingHom.ker ↑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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
⊢ FinitePresentation R A
refine' ⟨n, f, hf, _⟩
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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
hnoet : IsNoetherianRing (MvPolynomial (Fin n) R)
⊢ Ideal.FG (RingHom.ker ↑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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
⊢ Ideal.FG (RingHom.ker ↑f)
have hnoet : IsNoetherianRing (MvPolynomial (Fin n) R) := by infer_instance
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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
⊢ Ideal.FG (RingHom.ker ↑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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
hnoet : IsNoetherianRing (MvPolynomial (Fin n) R)
⊢ Ideal.FG (RingHom.ker ↑f)
rw [isNoetherianRing_iff] at hnoet
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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
this : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule
⊢ Ideal.FG (RingHom.ker ↑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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
⊢ Ideal.FG (RingHom.ker ↑f)
letI : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule
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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
this✝ : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule
this : Submodule.FG (RingHom.ker ↑f)
⊢ Ideal.FG (RingHom.ker ↑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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
this : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule
⊢ Ideal.FG (RingHom.ker ↑f)
have := hnoet.noetherian (RingHom.ker f.toRingHom)
no goals
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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)
this✝ : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule
this : Submodule.FG (RingHom.ker ↑f)
⊢ Ideal.FG (RingHom.ker ↑f)
convert this
no goals
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
inst✝ : IsNoetherianRing R
h : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
⊢ IsNoetherianRing (MvPolynomial (Fin n) R)
infer_instance