case mp
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
⊢ FinitePresentation R A → ∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)

case mpr
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
⊢ (∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑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
⊢ FinitePresentation R A ↔ ∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
constructor
case mp.intro.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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ↑f
hfk : Ideal.FG (RingHom.ker ↑f)
⊢ ∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
case mp
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
⊢ FinitePresentation R A → ∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
rintro ⟨n, f, hfs, hfk⟩
case mp.intro.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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ↑f
hfk : Ideal.FG (RingHom.ker ↑f)
ulift_var : MvPolynomial (ULift ?m.48048) R ≃ₐ[R] MvPolynomial ?m.48048 R := MvPolynomial.renameEquiv R Equiv.ulift
⊢ ∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
case mp.intro.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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ↑f
hfk : Ideal.FG (RingHom.ker ↑f)
⊢ ∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
set ulift_var := MvPolynomial.renameEquiv R Equiv.ulift
case mp.intro.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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ↑f
hfk : Ideal.FG (RingHom.ker ↑f)
ulift_var : MvPolynomial (ULift (Fin n)) R ≃ₐ[R] MvPolynomial (Fin n) R := MvPolynomial.renameEquiv R Equiv.ulift
⊢ Ideal.FG (RingHom.ker ↑↑ulift_var)
case mp.intro.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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ↑f
hfk : Ideal.FG (RingHom.ker ↑f)
ulift_var : MvPolynomial (ULift ?m.48048) R ≃ₐ[R] MvPolynomial ?m.48048 R := MvPolynomial.renameEquiv R Equiv.ulift
⊢ ∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
refine'
  ⟨ULift (Fin n), inferInstance, f.comp ulift_var.toAlgHom, hfs.comp ulift_var.surjective,
    Ideal.fg_ker_comp _ _ _ hfk ulift_var.surjective⟩
case mp.intro.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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ↑f
hfk : Ideal.FG (RingHom.ker ↑f)
ulift_var : MvPolynomial (ULift (Fin n)) R ≃ₐ[R] MvPolynomial (Fin n) R := MvPolynomial.renameEquiv R Equiv.ulift
⊢ Ideal.FG ⊥
case mp.intro.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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ↑f
hfk : Ideal.FG (RingHom.ker ↑f)
ulift_var : MvPolynomial (ULift (Fin n)) R ≃ₐ[R] MvPolynomial (Fin n) R := MvPolynomial.renameEquiv R Equiv.ulift
⊢ Ideal.FG (RingHom.ker ↑↑ulift_var)
erw [RingHom.ker_coe_equiv ulift_var.toRingEquiv]
no goals
case mp.intro.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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective ↑f
hfk : Ideal.FG (RingHom.ker ↑f)
ulift_var : MvPolynomial (ULift (Fin n)) R ≃ₐ[R] MvPolynomial (Fin n) R := MvPolynomial.renameEquiv R Equiv.ulift
⊢ Ideal.FG ⊥
exact Submodule.fg_bot
case mpr.intro.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
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ FinitePresentation R A
case mpr
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
⊢ (∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)) → FinitePresentation R A
rintro ⟨ι, hfintype, f, hf⟩
case mpr.intro.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
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ FinitePresentation R A
case mpr.intro.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
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ FinitePresentation R A
have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
case mpr.intro.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
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ Ideal.FG (RingHom.ker ↑↑(AlgEquiv.symm equiv))
case mpr.intro.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
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ FinitePresentation R A
refine'
  ⟨Fintype.card ι, f.comp equiv.symm, hf.1.comp (AlgEquiv.symm equiv).surjective,
    Ideal.fg_ker_comp _ f _ hf.2 equiv.symm.surjective⟩
case mpr.intro.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
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ Ideal.FG ⊥
case mpr.intro.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
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ Ideal.FG (RingHom.ker ↑↑(AlgEquiv.symm equiv))
erw [RingHom.ker_coe_equiv equiv.symm.toRingEquiv]
no goals
case mpr.intro.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
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ Ideal.FG ⊥
exact Submodule.fg_bot