R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
h' : FiniteType f
this : Algebra R S := toAlgebra f
⊢ Finite f
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
h' : FiniteType f
⊢ Finite f
letI := f.toAlgebra
case mk.intro
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
this : Algebra R S := toAlgebra f
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
⊢ Finite f
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
h' : FiniteType f
this : Algebra R S := toAlgebra f
⊢ Finite f
obtain ⟨s, hs⟩ := h'
case mk.intro.out
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
this : Algebra R S := toAlgebra f
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
⊢ FG ⊤
case mk.intro
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
this : Algebra R S := toAlgebra f
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
⊢ Finite f
constructor
case mk.intro.out
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
this : Algebra R S := toAlgebra f
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
⊢ FG (↑Subalgebra.toSubmodule ⊤)
case mk.intro.out
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
this : Algebra R S := toAlgebra f
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
⊢ FG ⊤
change (⊤ : Subalgebra R S).toSubmodule.FG
case mk.intro.out
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
this : Algebra R S := toAlgebra f
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
⊢ FG (↑Subalgebra.toSubmodule (Algebra.adjoin R ↑s))
case mk.intro.out
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
this : Algebra R S := toAlgebra f
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
⊢ FG (↑Subalgebra.toSubmodule ⊤)
rw [← hs]
no goals
case mk.intro.out
R : Type u_1
A : Type ?u.599454
B : Type ?u.599457
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing S
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : R →+* S
h : IsIntegral f
this : Algebra R S := toAlgebra f
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
⊢ FG (↑Subalgebra.toSubmodule (Algebra.adjoin R ↑s))
exact FG_adjoin_of_finite (Set.toFinite _) fun x _ => h x