case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
⊢ IsIntegral R x
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
hx : IsIntegral A x
⊢ IsIntegral R x
rcases hx with ⟨p, pmonic, hp⟩
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
⊢ IsIntegral R x
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S
g : S →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
⊢ IsIntegral R x
let S : Set B := ↑(p.map <| algebraMap A B).frange
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (S ∪ {x})))
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
⊢ IsIntegral R x
refine' isIntegral_of_mem_of_FG (adjoin R (S ∪ {x})) _ _ (subset_adjoin <| Or.inr rfl)
case intro.intro.refine'_1
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x✝ : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x✝ p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
x : B
hx : x ∈ S
⊢ IsIntegral R x

case intro.intro.refine'_2
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
⊢ FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R S } {x}))
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
⊢ FG (↑Subalgebra.toSubmodule (adjoin R (S ∪ {x})))
refine' fg_trans (FG_adjoin_of_finite (Finset.finite_toSet _) fun x hx => _) _
case intro.intro.refine'_1
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x✝ : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x✝ p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
x : B
hx : ∃ a, a ∈ support (Polynomial.map (algebraMap A B) p) ∧ coeff (Polynomial.map (algebraMap A B) p) a = x
⊢ IsIntegral R x
case intro.intro.refine'_1
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x✝ : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x✝ p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
x : B
hx : x ∈ S
⊢ IsIntegral R x
rw [Finset.mem_coe, frange, Finset.mem_image] at hx
case intro.intro.refine'_1.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
i : ℕ
left✝ : i ∈ support (Polynomial.map (algebraMap A B) p)
⊢ IsIntegral R (coeff (Polynomial.map (algebraMap A B) p) i)
case intro.intro.refine'_1
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x✝ : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x✝ p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
x : B
hx : ∃ a, a ∈ support (Polynomial.map (algebraMap A B) p) ∧ coeff (Polynomial.map (algebraMap A B) p) a = x
⊢ IsIntegral R x
rcases hx with ⟨i, _, rfl⟩
case intro.intro.refine'_1.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
i : ℕ
left✝ : i ∈ support (Polynomial.map (algebraMap A B) p)
⊢ IsIntegral R (↑(algebraMap A B) (coeff p i))
case intro.intro.refine'_1.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
i : ℕ
left✝ : i ∈ support (Polynomial.map (algebraMap A B) p)
⊢ IsIntegral R (coeff (Polynomial.map (algebraMap A B) p) i)
rw [coeff_map]
no goals
case intro.intro.refine'_1.intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
i : ℕ
left✝ : i ∈ support (Polynomial.map (algebraMap A B) p)
⊢ IsIntegral R (↑(algebraMap A B) (coeff p i))
exact map_isIntegral (IsScalarTower.toAlgHom R A B) (A_int _)
case intro.intro.refine'_2.hx
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
⊢ IsIntegral { x // x ∈ adjoin R S } x
case intro.intro.refine'_2
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
⊢ FG (↑Subalgebra.toSubmodule (adjoin { x // x ∈ adjoin R S } {x}))
apply FG_adjoin_singleton_of_integral
no goals
case intro.intro.refine'_2.hx
R : Type u_1
A : Type u_2
B : Type u_3
S✝ : Type ?u.1384892
T : Type ?u.1384895
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing S✝
inst✝⁴ : CommRing T
inst✝³ : Algebra A B
inst✝² : Algebra R B
f : R →+* S✝
g : S✝ →+* T
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R A B
A_int : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : Monic p
hp : eval₂ (algebraMap A B) x p = 0
S : Set B := ↑(frange (Polynomial.map (algebraMap A B) p))
⊢ IsIntegral { x // x ∈ adjoin R S } x
exact isIntegral_trans_aux _ pmonic hp