F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f))) ⊆ ↑⊥
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ⊤ = ⊥
rw [eq_bot_iff, ← adjoin_roots L f, roots_map (algebraMap K L) h, Algebra.adjoin_le_iff]
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
⊢ y ∈ ↑⊥
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
⊢ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f))) ⊆ ↑⊥
intro y hy
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy✝ : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
hy : ∃ a, a ∈ Multiset.toFinset (roots f) ∧ ↑(algebraMap K L) a = y
⊢ y ∈ ↑⊥
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
⊢ y ∈ ↑⊥
rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
x : K
hxy : ↑(algebraMap K L) x = y
⊢ y ∈ ↑⊥
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy✝ : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
hy : ∃ a, a ∈ Multiset.toFinset (roots f) ∧ ↑(algebraMap K L) a = y
⊢ y ∈ ↑⊥
obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
x : K
hxy : ↑(algebraMap K L) x = y
⊢ ↑(algebraMap K L) x ∈ ↑⊥
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
x : K
hxy : ↑(algebraMap K L) x = y
⊢ y ∈ ↑⊥
rw [← hxy]
no goals
case intro.intro
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : Splits (RingHom.id K) f
y : L
hy : y ∈ ↑(Multiset.toFinset (Multiset.map (↑(algebraMap K L)) (roots f)))
x : K
hxy : ↑(algebraMap K L) x = y
⊢ ↑(algebraMap K L) x ∈ ↑⊥
exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))))
      (RingEquiv.toRingHom (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))))
    f
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits
    (RingEquiv.toRingHom
      (RingEquiv.trans (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))
        (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L))))))
    f
rw [RingEquiv.toRingHom_trans]
no goals
F : Type u
K : Type v
L : Type w
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field F
inst✝⁴ : Algebra K L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : IsScalarTower F K L
f : K[X]
inst✝ : IsSplittingField K L f
h : ⊤ = ⊥
⊢ Splits
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))))
      (RingEquiv.toRingHom (RingEquiv.ofBijective (algebraMap K L) (_ : Function.Bijective ↑(algebraMap K L)))))
    f
exact splits_comp_of_splits _ _ (splits L f)