k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
⊢ ⊤ ≤ (maximalSubfieldWithHom K L M).carrier
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
⊢ (maximalSubfieldWithHom K L M).carrier = ⊤
rw [eq_top_iff]
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
⊢ ⊤ ≤ (maximalSubfieldWithHom K L M).carrier
intro x _
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
let N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
letI : Field N := (Subalgebra.isField_of_algebraic N hL).toField
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
letI : Algebra N M := (maximalSubfieldWithHom K L M).emb.toRingHom.toAlgebra
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
obtain ⟨y, hy⟩ := IsAlgClosed.exists_aeval_eq_zero M (minpoly N x) <|
  (minpoly.degree_pos
    (isAlgebraic_iff_isIntegral.1 (Algebra.isAlgebraic_of_larger_base _ _ hL x))).ne'
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
let O : Subalgebra N L := Algebra.adjoin N {(x : L)}
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
letI : Algebra N O := Subalgebra.algebra O
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
let larger_emb : O →ₐ[N] M := Algebra.adjoin.liftSingleton N x y hy
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
let larger_emb' : O →ₐ[K] M := AlgHom.restrictScalars K (S := N) (A := O) (B := M) larger_emb
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
have hNO : N ≤ O.restrictScalars K := by
  intro z hz
  show algebraMap N L ⟨z, hz⟩ ∈ O
  exact O.algebraMap_mem _
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
let O' : SubfieldWithHom K L M :=
  ⟨O.restrictScalars K, larger_emb'⟩
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
hO' : maximalSubfieldWithHom K L M ≤ O'
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
have hO' : maximalSubfieldWithHom K L M ≤ O' := by
  refine' ⟨hNO, _⟩
  intro z
  show Algebra.adjoin.liftSingleton N x y hy (@algebraMap N O _ _ (Subalgebra.algebra O) z) =
      algebraMap N M z
  exact AlgHom.commutes _ _
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
hO' : maximalSubfieldWithHom K L M ≤ O'
⊢ x ∈ O'.carrier
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
hO' : maximalSubfieldWithHom K L M ≤ O'
⊢ x ∈ (maximalSubfieldWithHom K L M).carrier
refine' (maximalSubfieldWithHom_is_maximal K L M O' hO').fst _
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
hO' : maximalSubfieldWithHom K L M ≤ O'
⊢ x ∈ Algebra.adjoin { x // x ∈ N } {x}
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
hO' : maximalSubfieldWithHom K L M ≤ O'
⊢ x ∈ O'.carrier
show x ∈ Algebra.adjoin N {(x : L)}
no goals
case intro
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
hO' : maximalSubfieldWithHom K L M ≤ O'
⊢ x ∈ Algebra.adjoin { x // x ∈ N } {x}
exact Algebra.subset_adjoin (Set.mem_singleton x)
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
z : L
hz : z ∈ N
⊢ z ∈ Subalgebra.restrictScalars K O
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
⊢ N ≤ Subalgebra.restrictScalars K O
intro z hz
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
z : L
hz : z ∈ N
⊢ ↑(algebraMap { x // x ∈ N } L) { val := z, property := hz } ∈ O
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
z : L
hz : z ∈ N
⊢ z ∈ Subalgebra.restrictScalars K O
show algebraMap N L ⟨z, hz⟩ ∈ O
no goals
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
z : L
hz : z ∈ N
⊢ ↑(algebraMap { x // x ∈ N } L) { val := z, property := hz } ∈ O
exact O.algebraMap_mem _
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
⊢ ∀ (x : { x // x ∈ (maximalSubfieldWithHom K L M).carrier }),
    ↑O'.emb (↑(inclusion hNO) x) = ↑(maximalSubfieldWithHom K L M).emb x
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
⊢ maximalSubfieldWithHom K L M ≤ O'
refine' ⟨hNO, _⟩
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
z : { x // x ∈ (maximalSubfieldWithHom K L M).carrier }
⊢ ↑O'.emb (↑(inclusion hNO) z) = ↑(maximalSubfieldWithHom K L M).emb z
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
⊢ ∀ (x : { x // x ∈ (maximalSubfieldWithHom K L M).carrier }),
    ↑O'.emb (↑(inclusion hNO) x) = ↑(maximalSubfieldWithHom K L M).emb x
intro z
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
z : { x // x ∈ (maximalSubfieldWithHom K L M).carrier }
⊢ ↑(Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy) (↑(algebraMap { x // x ∈ N } { x // x ∈ O }) z) =
    ↑(algebraMap { x // x ∈ N } M) z
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
z : { x // x ∈ (maximalSubfieldWithHom K L M).carrier }
⊢ ↑O'.emb (↑(inclusion hNO) z) = ↑(maximalSubfieldWithHom K L M).emb z
show Algebra.adjoin.liftSingleton N x y hy (@algebraMap N O _ _ (Subalgebra.algebra O) z) =
    algebraMap N M z
no goals
k : Type u
inst✝⁶ : Field k
K : Type u
L : Type v
M : Type w
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Field M
inst✝¹ : Algebra K M
inst✝ : IsAlgClosed M
hL : Algebra.IsAlgebraic K L
E₁ E₂ E₃ : SubfieldWithHom K L M
x : L
a✝ : x ∈ ⊤
N : Subalgebra K L := (maximalSubfieldWithHom K L M).carrier
this✝¹ : Field { x // x ∈ N } := IsField.toField (_ : IsField { x // x ∈ N })
this✝ : Algebra { x // x ∈ N } M := RingHom.toAlgebra ↑(maximalSubfieldWithHom K L M).emb
y : M
hy : ↑(aeval y) (minpoly { x // x ∈ N } x) = 0
O : Subalgebra { x // x ∈ N } L := Algebra.adjoin { x // x ∈ N } {x}
this : Algebra { x // x ∈ N } { x // x ∈ O } := Subalgebra.algebra O
larger_emb : { x // x ∈ O } →ₐ[{ x // x ∈ N }] M := Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy
larger_emb' : { x // x ∈ O } →ₐ[K] M := AlgHom.restrictScalars K larger_emb
hNO : N ≤ Subalgebra.restrictScalars K O
O' : SubfieldWithHom K L M := { carrier := Subalgebra.restrictScalars K O, emb := larger_emb' }
z : { x // x ∈ (maximalSubfieldWithHom K L M).carrier }
⊢ ↑(Algebra.adjoin.liftSingleton { x // x ∈ N } x y hy) (↑(algebraMap { x // x ∈ N } { x // x ∈ O }) z) =
    ↑(algebraMap { x // x ∈ N } M) z
exact AlgHom.commutes _ _