Theorem: IsSeparable_of_isLocalization (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
⊢ IsSeparable Rₚ Sₚ
Tactic:
have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
  (algebraMap R S) (Submonoid.le_comap_map M) := by
  apply IsLocalization.ringHom_ext M
  simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
State after:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ IsSeparable Rₚ Sₚ

State before:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ IsSeparable Rₚ Sₚ
Tactic:
refine ⟨fun x ↦ ?_⟩
State after:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : Sₚ
⊢ (minpoly Rₚ x).Separable

State before:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : Sₚ
⊢ (minpoly Rₚ x).Separable
Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid S M) x
State after:
case intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
⊢ (minpoly Rₚ (IsLocalization.mk' Sₚ x s)).Separable

State before:
case intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
⊢ (minpoly Rₚ (IsLocalization.mk' Sₚ x s)).Separable
Tactic:
obtain ⟨t, ht, e⟩ := s.prop
State after:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
⊢ (minpoly Rₚ (IsLocalization.mk' Sₚ x s)).Separable

State before:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
⊢ (minpoly Rₚ (IsLocalization.mk' Sₚ x s)).Separable
Tactic:
let P := ((minpoly R x).map (algebraMap R Rₚ)).scaleRoots (IsLocalization.mk' _ 1 ⟨t, ht⟩)
State after:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ (minpoly Rₚ (IsLocalization.mk' Sₚ x s)).Separable

State before:
case intro.intro.intro.intro
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ (minpoly Rₚ (IsLocalization.mk' Sₚ x s)).Separable
Tactic:
refine Separable.of_dvd ?_ (minpoly.dvd _ (p := P) ?_)
State after:
case intro.intro.intro.intro.refine_1
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ P.Separable

case intro.intro.intro.intro.refine_2
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ (aeval (IsLocalization.mk' Sₚ x s)) P = 0

State before:
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
⊢ algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
Tactic:
apply IsLocalization.ringHom_ext M
State after:
case h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)

State before:
case h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (IsLocalization.map Sₚ (algebraMap R S) ⋯).comp (algebraMap R Rₚ)
Tactic:
simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
State after:
no goals

State before:
case intro.intro.intro.intro.refine_1
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ P.Separable
Tactic:
apply (IsSeparable.separable R x).map.scaleRoots
State after:
case intro.intro.intro.intro.refine_1.hr
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ IsUnit (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)

State before:
case intro.intro.intro.intro.refine_1.hr
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ IsUnit (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
Tactic:
exact isUnit_of_invertible _
State after:
no goals

State before:
case intro.intro.intro.intro.refine_2
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ (aeval (IsLocalization.mk' Sₚ x s)) P = 0
Tactic:
rw [aeval_def]
State after:
case intro.intro.intro.intro.refine_2
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ eval₂ (algebraMap Rₚ Sₚ) (IsLocalization.mk' Sₚ x s) P = 0

State before:
case intro.intro.intro.intro.refine_2
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ eval₂ (algebraMap Rₚ Sₚ) (IsLocalization.mk' Sₚ x s) P = 0
Tactic:
convert scaleRoots_eval₂_eq_zero _ (r := algebraMap S Sₚ x) _
State after:
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ IsLocalization.mk' Sₚ x s = (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩) * (algebraMap S Sₚ) x

case intro.intro.intro.intro.refine_2.convert_6
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ eval₂ (algebraMap Rₚ Sₚ) ((algebraMap S Sₚ) x) (Polynomial.map (algebraMap R Rₚ) (minpoly R x)) = 0

State before:
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ IsLocalization.mk' Sₚ x s = (algebraMap Rₚ Sₚ) (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩) * (algebraMap S Sₚ) x
Tactic:
rw [this, IsLocalization.map_mk', _root_.map_one, IsLocalization.mk'_eq_mul_mk'_one,
  mul_comm]
State after:
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ IsLocalization.mk' Sₚ 1 s * (algebraMap S Sₚ) x =
    IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) ↑⟨t, ht⟩, ⋯⟩ * (algebraMap S Sₚ) x

State before:
case h.e'_2.h.e'_6
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ IsLocalization.mk' Sₚ 1 s * (algebraMap S Sₚ) x =
    IsLocalization.mk' Sₚ 1 ⟨(algebraMap R S) ↑⟨t, ht⟩, ⋯⟩ * (algebraMap S Sₚ) x
Tactic:
congr
State after:
case h.e'_2.h.e'_6.e_a.e_y
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ s = ⟨(algebraMap R S) ↑⟨t, ht⟩, ⋯⟩

State before:
case h.e'_2.h.e'_6.e_a.e_y
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ s = ⟨(algebraMap R S) ↑⟨t, ht⟩, ⋯⟩
Tactic:
ext
State after:
case h.e'_2.h.e'_6.e_a.e_y.a
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ ↑s = ↑⟨(algebraMap R S) ↑⟨t, ht⟩, ⋯⟩

State before:
case h.e'_2.h.e'_6.e_a.e_y.a
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ ↑s = ↑⟨(algebraMap R S) ↑⟨t, ht⟩, ⋯⟩
Tactic:
exact e.symm
State after:
no goals

State before:
case intro.intro.intro.intro.refine_2.convert_6
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ eval₂ (algebraMap Rₚ Sₚ) ((algebraMap S Sₚ) x) (Polynomial.map (algebraMap R Rₚ) (minpoly R x)) = 0
Tactic:
rw [← aeval_def, ← map_aeval_eq_aeval_map, minpoly.aeval, map_zero]
State after:
case intro.intro.intro.intro.refine_2.convert_6.h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (algebraMap S Sₚ).comp (algebraMap R S)

State before:
case intro.intro.intro.intro.refine_2.convert_6.h
R : Type u_1
S : Type u_2
Rₚ : Type u_3
Sₚ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field Rₚ
inst✝⁹ : CommRing Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : IsSeparable R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
x : S
s : ↥(Algebra.algebraMapSubmonoid S M)
t : R
ht : t ∈ ↑M
e : (algebraMap R S) t = ↑s
P : Rₚ[X] := (Polynomial.map (algebraMap R Rₚ) (minpoly R x)).scaleRoots (IsLocalization.mk' Rₚ 1 ⟨t, ht⟩)
⊢ (algebraMap Rₚ Sₚ).comp (algebraMap R Rₚ) = (algebraMap S Sₚ).comp (algebraMap R S)
Tactic:
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
State after:
no goals