[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
⊢ x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}
[PROOFSTEP]
dsimp
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
⊢ x ∈
    Polynomial.roots
      (Polynomial.map (algebraMap R L)
        ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
            (_ : _root_.IsAlgebraic R x)))
[PROOFSTEP]
have h : p.1.map (algebraMap R L) ≠ 0 :=
  by
  rw [Ne.def, ← Polynomial.degree_eq_bot,
    Polynomial.degree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective R L), Polynomial.degree_eq_bot]
  exact p.2.1
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
⊢ Polynomial.map (algebraMap R L) ↑p ≠ 0
[PROOFSTEP]
rw [Ne.def, ← Polynomial.degree_eq_bot,
  Polynomial.degree_map_eq_of_injective (NoZeroSMulDivisors.algebraMap_injective R L), Polynomial.degree_eq_bot]
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
⊢ ¬↑p = 0
[PROOFSTEP]
exact p.2.1
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x : L
p : { x_1 // x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0 } :=
  Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0) (_ : _root_.IsAlgebraic R x)
h : Polynomial.map (algebraMap R L) ↑p ≠ 0
⊢ x ∈
    Polynomial.roots
      (Polynomial.map (algebraMap R L)
        ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
            (_ : _root_.IsAlgebraic R x)))
[PROOFSTEP]
erw [Polynomial.mem_roots h, Polynomial.IsRoot, Polynomial.eval_map, ← Polynomial.aeval_def, p.2.2]
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x y : L
⊢ (fun x =>
          let p :=
            Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
              (_ : _root_.IsAlgebraic R x);
          { fst := ↑p,
            snd :=
              { val := x, property := (_ : x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}) } })
        x =
      (fun x =>
          let p :=
            Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
              (_ : _root_.IsAlgebraic R x);
          { fst := ↑p,
            snd :=
              { val := x, property := (_ : x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}) } })
        y →
    x = y
[PROOFSTEP]
intro h
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x y : L
h :
  (fun x =>
        let p :=
          Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
            (_ : _root_.IsAlgebraic R x);
        { fst := ↑p,
          snd :=
            { val := x, property := (_ : x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}) } })
      x =
    (fun x =>
        let p :=
          Classical.indefiniteDescription (fun x_1 => x_1 ≠ 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
            (_ : _root_.IsAlgebraic R x);
        { fst := ↑p,
          snd :=
            { val := x, property := (_ : x ∈ {x_1 | x_1 ∈ Polynomial.roots (Polynomial.map (algebraMap R L) ↑p)}) } })
      y
⊢ x = y
[PROOFSTEP]
simp at h
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x y : L
h :
  ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
          (_ : _root_.IsAlgebraic R x)) =
      ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ ↑(Polynomial.aeval y) x = 0) (_ : _root_.IsAlgebraic R y)) ∧
    HEq
      { val := x,
        property :=
          (_ :
            x ∈
              {x_1 |
                x_1 ∈
                  Polynomial.roots
                    (Polynomial.map (algebraMap R L)
                      ↑(Classical.indefiniteDescription (fun x_2 => x_2 ≠ 0 ∧ ↑(Polynomial.aeval x) x_2 = 0)
                          (_ : _root_.IsAlgebraic R x)))}) }
      { val := y,
        property :=
          (_ :
            y ∈
              {x |
                x ∈
                  Polynomial.roots
                    (Polynomial.map (algebraMap R L)
                      ↑(Classical.indefiniteDescription (fun x => x ≠ 0 ∧ ↑(Polynomial.aeval y) x = 0)
                          (_ : _root_.IsAlgebraic R y)))}) }
⊢ x = y
[PROOFSTEP]
refine' (Subtype.heq_iff_coe_eq _).1 h.2
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
x y : L
h :
  ↑(Classical.indefiniteDescription (fun x_1 => ¬x_1 = 0 ∧ ↑(Polynomial.aeval x) x_1 = 0)
          (_ : _root_.IsAlgebraic R x)) =
      ↑(Classical.indefiniteDescription (fun x => ¬x = 0 ∧ ↑(Polynomial.aeval y) x = 0) (_ : _root_.IsAlgebraic R y)) ∧
    HEq
      { val := x,
        property :=
          (_ :
            x ∈
              {x_1 |
                x_1 ∈
                  Polynomial.roots
                    (Polynomial.map (algebraMap R L)
                      ↑(Classical.indefiniteDescription (fun x_2 => x_2 ≠ 0 ∧ ↑(Polynomial.aeval x) x_2 = 0)
                          (_ : _root_.IsAlgebraic R x)))}) }
      { val := y,
        property :=
          (_ :
            y ∈
              {x |
                x ∈
                  Polynomial.roots
                    (Polynomial.map (algebraMap R L)
                      ↑(Classical.indefiniteDescription (fun x => x ≠ 0 ∧ ↑(Polynomial.aeval y) x = 0)
                          (_ : _root_.IsAlgebraic R y)))}) }
⊢ ∀ (x_1 : L),
    x_1 ∈
        {x_2 |
          x_2 ∈
            Polynomial.roots
              (Polynomial.map (algebraMap R L)
                ↑(Classical.indefiniteDescription (fun x_3 => x_3 ≠ 0 ∧ ↑(Polynomial.aeval x) x_3 = 0)
                    (_ : _root_.IsAlgebraic R x)))} ↔
      x_1 ∈
        {x |
          x ∈
            Polynomial.roots
              (Polynomial.map (algebraMap R L)
                ↑(Classical.indefiniteDescription (fun x => x ≠ 0 ∧ ↑(Polynomial.aeval y) x = 0)
                    (_ : _root_.IsAlgebraic R y)))}
[PROOFSTEP]
simp only [h.1, iff_self_iff, forall_true_iff]
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p) }) =
    sum fun p => #↑{x | x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p)}
[PROOFSTEP]
rw [← mk_sigma]
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) p) }) =
    #((i : R[X]) × ↑{x | x ∈ Polynomial.roots (Polynomial.map (algebraMap R L) i)})
[PROOFSTEP]
rfl
[GOAL]
R L : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing L
inst✝² : IsDomain L
inst✝¹ : Algebra R L
inst✝ : NoZeroSMulDivisors R L
halg : IsAlgebraic R L
⊢ max (max (max #R ℵ₀) ℵ₀) ℵ₀ = max #R ℵ₀
[PROOFSTEP]
simp only [max_assoc, max_comm ℵ₀, max_left_comm ℵ₀, max_self]
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : Field L
inst✝¹ : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
inst✝ : IsAlgClosed K
hv : IsTranscendenceBasis R v
this : Nontrivial R := RingHom.domain_nontrivial (algebraMap R K)
⊢ IsAlgClosed K
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
⊢ K ≃+* L
[PROOFSTEP]
letI := isAlgClosure_of_transcendence_basis v hv
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
⊢ K ≃+* L
[PROOFSTEP]
letI := isAlgClosure_of_transcendence_basis w hw
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ K ≃+* L
[PROOFSTEP]
have e : Algebra.adjoin R (Set.range v) ≃+* Algebra.adjoin R (Set.range w)
[GOAL]
case e
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ { x // x ∈ Algebra.adjoin R (Set.range v) } ≃+* { x // x ∈ Algebra.adjoin R (Set.range w) }
[PROOFSTEP]
refine' hv.1.aevalEquiv.symm.toRingEquiv.trans _
[GOAL]
case e
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ MvPolynomial ι R ≃+* { x // x ∈ Algebra.adjoin R (Set.range w) }
[PROOFSTEP]
refine' (AlgEquiv.ofAlgHom (MvPolynomial.rename e) (MvPolynomial.rename e.symm) _ _).toRingEquiv.trans _
[GOAL]
case e.refine'_1
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ AlgHom.comp (MvPolynomial.rename ↑e) (MvPolynomial.rename ↑e.symm) = AlgHom.id R (MvPolynomial κ R)
[PROOFSTEP]
ext
[GOAL]
case e.refine'_1.hf.a
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
i✝ : κ
m✝ : κ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(AlgHom.comp (MvPolynomial.rename ↑e) (MvPolynomial.rename ↑e.symm)) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ (↑(AlgHom.id R (MvPolynomial κ R)) (MvPolynomial.X i✝))
[PROOFSTEP]
simp
[GOAL]
case e.refine'_2
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ AlgHom.comp (MvPolynomial.rename ↑e.symm) (MvPolynomial.rename ↑e) = AlgHom.id R (MvPolynomial ι R)
[PROOFSTEP]
ext
[GOAL]
case e.refine'_2.hf.a
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
i✝ : ι
m✝ : ι →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑(AlgHom.comp (MvPolynomial.rename ↑e.symm) (MvPolynomial.rename ↑e)) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ (↑(AlgHom.id R (MvPolynomial ι R)) (MvPolynomial.X i✝))
[PROOFSTEP]
simp
[GOAL]
case e.refine'_3
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
⊢ MvPolynomial κ R ≃+* { x // x ∈ Algebra.adjoin R (Set.range w) }
[PROOFSTEP]
exact hw.1.aevalEquiv.toRingEquiv
[GOAL]
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e✝ : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range v) } K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure { x // x ∈ Algebra.adjoin R (Set.range w) } L := isAlgClosure_of_transcendence_basis w hw
e : { x // x ∈ Algebra.adjoin R (Set.range v) } ≃+* { x // x ∈ Algebra.adjoin R (Set.range w) }
⊢ K ≃+* L
[PROOFSTEP]
exact IsAlgClosure.equivOfEquiv K L e
[GOAL]
R L K : Type u
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ hv : IsTranscendenceBasis R v
⊢ max #{ x // x ∈ Algebra.adjoin R (Set.range v) } ℵ₀ = max #(MvPolynomial ι R) ℵ₀
[PROOFSTEP]
rw [Cardinal.eq.2 ⟨hv.1.aevalEquiv.toEquiv⟩]
[GOAL]
R L K : Type u
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ hv : IsTranscendenceBasis R v
⊢ max (max (max #R #ι) ℵ₀) ℵ₀ = max (max #R #ι) ℵ₀
[PROOFSTEP]
simp [max_assoc]
[GOAL]
R L K : Type u
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ #ι
⊢ max (max #R #ι) ℵ₀ = #ι
[PROOFSTEP]
rw [max_eq_left, max_eq_right]
[GOAL]
R L K : Type u
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ #ι
⊢ #R ≤ #ι
[PROOFSTEP]
exact le_trans hR this
[GOAL]
R L K : Type u
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type u
v : ι → K
hv✝ : IsTranscendenceBasis R v
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ #ι
⊢ ℵ₀ ≤ max #R #ι
[PROOFSTEP]
exact le_max_of_le_right this
[GOAL]
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases' exists_isTranscendenceBasis ℤ (show Function.Injective (algebraMap ℤ K) from Int.cast_injective) with s hs
[GOAL]
case intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases' exists_isTranscendenceBasis ℤ (show Function.Injective (algebraMap ℤ L) from Int.cast_injective) with t ht
[GOAL]
case intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
have : #s = #t :=
  by
  rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (le_of_eq mk_int) hK, ←
    cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (le_of_eq mk_int), hKL]
  rwa [← hKL]
[GOAL]
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ #↑s = #↑t
[PROOFSTEP]
rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (le_of_eq mk_int) hK, ←
  cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (le_of_eq mk_int), hKL]
[GOAL]
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ ℵ₀ < #L
[PROOFSTEP]
rwa [← hKL]
[GOAL]
case intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
this : #↑s = #↑t
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases' Cardinal.eq.1 this with e
[GOAL]
case intro.intro.intro
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : #K = #L
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
this : #↑s = #↑t
e : ↑s ≃ ↑t
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
letI : Algebra (ZMod p) K := ZMod.algebra _ _
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this : Algebra (ZMod p) K := ZMod.algebra K p
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
letI : Algebra (ZMod p) L := ZMod.algebra _ _
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases'
  exists_isTranscendenceBasis (ZMod p) (show Function.Injective (algebraMap (ZMod p) K) from RingHom.injective _) with s
  hs
[GOAL]
case intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases'
  exists_isTranscendenceBasis (ZMod p) (show Function.Injective (algebraMap (ZMod p) L) from RingHom.injective _) with t
  ht
[GOAL]
case intro.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
have : #s = #t :=
  by
  rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (lt_aleph0_of_finite (ZMod p)).le hK, ←
    cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (lt_aleph0_of_finite (ZMod p)).le, hKL]
  rwa [← hKL]
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ #↑s = #↑t
[PROOFSTEP]
rw [← cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ hs (lt_aleph0_of_finite (ZMod p)).le hK, ←
  cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _ ht (lt_aleph0_of_finite (ZMod p)).le, hKL]
[GOAL]
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ ℵ₀ < #L
[PROOFSTEP]
rwa [← hKL]
[GOAL]
case intro.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝¹ : Algebra (ZMod p) K := ZMod.algebra K p
this✝ : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
this : #↑s = #↑t
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
cases' Cardinal.eq.1 this with e
[GOAL]
case intro.intro.intro
K L : Type
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
this✝¹ : Algebra (ZMod p) K := ZMod.algebra K p
this✝ : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
this : #↑s = #↑t
e : ↑s ≃ ↑t
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
exact ⟨equivOfTranscendenceBasis _ _ e hs ht⟩
[GOAL]
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
rcases CharP.char_is_prime_or_zero K p with (hp | hp)
[GOAL]
case inl
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
hp : Nat.Prime p
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
haveI : Fact p.Prime := ⟨hp⟩
[GOAL]
case inl
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
hp : Nat.Prime p
this : Fact (Nat.Prime p)
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
exact ringEquivOfCardinalEqOfCharP p hK hKL
[GOAL]
case inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : #K = #L
hp : p = 0
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
simp only [hp] at *
[GOAL]
case inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : #K = #L
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
letI : CharZero K := CharP.charP_to_charZero K
[GOAL]
case inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : #K = #L
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
this : CharZero K := CharP.charP_to_charZero K
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
letI : CharZero L := CharP.charP_to_charZero L
[GOAL]
case inr
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
hK : ℵ₀ < #K
hKL : #K = #L
inst✝¹ : CharP K 0
inst✝ : CharP L 0
hp : True
this✝ : CharZero K := CharP.charP_to_charZero K
this : CharZero L := CharP.charP_to_charZero L
⊢ Nonempty (K ≃+* L)
[PROOFSTEP]
exact ringEquivOfCardinalEqOfCharZero hK hKL


[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
⊢ ↑(taylor r) p ∈ R[X]⁰
[PROOFSTEP]
rw [mem_nonZeroDivisors_iff]
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
⊢ ∀ (x : (fun x => R[X]) p), x * ↑(taylor r) p = 0 → x = 0
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
x : R[X]
hx : x * ↑(taylor r) p = 0
⊢ x = 0
[PROOFSTEP]
have : x = taylor (r - r) x := by simp
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
x : R[X]
hx : x * ↑(taylor r) p = 0
⊢ x = ↑(taylor (r - r)) x
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
hp : p ∈ R[X]⁰
x : R[X]
hx : x * ↑(taylor r) p = 0
this : x = ↑(taylor (r - r)) x
⊢ x = 0
[PROOFSTEP]
rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul, LinearMap.map_eq_zero_iff _ (taylor_injective _),
  mul_right_mem_nonZeroDivisors_eq_zero_iff hp, LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ R[X]⁰ ≤
    Submonoid.comap
      {
        toMonoidHom :=
          { toOneHom := { toFun := ↑(taylor r), map_one' := (_ : ↑(taylor r) 1 = ↑Polynomial.C 1) },
            map_mul' := (_ : ∀ (p q : R[X]), ↑(taylor r) (p * q) = ↑(taylor r) p * ↑(taylor r) q) },
        map_zero' := (_ : ↑(taylor r) 0 = 0),
        map_add' := (_ : ∀ (x y : R[X]), ↑(taylor r) (x + y) = ↑(taylor r) x + ↑(taylor r) y) }
      R[X]⁰
[PROOFSTEP]
exact taylor_mem_nonZeroDivisors r
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ ↑(laurentAux r) (↑(algebraMap R[X] (RatFunc R)) p) = ↑(algebraMap ((fun x => R[X]) p) (RatFunc R)) (↑(taylor r) p)
[PROOFSTEP]
rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one, map_one]
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ ↑(laurent r) X = X + ↑C r
[PROOFSTEP]
rw [← algebraMap_X, laurent_algebraMap, taylor_X, _root_.map_add, algebraMap_C]
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
x : R
⊢ ↑(laurent r) (↑C x) = ↑C x
[PROOFSTEP]
rw [← algebraMap_C, laurent_algebraMap, taylor_C]
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ ↑(laurent 0) f = f
[PROOFSTEP]
induction f using RatFunc.induction_on
[GOAL]
case f
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
p✝ q✝ : R[X]
hq✝ : q✝ ≠ 0
⊢ ↑(laurent 0) (↑(algebraMap R[X] (RatFunc R)) p✝ / ↑(algebraMap R[X] (RatFunc R)) q✝) =
    ↑(algebraMap R[X] (RatFunc R)) p✝ / ↑(algebraMap R[X] (RatFunc R)) q✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
⊢ ↑(laurent r) (↑(laurent s) f) = ↑(laurent (r + s)) f
[PROOFSTEP]
induction f using RatFunc.induction_on
[GOAL]
case f
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f : RatFunc R
p✝ q✝ : R[X]
hq✝ : q✝ ≠ 0
⊢ ↑(laurent r) (↑(laurent s) (↑(algebraMap R[X] (RatFunc R)) p✝ / ↑(algebraMap R[X] (RatFunc R)) q✝)) =
    ↑(laurent (r + s)) (↑(algebraMap R[X] (RatFunc R)) p✝ / ↑(algebraMap R[X] (RatFunc R)) q✝)
[PROOFSTEP]
simp_rw [laurent_div, taylor_taylor]
[GOAL]
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f x✝¹ x✝ : RatFunc R
h : ↑(laurent r) x✝¹ = ↑(laurent r) x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
simpa [laurent_laurent] using congr_arg (laurent (-r)) h


[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ fixingSubgroup ⊥ = ⊤
[PROOFSTEP]
ext f
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
⊢ f ∈ fixingSubgroup ⊥ ↔ f ∈ ⊤
[PROOFSTEP]
refine' ⟨fun _ => Subgroup.mem_top _, fun _ => _⟩
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
⊢ f ∈ fixingSubgroup ⊥
[PROOFSTEP]
rintro ⟨x, hx : x ∈ (⊥ : IntermediateField K L)⟩
[GOAL]
case h.mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
x : L
hx : x ∈ ⊥
⊢ f • ↑{ val := x, property := hx } = ↑{ val := x, property := hx }
[PROOFSTEP]
rw [IntermediateField.mem_bot] at hx
[GOAL]
case h.mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
x : L
hx✝ : x ∈ ⊥
hx : x ∈ Set.range ↑(algebraMap K L)
⊢ f • ↑{ val := x, property := hx✝ } = ↑{ val := x, property := hx✝ }
[PROOFSTEP]
rcases hx with ⟨y, rfl⟩
[GOAL]
case h.mk.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
f : L ≃ₐ[K] L
x✝ : f ∈ ⊤
y : K
hx : ↑(algebraMap K L) y ∈ ⊥
⊢ f • ↑{ val := ↑(algebraMap K L) y, property := hx } = ↑{ val := ↑(algebraMap K L) y, property := hx }
[PROOFSTEP]
exact f.commutes y
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h12 : E1 ≤ E2
⊢ fixingSubgroup E2 ≤ fixingSubgroup E1
[PROOFSTEP]
rintro σ hσ ⟨x, hx⟩
[GOAL]
case mk
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 E2 : IntermediateField K L
h12 : E1 ≤ E2
σ : L ≃ₐ[K] L
hσ : σ ∈ fixingSubgroup E2
x : L
hx : x ∈ ↑E1
⊢ σ • ↑{ val := x, property := hx } = ↑{ val := x, property := hx }
[PROOFSTEP]
exact hσ ⟨x, h12 hx⟩
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ ∀ {x y : Set (L ≃ₐ[K] L)},
    x ∈ (fun g => g.carrier) '' fixedByFinite K L →
      y ∈ (fun g => g.carrier) '' fixedByFinite K L → ∃ z, z ∈ (fun g => g.carrier) '' fixedByFinite K L ∧ z ⊆ x ∩ y
[PROOFSTEP]
rintro X Y ⟨H1, ⟨E1, h_E1, rfl⟩, rfl⟩ ⟨H2, ⟨E2, h_E2, rfl⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
⊢ ∃ z,
    z ∈ (fun g => g.carrier) '' fixedByFinite K L ∧
      z ⊆
        (fun g => g.carrier) (IntermediateField.fixingSubgroup E1) ∩
          (fun g => g.carrier) (IntermediateField.fixingSubgroup E2)
[PROOFSTEP]
use(IntermediateField.fixingSubgroup (E1 ⊔ E2)).carrier
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
⊢ (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ∈
      (fun g => g.carrier) '' fixedByFinite K L ∧
    (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ⊆
      (fun g => g.carrier) (IntermediateField.fixingSubgroup E1) ∩
        (fun g => g.carrier) (IntermediateField.fixingSubgroup E2)
[PROOFSTEP]
refine' ⟨⟨_, ⟨_, finiteDimensional_sup E1 E2 h_E1 h_E2, rfl⟩, rfl⟩, _⟩
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
⊢ (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ⊆
    (fun g => g.carrier) (IntermediateField.fixingSubgroup E1) ∩
      (fun g => g.carrier) (IntermediateField.fixingSubgroup E2)
[PROOFSTEP]
rw [Set.subset_inter_iff]
[GOAL]
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
E1 : IntermediateField K L
h_E1 : E1 ∈ finiteExts K L
E2 : IntermediateField K L
h_E2 : E2 ∈ finiteExts K L
⊢ (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ⊆
      (fun g => g.carrier) (IntermediateField.fixingSubgroup E1) ∧
    (IntermediateField.fixingSubgroup (E1 ⊔ E2)).toSubmonoid.toSubsemigroup.carrier ⊆
      (fun g => g.carrier) (IntermediateField.fixingSubgroup E2)
[PROOFSTEP]
exact ⟨IntermediateField.fixingSubgroup.antimono le_sup_left, IntermediateField.fixingSubgroup.antimono le_sup_right⟩
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
U : Set (L ≃ₐ[K] L)
hU : U ∈ (galBasis K L).sets
⊢ U * U ⊆ U
[PROOFSTEP]
rcases hU with ⟨H, _, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : Subgroup (L ≃ₐ[K] L)
left✝ : H ∈ fixedByFinite K L
⊢ (fun g => g.carrier) H * (fun g => g.carrier) H ⊆ (fun g => g.carrier) H
[PROOFSTEP]
rintro x ⟨a, b, haH, hbH, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : Subgroup (L ≃ₐ[K] L)
left✝ : H ∈ fixedByFinite K L
a b : L ≃ₐ[K] L
haH : a ∈ (fun g => g.carrier) H
hbH : b ∈ (fun g => g.carrier) H
⊢ (fun x x_1 => x * x_1) a b ∈ (fun g => g.carrier) H
[PROOFSTEP]
exact H.mul_mem haH hbH
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
U : Set (L ≃ₐ[K] L)
hU : U ∈ (galBasis K L).sets
⊢ U ⊆ (fun x => x⁻¹) ⁻¹' U
[PROOFSTEP]
rcases hU with ⟨H, _, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : Subgroup (L ≃ₐ[K] L)
left✝ : H ∈ fixedByFinite K L
⊢ (fun g => g.carrier) H ⊆ (fun x => x⁻¹) ⁻¹' (fun g => g.carrier) H
[PROOFSTEP]
exact fun _ => H.inv_mem'
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ ∀ (x₀ : L ≃ₐ[K] L) {U : Set (L ≃ₐ[K] L)},
    U ∈ (galBasis K L).sets → ∃ V, V ∈ (galBasis K L).sets ∧ V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U
[PROOFSTEP]
rintro σ U ⟨H, ⟨E, hE, rfl⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
⊢ ∃ V,
    V ∈ (galBasis K L).sets ∧ V ⊆ (fun x => σ * x * σ⁻¹) ⁻¹' (fun g => g.carrier) (IntermediateField.fixingSubgroup E)
[PROOFSTEP]
let F : IntermediateField K L := E.map σ.symm.toAlgHom
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
⊢ ∃ V,
    V ∈ (galBasis K L).sets ∧ V ⊆ (fun x => σ * x * σ⁻¹) ⁻¹' (fun g => g.carrier) (IntermediateField.fixingSubgroup E)
[PROOFSTEP]
refine' ⟨F.fixingSubgroup.carrier, ⟨⟨F.fixingSubgroup, ⟨F, _, rfl⟩, rfl⟩, fun g hg => _⟩⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
⊢ F ∈ finiteExts K L
[PROOFSTEP]
have : FiniteDimensional K E := hE
[GOAL]
case intro.intro.intro.intro.refine'_1
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
this : FiniteDimensional K { x // x ∈ E }
⊢ F ∈ finiteExts K L
[PROOFSTEP]
apply im_finiteDimensional σ.symm
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
⊢ g ∈ (fun x => σ * x * σ⁻¹) ⁻¹' (fun g => g.carrier) (IntermediateField.fixingSubgroup E)
[PROOFSTEP]
change σ * g * σ⁻¹ ∈ E.fixingSubgroup
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
⊢ σ * g * σ⁻¹ ∈ IntermediateField.fixingSubgroup E
[PROOFSTEP]
rw [IntermediateField.mem_fixingSubgroup_iff]
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
⊢ ∀ (x : L), x ∈ E → ↑(σ * g * σ⁻¹) x = x
[PROOFSTEP]
intro x hx
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ ↑(σ * g * σ⁻¹) x = x
[PROOFSTEP]
change σ (g (σ⁻¹ x)) = x
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ ↑σ (↑g (↑σ⁻¹ x)) = x
[PROOFSTEP]
have h_in_F : σ⁻¹ x ∈ F := ⟨x, hx, by dsimp; rw [← AlgEquiv.invFun_eq_symm]; rfl⟩
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ ↑↑↑(AlgEquiv.symm σ) x = ↑σ⁻¹ x
[PROOFSTEP]
dsimp
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ ↑(AlgEquiv.symm σ) x = ↑σ⁻¹ x
[PROOFSTEP]
rw [← AlgEquiv.invFun_eq_symm]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
⊢ Equiv.invFun σ.toEquiv x = ↑σ⁻¹ x
[PROOFSTEP]
rfl
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
⊢ ↑σ (↑g (↑σ⁻¹ x)) = x
[PROOFSTEP]
have h_g_fix : g (σ⁻¹ x) = σ⁻¹ x :=
  by
  rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg
  exact hg (σ⁻¹ x) h_in_F
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
⊢ ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
[PROOFSTEP]
rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : ∀ (x : L), x ∈ F → ↑g x = x
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
⊢ ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
[PROOFSTEP]
exact hg (σ⁻¹ x) h_in_F
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
h_g_fix : ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
⊢ ↑σ (↑g (↑σ⁻¹ x)) = x
[PROOFSTEP]
rw [h_g_fix]
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
h_g_fix : ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
⊢ ↑σ (↑σ⁻¹ x) = x
[PROOFSTEP]
change σ (σ⁻¹ x) = x
[GOAL]
case intro.intro.intro.intro.refine'_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
σ : L ≃ₐ[K] L
E : IntermediateField K L
hE : E ∈ finiteExts K L
F : IntermediateField K L := IntermediateField.map (↑(AlgEquiv.symm σ)) E
g : L ≃ₐ[K] L
hg : g ∈ (IntermediateField.fixingSubgroup F).toSubmonoid.toSubsemigroup.carrier
x : L
hx : x ∈ E
h_in_F : ↑σ⁻¹ x ∈ F
h_g_fix : ↑g (↑σ⁻¹ x) = ↑σ⁻¹ x
⊢ ↑σ (↑σ⁻¹ x) = x
[PROOFSTEP]
exact AlgEquiv.apply_symm_apply σ x
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K { x // x ∈ E }
⊢ IsOpen ↑(fixingSubgroup E)
[PROOFSTEP]
have h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L := ⟨E.fixingSubgroup, ⟨E, ‹_›, rfl⟩, rfl⟩
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K { x // x ∈ E }
h_basis : (fixingSubgroup E).toSubmonoid.toSubsemigroup.carrier ∈ galGroupBasis K L
⊢ IsOpen ↑(fixingSubgroup E)
[PROOFSTEP]
have h_nhd := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
[GOAL]
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : FiniteDimensional K { x // x ∈ E }
h_basis : (fixingSubgroup E).toSubmonoid.toSubsemigroup.carrier ∈ galGroupBasis K L
h_nhd : (fixingSubgroup E).toSubmonoid.toSubsemigroup.carrier ∈ 𝓝 1
⊢ IsOpen ↑(fixingSubgroup E)
[PROOFSTEP]
exact Subgroup.isOpen_of_mem_nhds _ h_nhd
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
let φ := f⁻¹ * g
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
cases' FunLike.exists_ne hfg with x hx
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
have hφx : φ x ≠ x := by
  apply ne_of_apply_ne f
  change f (f.symm (g x)) ≠ f x
  rw [AlgEquiv.apply_symm_apply f (g x), ne_comm]
  exact hx
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
⊢ ↑φ x ≠ x
[PROOFSTEP]
apply ne_of_apply_ne f
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
⊢ ↑f (↑φ x) ≠ ↑f x
[PROOFSTEP]
change f (f.symm (g x)) ≠ f x
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
⊢ ↑f (↑(AlgEquiv.symm f) (↑g x)) ≠ ↑f x
[PROOFSTEP]
rw [AlgEquiv.apply_symm_apply f (g x), ne_comm]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
⊢ ↑f x ≠ ↑g x
[PROOFSTEP]
exact hx
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
let E : IntermediateField K L := IntermediateField.adjoin K { x }
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
let h_findim : FiniteDimensional K E := IntermediateField.adjoin.finiteDimensional (h_int x)
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
let H := E.fixingSubgroup
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
have h_basis : (H : Set (L ≃ₐ[K] L)) ∈ galGroupBasis K L := ⟨H, ⟨E, ⟨h_findim, rfl⟩⟩, rfl⟩
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
have h_nhd := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
h_nhd : ↑H ∈ 𝓝 1
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
rw [mem_nhds_iff] at h_nhd
[GOAL]
case intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
h_nhd : ∃ t, t ⊆ ↑H ∧ IsOpen t ∧ 1 ∈ t
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
rcases h_nhd with ⟨W, hWH, hW_open, hW_1⟩
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
refine'
  ⟨leftCoset f W, leftCoset g W,
    ⟨hW_open.leftCoset f, hW_open.leftCoset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, _⟩⟩
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
⊢ Disjoint (leftCoset f W) (leftCoset g W)
[PROOFSTEP]
rw [Set.disjoint_left]
[GOAL]
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
⊢ ∀ ⦃a : L ≃ₐ[K] L⦄, a ∈ leftCoset f W → ¬a ∈ leftCoset g W
[PROOFSTEP]
rintro σ ⟨w1, hw1, h⟩ ⟨w2, hw2, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : (fun x => f * x) w1 = (fun x => g * x) w2
⊢ False
[PROOFSTEP]
rw [eq_inv_mul_iff_mul_eq.symm, ← mul_assoc, mul_inv_eq_iff_eq_mul.symm] at h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
⊢ False
[PROOFSTEP]
have h_in_H : w1 * w2⁻¹ ∈ H := H.mul_mem (hWH hw1) (H.inv_mem (hWH hw2))
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : w1 * w2⁻¹ ∈ H
⊢ False
[PROOFSTEP]
rw [h] at h_in_H
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : f⁻¹ * g ∈ H
⊢ False
[PROOFSTEP]
change φ ∈ E.fixingSubgroup at h_in_H
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : φ ∈ IntermediateField.fixingSubgroup E
⊢ False
[PROOFSTEP]
rw [IntermediateField.mem_fixingSubgroup_iff] at h_in_H
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : ∀ (x : L), x ∈ E → ↑φ x = x
⊢ False
[PROOFSTEP]
specialize h_in_H x
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → ↑φ x = x
⊢ False
[PROOFSTEP]
have hxE : x ∈ E := by
  apply IntermediateField.subset_adjoin
  apply Set.mem_singleton
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → ↑φ x = x
⊢ x ∈ E
[PROOFSTEP]
apply IntermediateField.subset_adjoin
[GOAL]
case a
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → ↑φ x = x
⊢ x ∈ {x}
[PROOFSTEP]
apply Set.mem_singleton
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
f g : L ≃ₐ[K] L
hfg : f ≠ g
φ : L ≃ₐ[K] L := f⁻¹ * g
x : L
hx : ↑f x ≠ ↑g x
hφx : ↑φ x ≠ x
E : IntermediateField K L := K⟮x⟯
h_findim : FiniteDimensional K { x // x ∈ E } := IntermediateField.adjoin.finiteDimensional (h_int x)
H : Subgroup (L ≃ₐ[K] L) := IntermediateField.fixingSubgroup E
h_basis : ↑H ∈ galGroupBasis K L
W : Set (L ≃ₐ[K] L)
hWH : W ⊆ ↑H
hW_open : IsOpen W
hW_1 : 1 ∈ W
w1 : L ≃ₐ[K] L
hw1 : w1 ∈ W
w2 : L ≃ₐ[K] L
hw2 : w2 ∈ W
h : w1 * w2⁻¹ = f⁻¹ * g
h_in_H : x ∈ E → ↑φ x = x
hxE : x ∈ E
⊢ False
[PROOFSTEP]
exact hφx (h_in_H hxE)
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
⊢ IsTotallyDisconnected Set.univ
[PROOFSTEP]
apply isTotallyDisconnected_of_clopen_set
[GOAL]
case hX
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
⊢ Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ ¬y ∈ U
[PROOFSTEP]
intro σ τ h_diff
[GOAL]
case hX
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne.def, inv_mul_eq_one]
[GOAL]
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
⊢ σ⁻¹ * τ ≠ 1
[PROOFSTEP]
rwa [Ne.def, inv_mul_eq_one]
[GOAL]
case hX
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
rcases FunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
let E := IntermediateField.adjoin K ({ x } : Set L)
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
haveI := IntermediateField.adjoin.finiteDimensional (h_int x)
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K { x_1 // x_1 ∈ K⟮x⟯ }
⊢ ∃ U, IsClopen U ∧ σ ∈ U ∧ ¬τ ∈ U
[PROOFSTEP]
refine'
  ⟨leftCoset σ E.fixingSubgroup, ⟨E.fixingSubgroup_isOpen.leftCoset σ, E.fixingSubgroup_isClosed.leftCoset σ⟩,
    ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, _⟩
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K { x_1 // x_1 ∈ K⟮x⟯ }
⊢ ¬τ ∈ leftCoset σ ↑(IntermediateField.fixingSubgroup E)
[PROOFSTEP]
simp only [mem_leftCoset_iff, SetLike.mem_coe, IntermediateField.mem_fixingSubgroup_iff, not_forall]
[GOAL]
case hX.intro
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h_int : Algebra.IsIntegral K L
σ τ : L ≃ₐ[K] L
h_diff : σ ≠ τ
hστ : σ⁻¹ * τ ≠ 1
x : L
hx : ↑(σ⁻¹ * τ) x ≠ x
E : IntermediateField K L := K⟮x⟯
this : FiniteDimensional K { x_1 // x_1 ∈ K⟮x⟯ }
⊢ ∃ x_1 x, ¬↑(σ⁻¹ * τ) x_1 = x_1
[PROOFSTEP]
exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩