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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ FinitePresentation R B
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
e : A ≃ₐ[R] B
⊢ FinitePresentation R B
obtain ⟨n, f, hf⟩ := hfp
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Surjective ↑(AlgHom.comp (↑e) f) ∧ Ideal.FG (RingHom.ker ↑(AlgHom.comp (↑e) 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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ FinitePresentation R B
use n, AlgHom.comp (↑e) f
case intro.intro.left
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Surjective ↑(AlgHom.comp (↑e) f)

case intro.intro.right
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Ideal.FG (RingHom.ker ↑(AlgHom.comp (↑e) 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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Surjective ↑(AlgHom.comp (↑e) f) ∧ Ideal.FG (RingHom.ker ↑(AlgHom.comp (↑e) f))
constructor
case intro.intro.right
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
hker : RingHom.ker ↑(AlgHom.comp (↑e) f) = RingHom.ker ↑f
⊢ Ideal.FG (RingHom.ker ↑(AlgHom.comp (↑e) f))

case hker
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ RingHom.ker ↑(AlgHom.comp (↑e) f) = RingHom.ker ↑f
case intro.intro.right
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Ideal.FG (RingHom.ker ↑(AlgHom.comp (↑e) f))
suffices hker : (RingHom.ker (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom) = RingHom.ker f.toRingHom
case intro.intro.left
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Surjective (↑↑e ∘ ↑f)
case intro.intro.left
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Surjective ↑(AlgHom.comp (↑e) f)
rw [AlgHom.coe_comp]
no goals
case intro.intro.left
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ Surjective (↑↑e ∘ ↑f)
exact Function.Surjective.comp e.surjective hf.1
case intro.intro.right
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
hker : RingHom.ker ↑(AlgHom.comp (↑e) f) = RingHom.ker ↑f
⊢ Ideal.FG (RingHom.ker ↑f)
case intro.intro.right
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
hker : RingHom.ker ↑(AlgHom.comp (↑e) f) = RingHom.ker ↑f
⊢ Ideal.FG (RingHom.ker ↑(AlgHom.comp (↑e) f))
rw [hker]
no goals
case intro.intro.right
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
hker : RingHom.ker ↑(AlgHom.comp (↑e) f) = RingHom.ker ↑f
⊢ Ideal.FG (RingHom.ker ↑f)
exact hf.2
case hker
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
hco : ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑(AlgEquiv.toRingEquiv e) ↑f
⊢ RingHom.ker ↑(AlgHom.comp (↑e) f) = RingHom.ker ↑f
case hker
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ RingHom.ker ↑(AlgHom.comp (↑e) f) = RingHom.ker ↑f
have hco : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom = RingHom.comp (e.toRingEquiv : A ≃+* B)
  f.toRingHom := by
  have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom =
    e.toAlgHom.toRingHom.comp f.toRingHom := rfl
  have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
  rw [h, h1]
no goals
case hker
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
hco : ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑(AlgEquiv.toRingEquiv e) ↑f
⊢ RingHom.ker ↑(AlgHom.comp (↑e) f) = RingHom.ker ↑f
rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
  RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
h : ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑↑e ↑f
⊢ ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑(AlgEquiv.toRingEquiv e) ↑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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
⊢ ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑(AlgEquiv.toRingEquiv e) ↑f
have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom =
  e.toAlgHom.toRingHom.comp f.toRingHom := rfl
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
h : ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑↑e ↑f
h1 : ↑(AlgEquiv.toRingEquiv e) = ↑↑e
⊢ ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑(AlgEquiv.toRingEquiv e) ↑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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
h : ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑↑e ↑f
⊢ ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑(AlgEquiv.toRingEquiv e) ↑f
have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
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
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f ∧ Ideal.FG (RingHom.ker ↑f)
h : ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑↑e ↑f
h1 : ↑(AlgEquiv.toRingEquiv e) = ↑↑e
⊢ ↑(AlgHom.comp (↑e) f) = RingHom.comp ↑(AlgEquiv.toRingEquiv e) ↑f
rw [h, h1]