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

State before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ IsIntegrallyClosed S
Tactic:
let K := FractionRing R
State after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
⊢ IsIntegrallyClosed S

State before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
⊢ IsIntegrallyClosed S
Tactic:
let g : S →+* K := IsLocalization.map _ (T := R⁰) (RingHom.id R) hM
State after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
⊢ IsIntegrallyClosed S

State before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
⊢ IsIntegrallyClosed S
Tactic:
letI := g.toAlgebra
State after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ IsIntegrallyClosed S

State before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ IsIntegrallyClosed S
Tactic:
have : IsScalarTower R S K := IsScalarTower.of_algebraMap_eq'
  (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
State after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝ : Algebra S K := g.toAlgebra
this : IsScalarTower R S K
⊢ IsIntegrallyClosed S

State before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝ : Algebra S K := g.toAlgebra
this : IsScalarTower R S K
⊢ IsIntegrallyClosed S
Tactic:
have := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M S K
State after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
⊢ IsIntegrallyClosed S

State before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
⊢ IsIntegrallyClosed S
Tactic:
refine (isIntegrallyClosed_iff_isIntegralClosure (K := K)).mpr
  ⟨IsFractionRing.injective _ _, fun {x} ↦ ⟨?_, fun e ↦ e.choose_spec ▸ isIntegral_algebraMap⟩⟩
State after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
⊢ IsIntegral S x → ∃ y, (algebraMap S K) y = x

State before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
⊢ IsIntegral S x → ∃ y, (algebraMap S K) y = x
Tactic:
intro hx
State after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
⊢ ∃ y, (algebraMap S K) y = x

State before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
⊢ ∃ y, (algebraMap S K) y = x
Tactic:
obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
State after:
case intro.mk
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
⊢ ∃ y, (algebraMap S K) y = x

State before:
case intro.mk
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
⊢ ∃ y, (algebraMap S K) y = x
Tactic:
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp ‹_› hy
State after:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ∃ y, (algebraMap S K) y = x

State before:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ∃ y, (algebraMap S K) y = x
Tactic:
refine' ⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr _⟩
State after:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ((algebraMap R K).comp (RingHom.id R)) z = ((algebraMap R K).comp (RingHom.id R)) ↑⟨y, y_mem⟩ * x

State before:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ((algebraMap R K).comp (RingHom.id R)) z = ((algebraMap R K).comp (RingHom.id R)) ↑⟨y, y_mem⟩ * x
Tactic:
rw [RingHom.comp_id, hz, ← Algebra.smul_def]
State after:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x

State before:
case intro.mk.intro
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x
Tactic:
rfl
State after:
no goals

State before:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ algebraMap R K = (algebraMap S K).comp (algebraMap R S)
Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
State after:
no goals