internlm/Lean-Github huggingface dataset:
Theorem: IsSeparable_of_isLocalization
Proof 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 ↦ ?_⟩
Proof 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
Theorem: IsSeparable_of_isLocalization
Proof 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
Proof 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
Theorem: IsSeparable_of_isLocalization
Proof 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
Proof 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
Theorem: IsSeparable_of_isLocalization
Proof 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⟩)
Proof 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
Theorem: IsSeparable_of_isLocalization
Proof 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) ?_)
Proof 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
Theorem: IsSeparable_of_isLocalization
Proof 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
Proof 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ₚ)
Theorem: IsSeparable_of_isLocalization
Proof 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]
Proof state after:
no goals
Theorem: IsSeparable_of_isLocalization
Proof 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
Proof 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⟩)
Theorem: IsSeparable_of_isLocalization
Proof 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 _
Proof state after:
no goals
Theorem: IsSeparable_of_isLocalization
Proof 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]
Proof 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
Theorem: IsSeparable_of_isLocalization
Proof 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) _
Proof 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
Theorem: IsSeparable_of_isLocalization
Proof 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]
Proof 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
Theorem: IsSeparable_of_isLocalization
Proof 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
Proof 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⟩, ⋯⟩
Theorem: IsSeparable_of_isLocalization
Proof 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
Proof 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⟩, ⋯⟩
Theorem: IsSeparable_of_isLocalization
Proof 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
Proof state after:
no goals