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
hfp : ∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
ι : Type v
inst✝ : Finite ι
⊢ ∃ ι_1 x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
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
hfp : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
⊢ FinitePresentation R (MvPolynomial ι A)
rw [iff_quotient_mvPolynomial'] at hfp ⊢
case intro.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 v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
⊢ ∃ ι_1 x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
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
hfp : ∃ ι x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
ι : Type v
inst✝ : Finite ι
⊢ ∃ ι_1 x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
obtain ⟨(ι' : Type v), _, f, hf_surj, hf_ker⟩ := hfp
case intro.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 v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
⊢ ∃ ι_1 x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
case intro.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 v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
⊢ ∃ ι_1 x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
let g := (MvPolynomial.mapAlgHom f).comp (MvPolynomial.sumAlgEquiv R ι ι').toAlgHom
case intro.intro.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 v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ ∃ ι_1 x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
case intro.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 v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
⊢ ∃ ι_1 x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
cases nonempty_fintype (Sum ι ι')
case intro.intro.intro.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
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Ideal.FG (RingHom.ker ↑↑(MvPolynomial.sumAlgEquiv R ι ι'))

case intro.intro.intro.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
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.mapAlgHom f))
case intro.intro.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 v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ ∃ ι_1 x f, Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
refine
  ⟨Sum ι ι', by infer_instance, g,
    (MvPolynomial.map_surjective f.toRingHom hf_surj).comp (AlgEquiv.surjective _),
    Ideal.fg_ker_comp _ _ ?_ ?_ (AlgEquiv.surjective _)⟩
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
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Fintype (ι ⊕ ι')
infer_instance
case intro.intro.intro.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
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Ideal.FG ⊥
case intro.intro.intro.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
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Ideal.FG (RingHom.ker ↑↑(MvPolynomial.sumAlgEquiv R ι ι'))
erw [RingHom.ker_coe_equiv (MvPolynomial.sumAlgEquiv R ι ι').toRingEquiv]
no goals
case intro.intro.intro.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
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Ideal.FG ⊥
exact Submodule.fg_bot
case intro.intro.intro.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
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Ideal.FG (Ideal.map MvPolynomial.C (RingHom.ker ↑f))
case intro.intro.intro.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
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.mapAlgHom f))
rw [AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.ker_map]
no goals
case intro.intro.intro.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
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ↑f
hf_ker : Ideal.FG (RingHom.ker ↑f)
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f) ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Ideal.FG (Ideal.map MvPolynomial.C (RingHom.ker ↑f))
exact hf_ker.map MvPolynomial.C