case intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hS : adjoin F S = ⊤
hK : ∀ (x : E), x ∈ S → IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x)
ϕ : { x // x ∈ adjoin F S } →ₐ[F] K
⊢ Nonempty (E →ₐ[F] K)
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hS : adjoin F S = ⊤
hK : ∀ (x : E), x ∈ S → IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x)
⊢ Nonempty (E →ₐ[F] K)
cases' algHom_mk_adjoin_splits hK with ϕ
case intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hS : adjoin F S = ⊤
hK : ∀ (x : E), x ∈ S → IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x)
ϕ : { x // x ∈ ⊤ } →ₐ[F] K
⊢ Nonempty (E →ₐ[F] K)
case intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hS : adjoin F S = ⊤
hK : ∀ (x : E), x ∈ S → IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x)
ϕ : { x // x ∈ adjoin F S } →ₐ[F] K
⊢ Nonempty (E →ₐ[F] K)
rw [hS] at ϕ
no goals
case intro
F : Type u_2
E : Type u_1
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
hS : adjoin F S = ⊤
hK : ∀ (x : E), x ∈ S → IsIntegral F x ∧ Splits (algebraMap F K) (minpoly F x)
ϕ : { x // x ∈ ⊤ } →ₐ[F] K
⊢ Nonempty (E →ₐ[F] K)
exact ⟨ϕ.comp topEquiv.symm.toAlgHom⟩